diff --git a/Strata/Languages/Boogie/Options.lean b/Strata/Languages/Boogie/Options.lean index 042feea1..cd36b67f 100644 --- a/Strata/Languages/Boogie/Options.lean +++ b/Strata/Languages/Boogie/Options.lean @@ -4,6 +4,10 @@ SPDX-License-Identifier: Apache-2.0 OR MIT -/ +structure Z3Options where + -- Will prepend `(set-option e.fst e.snd)` ... for each `e: String × String` in `options` + options : List (String × String) + structure Options where verbose : Bool parseOnly : Bool @@ -13,6 +17,8 @@ structure Options where removeIrrelevantAxioms : Bool /-- Solver time limit in seconds -/ solverTimeout : Nat + z3Options: Option Z3Options + def Options.default : Options := { verbose := true, @@ -21,7 +27,8 @@ def Options.default : Options := { checkOnly := false, stopOnFirstError := false, removeIrrelevantAxioms := false, - solverTimeout := 10 + solverTimeout := 10, + z3Options := none, } instance : Inhabited Options where diff --git a/Strata/Languages/Boogie/Verifier.lean b/Strata/Languages/Boogie/Verifier.lean index 55bbd31f..76768b75 100644 --- a/Strata/Languages/Boogie/Verifier.lean +++ b/Strata/Languages/Boogie/Verifier.lean @@ -179,15 +179,27 @@ instance : ToFormat VCResults where instance : ToString VCResults where toString rs := toString (VCResults.format rs) -def getSolverPrelude : String → SolverM Unit -| "z3" => do - -- These options are set by the standard Boogie implementation and are - -- generally good for the Boogie dialect, too, though we may want to - -- have more fine-grained criteria for when to use them. - Solver.setOption "smt.mbqi" "false" - Solver.setOption "auto_config" "false" -| "cvc5" => return () -| _ => return () +def getSolverPrelude (z3Options : Option Z3Options) (solverName : String) : SolverM Unit := + match z3Options with + | .some l => do + let rec go := (λ l => + match l with + | [] => return () + | h :: t => do + Solver.setOption h.fst h.snd + go t + ) + go l.options + | _ => + match solverName with + | "z3" => do + -- These options are set by the standard Boogie implementation and are + -- generally good for the Boogie dialect, too, though we may want to + -- have more fine-grained criteria for when to use them. + Solver.setOption "smt.mbqi" "false" + Solver.setOption "auto_config" "false" + | "cvc5" => return () + | _ => return () def getSolverFlags (options : Options) (solver : String) : Array String := let produceModels := @@ -213,7 +225,7 @@ def dischargeObligation let filename := s!"{VC_folder_name}/{filename}" let handle ← IO.FS.Handle.mk filename IO.FS.Mode.write let solver ← Solver.fileWriter handle - let prelude := getSolverPrelude smtsolver + let prelude := getSolverPrelude options.z3Options smtsolver let (ids, estate) ← Strata.SMT.Encoder.encodeBoogie ctx prelude terms solver let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter if options.verbose then IO.println s!"Wrote problem to {filename}." diff --git a/Strata/Languages/Python/BoogiePrelude.lean b/Strata/Languages/Python/BoogiePrelude.lean index 80715e2b..329629b9 100644 --- a/Strata/Languages/Python/BoogiePrelude.lean +++ b/Strata/Languages/Python/BoogiePrelude.lean @@ -393,18 +393,18 @@ function Timedelta_get_days(timedelta : int) : int; function Timedelta_get_seconds(timedelta : int) : int; function Timedelta_get_microseconds(timedelta : int) : int; -axiom [Timedelta_deconstructors]: - (forall days0 : int, seconds0 : int, msecs0 : int, - days : int, seconds : int, msecs : int - :: {(Timedelta_mk(days0, seconds0, msecs0))} - Timedelta_mk(days0, seconds0, msecs0) == - Timedelta_mk(days, seconds, msecs) && - 0 <= msecs && msecs < 1000000 && - 0 <= seconds && seconds < 3600 * 24 && - -999999999 <= days && days <= 999999999 - ==> Timedelta_get_days(Timedelta_mk(days0, seconds0, msecs0)) == days && - Timedelta_get_seconds(Timedelta_mk(days0, seconds0, msecs0)) == seconds && - Timedelta_get_microseconds(Timedelta_mk(days0, seconds0, msecs0)) == msecs); +//axiom [Timedelta_deconstructors]: +// (forall days0 : int, seconds0 : int, msecs0 : int, +// days : int, seconds : int, msecs : int +// :: {(Timedelta_mk(days0, seconds0, msecs0))} +// Timedelta_mk(days0, seconds0, msecs0) == +// Timedelta_mk(days, seconds, msecs) && +// 0 <= msecs && msecs < 1000000 && +// 0 <= seconds && seconds < 3600 * 24 && +// -999999999 <= days && days <= 999999999 +// ==> Timedelta_get_days(Timedelta_mk(days0, seconds0, msecs0)) == days && +// Timedelta_get_seconds(Timedelta_mk(days0, seconds0, msecs0)) == seconds && +// Timedelta_get_microseconds(Timedelta_mk(days0, seconds0, msecs0)) == msecs); ////// Datetime. diff --git a/Strata/Languages/Python/PythonToBoogie.lean b/Strata/Languages/Python/PythonToBoogie.lean index faa3cef5..9542be00 100644 --- a/Strata/Languages/Python/PythonToBoogie.lean +++ b/Strata/Languages/Python/PythonToBoogie.lean @@ -194,6 +194,7 @@ partial def PyExprToString (e : Python.expr SourceRange) : String := | .Name _ id _ => s!"List[{id.val}]" | _ => panic! s!"Unsupported slice: {repr slice}" | _ => panic! s!"Unsupported subscript to string: {repr e}" + | .Constant _ (.ConString _ s) _ => s.val | _ => panic! s!"Unhandled Expr: {repr e}" def PyExprToMonoTy (e : Python.expr SourceRange) : Lambda.LMonoTy := @@ -609,9 +610,13 @@ partial def PyStmtToBoogie (jmp_targets: List String) (translation_ctx : Transla ([.ite guard (assign_tgt ++ (ArrPyStmtToBoogie translation_ctx body.val).fst) []], none) | _ => panic! s!"tgt must be single name: {repr tgt}" -- TODO: missing havoc - | .Assert _ a _ => + | .Assert _ a msg => let res := PyExprToBoogie translation_ctx a - ([(.assert "py_assertion" res.expr)], none) + match msg.val with + | .some s => + ([(.assert ("py_assertion_" ++ PyExprToString s) res.expr), (.assume ("py_assertion_assume_" ++ PyExprToString s) res.expr)], none) + | _ => + ([(.assert "py_assertion" res.expr), (.assume "py_assertion_assume" res.expr)], none) | .AugAssign _ lhs op rhs => match op with | .Add _ => diff --git a/StrataMain.lean b/StrataMain.lean index 54d994a3..5e2db125 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -208,7 +208,8 @@ def pyAnalyzeCommand : Command where let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f)) (Boogie.verify "z3" newPgm { Options.default with stopOnFirstError := false, verbose, - removeIrrelevantAxioms := true } + removeIrrelevantAxioms := false, + z3Options := some {options := []} } (moreFns := Strata.Python.ReFactory)) let mut s := "" for vcResult in vcResults do diff --git a/StrataTest/Languages/Python/expected/test_datetime.expected b/StrataTest/Languages/Python/expected/test_datetime.expected index 9ca7ad8b..64b00da7 100644 --- a/StrataTest/Languages/Python/expected/test_datetime.expected +++ b/StrataTest/Languages/Python/expected/test_datetime.expected @@ -13,10 +13,10 @@ assert_opt_name_none_or_bar: verified ensures_maybe_except_none: verified -py_assertion: unknown +py_assertion_start_leq_end: verified -py_assertion: unknown +py_assertion_start_dt_eq_start: verified -py_assertion: unknown +py_assertion_end_dt_eq_end: verified -py_assertion: unknown +py_assertion_start_dt_leq_end_dt: verified diff --git a/StrataTest/Languages/Python/tests/test_datetime.py b/StrataTest/Languages/Python/tests/test_datetime.py index 4a82e386..43b98952 100644 --- a/StrataTest/Languages/Python/tests/test_datetime.py +++ b/StrataTest/Languages/Python/tests/test_datetime.py @@ -18,13 +18,13 @@ # my_f_str(str(start), str(end)) -assert start <= end +assert start <= end, "start_leq_end" # These require mbqi / autoconfig start_dt : datetime = datetime.strptime(str(start), "%Y-%m-%d") -assert start_dt == start +assert start_dt == start, "start_dt_eq_start" end_dt : datetime = datetime.strptime(str(end), "%Y-%m-%d") -assert end_dt == end +assert end_dt == end, "end_dt_eq_end" # This is unknown -assert start_dt <= end_dt +assert start_dt <= end_dt, "start_dt_leq_end_dt"