From 2cf6df2151becc2820eb3bb3961a32dbdb1f8fe5 Mon Sep 17 00:00:00 2001 From: Stevendeo Date: Wed, 29 Nov 2023 11:04:35 +0100 Subject: [PATCH] Fix timelimit per goal (#984) * Stop process decl as soon as a status is printed * Update tests --- src/bin/common/solving_loop.ml | 13 +++-- .../testfile-qfbv-timeout.dolmen.expected | 9 +++ tests/bitv/testfile-qfbv-timeout.dolmen.smt2 | 58 +++++++++++++++++++ tests/dune.inc | 21 +++++++ 4 files changed, 97 insertions(+), 4 deletions(-) create mode 100644 tests/bitv/testfile-qfbv-timeout.dolmen.expected create mode 100644 tests/bitv/testfile-qfbv-timeout.dolmen.smt2 diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 476630bcd..3d720dc0a 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -129,6 +129,8 @@ type solve_res = | Unknown of model option | Unsat +exception StopProcessDecl + let main () = let () = Dolmen_loop.Code.init [] in @@ -154,12 +156,15 @@ let main () = match status with | Timeout _ when not (Options.get_timelimit_per_goal ()) -> exit_as_timeout () - | _ -> () + | _ -> raise StopProcessDecl in let () = - List.iter - (FE.process_decl ~hook_on_status ftdn_env) - cnf + try + List.iter + (FE.process_decl ~hook_on_status ftdn_env) + cnf + with + | StopProcessDecl -> () in if Options.get_timelimit_per_goal() then Options.Time.unset_timeout (); diff --git a/tests/bitv/testfile-qfbv-timeout.dolmen.expected b/tests/bitv/testfile-qfbv-timeout.dolmen.expected new file mode 100644 index 000000000..3c63839ab --- /dev/null +++ b/tests/bitv/testfile-qfbv-timeout.dolmen.expected @@ -0,0 +1,9 @@ + +unknown +(:reason-unknown (:timeout :assume)) + +unknown +(:reason-unknown (:timeout :assume)) + +unknown +(:reason-unknown (:timeout :assume)) diff --git a/tests/bitv/testfile-qfbv-timeout.dolmen.smt2 b/tests/bitv/testfile-qfbv-timeout.dolmen.smt2 new file mode 100644 index 000000000..27fcf0299 --- /dev/null +++ b/tests/bitv/testfile-qfbv-timeout.dolmen.smt2 @@ -0,0 +1,58 @@ +(set-info :smt-lib-version 2.6) +(set-option :reproducible-resource-limit 1) +(set-logic QF_BV) +(set-info :source | + Patrice Godefroid, SAGE (systematic dynamic test generation) + For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf +|) +(set-info :category "industrial") +(set-info :status unsat) +(declare-fun T4_11167 () (_ BitVec 32)) +(declare-fun T2_10410 () (_ BitVec 16)) +(declare-fun T2_10408 () (_ BitVec 16)) +(declare-fun T2_10475 () (_ BitVec 16)) +(declare-fun T2_10473 () (_ BitVec 16)) +(declare-fun T2_10532 () (_ BitVec 16)) +(declare-fun T2_10530 () (_ BitVec 16)) +(declare-fun T2_10606 () (_ BitVec 16)) +(declare-fun T2_10604 () (_ BitVec 16)) +(declare-fun T2_10669 () (_ BitVec 16)) +(declare-fun T2_10667 () (_ BitVec 16)) +(declare-fun T2_10734 () (_ BitVec 16)) +(declare-fun T2_10736 () (_ BitVec 16)) +(declare-fun T1_11167 () (_ BitVec 8)) +(declare-fun T1_11168 () (_ BitVec 8)) +(declare-fun T1_11169 () (_ BitVec 8)) +(declare-fun T1_11170 () (_ BitVec 8)) +(declare-fun T1_10736 () (_ BitVec 8)) +(declare-fun T1_10737 () (_ BitVec 8)) +(declare-fun T1_10734 () (_ BitVec 8)) +(declare-fun T1_10735 () (_ BitVec 8)) +(declare-fun T1_10669 () (_ BitVec 8)) +(declare-fun T1_10670 () (_ BitVec 8)) +(declare-fun T1_10667 () (_ BitVec 8)) +(declare-fun T1_10668 () (_ BitVec 8)) +(declare-fun T1_10606 () (_ BitVec 8)) +(declare-fun T1_10607 () (_ BitVec 8)) +(declare-fun T1_10604 () (_ BitVec 8)) +(declare-fun T1_10605 () (_ BitVec 8)) +(declare-fun T1_10532 () (_ BitVec 8)) +(declare-fun T1_10533 () (_ BitVec 8)) +(declare-fun T1_10530 () (_ BitVec 8)) +(declare-fun T1_10531 () (_ BitVec 8)) +(declare-fun T1_10475 () (_ BitVec 8)) +(declare-fun T1_10476 () (_ BitVec 8)) +(declare-fun T1_10473 () (_ BitVec 8)) +(declare-fun T1_10474 () (_ BitVec 8)) +(declare-fun T1_10410 () (_ BitVec 8)) +(declare-fun T1_10411 () (_ BitVec 8)) +(declare-fun T1_10408 () (_ BitVec 8)) +(declare-fun T1_10409 () (_ BitVec 8)) +(assert (let ((?v_0 (bvadd T4_11167 (_ bv4 32))) (?v_12 ((_ zero_extend 16) T2_10408))) (let ((?v_10 (bvadd ?v_0 (bvsub (bvadd (bvadd (bvadd ?v_0 (_ bv61 32)) ?v_12) ((_ zero_extend 16) T2_10410)) ?v_0)))) (let ((?v_1 (bvadd ?v_10 (_ bv4 32))) (?v_18 ((_ zero_extend 16) T2_10473))) (let ((?v_16 (bvadd ?v_1 (bvsub (bvadd (bvadd (bvadd ?v_1 (_ bv53 32)) ?v_18) ((_ zero_extend 16) T2_10475)) ?v_1)))) (let ((?v_2 (bvadd ?v_16 (_ bv4 32))) (?v_24 ((_ zero_extend 16) T2_10530))) (let ((?v_22 (bvadd ?v_2 (bvsub (bvadd (bvadd (bvadd ?v_2 (_ bv70 32)) ?v_24) ((_ zero_extend 16) T2_10532)) ?v_2)))) (let ((?v_3 (bvadd ?v_22 (_ bv4 32))) (?v_30 ((_ zero_extend 16) T2_10604))) (let ((?v_28 (bvadd ?v_3 (bvsub (bvadd (bvadd (bvadd ?v_3 (_ bv59 32)) ?v_30) ((_ zero_extend 16) T2_10606)) ?v_3)))) (let ((?v_4 (bvadd ?v_28 (_ bv4 32))) (?v_36 ((_ zero_extend 16) T2_10667))) (let ((?v_34 (bvadd ?v_4 (bvsub (bvadd (bvadd (bvadd ?v_4 (_ bv63 32)) ?v_36) ((_ zero_extend 16) T2_10669)) ?v_4)))) (let ((?v_5 (bvadd ?v_34 (_ bv4 32)))) (let ((?v_40 (bvadd ?v_5 (_ bv42 32))) (?v_39 ((_ zero_extend 16) T2_10734)) (?v_38 (bvadd ?v_4 (_ bv42 32))) (?v_37 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_5) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_35 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_34) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_33 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_40) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_32 (bvadd ?v_3 (_ bv42 32))) (?v_31 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_4) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_29 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_28) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_27 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_38) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_26 (bvadd ?v_2 (_ bv42 32))) (?v_25 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_3) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_23 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_22) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_21 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_32) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_20 (bvadd ?v_1 (_ bv42 32))) (?v_19 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_2) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_17 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_16) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_15 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_26) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_14 (bvadd ?v_0 (_ bv42 32))) (?v_13 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_1) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_11 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_10) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_9 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_20) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_8 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_0) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_7 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) T4_11167) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_6 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_14) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (and true (= T2_10408 (bvor (bvshl ((_ zero_extend 8) T1_10409) (_ bv8 16)) ((_ zero_extend 8) T1_10408))) (= T2_10410 (bvor (bvshl ((_ zero_extend 8) T1_10411) (_ bv8 16)) ((_ zero_extend 8) T1_10410))) (= T2_10473 (bvor (bvshl ((_ zero_extend 8) T1_10474) (_ bv8 16)) ((_ zero_extend 8) T1_10473))) (= T2_10475 (bvor (bvshl ((_ zero_extend 8) T1_10476) (_ bv8 16)) ((_ zero_extend 8) T1_10475))) (= T2_10530 (bvor (bvshl ((_ zero_extend 8) T1_10531) (_ bv8 16)) ((_ zero_extend 8) T1_10530))) (= T2_10532 (bvor (bvshl ((_ zero_extend 8) T1_10533) (_ bv8 16)) ((_ zero_extend 8) T1_10532))) (= T2_10604 (bvor (bvshl ((_ zero_extend 8) T1_10605) (_ bv8 16)) ((_ zero_extend 8) T1_10604))) (= T2_10606 (bvor (bvshl ((_ zero_extend 8) T1_10607) (_ bv8 16)) ((_ zero_extend 8) T1_10606))) (= T2_10667 (bvor (bvshl ((_ zero_extend 8) T1_10668) (_ bv8 16)) ((_ zero_extend 8) T1_10667))) (= T2_10669 (bvor (bvshl ((_ zero_extend 8) T1_10670) (_ bv8 16)) ((_ zero_extend 8) T1_10669))) (= T2_10734 (bvor (bvshl ((_ zero_extend 8) T1_10735) (_ bv8 16)) ((_ zero_extend 8) T1_10734))) (= T2_10736 (bvor (bvshl ((_ zero_extend 8) T1_10737) (_ bv8 16)) ((_ zero_extend 8) T1_10736))) (= T4_11167 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_11170) (_ bv8 32)) ((_ zero_extend 24) T1_11169)) (_ bv8 32)) ((_ zero_extend 24) T1_11168)) (_ bv8 32)) ((_ zero_extend 24) T1_11167))) (bvslt (bvadd ?v_5 (bvsub (bvadd (bvadd (bvadd ?v_5 (_ bv64 32)) ?v_39) ((_ zero_extend 16) T2_10736)) ?v_5)) (_ bv0 32)) (bvult (_ bv0 32) ?v_6) (bvule (_ bv0 32) ?v_6) (bvult (_ bv0 32) ?v_7) (bvule (_ bv0 32) ?v_7) (bvult (_ bv0 32) ?v_8) (bvule (_ bv0 32) ?v_8) (bvult (_ bv0 32) ?v_9) (bvule (_ bv0 32) ?v_9) (bvult (_ bv0 32) ?v_11) (bvule (_ bv0 32) ?v_11) (= ?v_12 (_ bv0 32)) (bvult (_ bv0 32) ?v_13) (bvule (_ bv0 32) ?v_13) (not (= ?v_14 (_ bv4294967295 32))) (bvule (_ bv0 32) T4_11167) (not (= T4_11167 (_ bv11151 32))) (bvule T4_11167 (_ bv11151 32)) (not (= T4_11167 (_ bv4294967295 32))) (bvult (_ bv0 32) ?v_15) (bvule (_ bv0 32) ?v_15) (bvult (_ bv0 32) ?v_17) (bvule (_ bv0 32) ?v_17) (= ?v_18 (_ bv0 32)) (not (= ?v_0 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_0) (bvult (_ bv0 32) ?v_19) (bvule (_ bv0 32) ?v_19) (not (= ?v_20 (_ bv4294967295 32))) (not (= ?v_10 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_10) (bvult (_ bv0 32) ?v_21) (bvule (_ bv0 32) ?v_21) (bvult (_ bv0 32) ?v_23) (bvule (_ bv0 32) ?v_23) (= ?v_24 (_ bv0 32)) (not (= ?v_1 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_1) (bvult (_ bv0 32) ?v_25) (bvule (_ bv0 32) ?v_25) (not (= ?v_26 (_ bv4294967295 32))) (not (= ?v_16 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_16) (bvult (_ bv0 32) ?v_27) (bvule (_ bv0 32) ?v_27) (bvult (_ bv0 32) ?v_29) (bvule (_ bv0 32) ?v_29) (= ?v_30 (_ bv0 32)) (not (= ?v_2 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_2) (bvult (_ bv0 32) ?v_31) (bvule (_ bv0 32) ?v_31) (not (= ?v_32 (_ bv4294967295 32))) (not (= ?v_22 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_22) (bvult (_ bv0 32) ?v_33) (bvule (_ bv0 32) ?v_33) (bvult (_ bv0 32) ?v_35) (bvule (_ bv0 32) ?v_35) (= ?v_36 (_ bv0 32)) (not (= ?v_3 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_3) (bvult (_ bv0 32) ?v_37) (bvule (_ bv0 32) ?v_37) (not (= ?v_38 (_ bv4294967295 32))) (not (= ?v_28 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_28) (= ?v_39 (_ bv0 32)) (not (= ?v_4 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_4) (not (= ?v_40 (_ bv4294967295 32))) (not (= ?v_34 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_34) (not (= ?v_5 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_5)))))))))))))))))) +(check-sat) +(get-info :reason-unknown) +(check-sat) +(get-info :reason-unknown) +(check-sat) +(get-info :reason-unknown) +(exit) diff --git a/tests/dune.inc b/tests/dune.inc index 834fd3cff..6d6a0bac6 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -120739,6 +120739,27 @@ ; Auto-generated part begin (subdir bitv + (rule + (target testfile-qfbv-timeout.dolmen_dolmen.output) + (deps (:input testfile-qfbv-timeout.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-qfbv-timeout.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-qfbv-timeout.dolmen.expected testfile-qfbv-timeout.dolmen_dolmen.output))) (rule (target testfile-int2bv-immediate.dolmen_dolmen.output) (deps (:input testfile-int2bv-immediate.dolmen.smt2))