diff --git a/CHANGES.md b/CHANGES.md index 5205d252f4..6100f40b21 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -6,12 +6,18 @@ This release supports [version ## Changes +* The `cryptol_load` and `cryptol_prims` commands now fail if used + in a nested scope, instead of behaving strangely. + * The old behavior of SAWScript where top-level names could be arbitrarily rebound, such that existing uses would see the updated value, has been superseded. Among other problems, it wasn't type safe. - Substitute functionality is now available by using the new syntax - `let rebindable`. + Now, rebinding a variable creates a new variable that hides the + old one; prior references are not affected. + + Substitute functionality for the old behavior is now available by + using the new syntax `let rebindable`. After `let rebindable x = 3`, `x` is mutable and a subsequent `let rebindable x = 4` will change the value seen by all uses. The value type must remain the same; to avoid unnecessary @@ -174,6 +180,16 @@ This release supports [version ## Bug Fixes +* The Cryptol environment now tracks SAWScript scopes properly (#2304). + Note though that SAWCore-level names, which are for example bound by + uses of `let {{ ... }}`, are still not scoped and can trigger + duplicate variable errors. + See #2726 for further information. + +* A number of internal weirdnesses in SAWScript's internal variable handling + have been cleaned out; for example, bindings made in `proof_subshell` no + longer escape the subshell (#2243). + * Fix a bug that would cause SAW to crash when loading an instantiation of a parameterized Cryptol module that contains newtypes or enums (#2673). diff --git a/examples/ecdsa/ecdsa.saw b/examples/ecdsa/ecdsa.saw index 66e23645ee..9d9a5b8ed1 100644 --- a/examples/ecdsa/ecdsa.saw +++ b/examples/ecdsa/ecdsa.saw @@ -412,115 +412,102 @@ p384_point_ops_sub_simp <- do { }; p384_point_ops_field_mul_simp <- do { - let {{ thm x = p384_ec_point_ops::p384_point_ops.field.mul x == - p384_field::p384_field_mul x }}; + let t = {{ \x -> p384_ec_point_ops::p384_point_ops.field.mul x == + p384_field::p384_field_mul x }}; // This is pretty quick even without the rewriting and uniterpretation // used above. - let t = unfold_term ["thm"] {{ thm }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_point_ops_field_sq_simp <- do { - let {{ thm x = p384_ec_point_ops::p384_point_ops.field.sq x == - p384_field::p384_field_sq x }}; + let t = {{ \x -> p384_ec_point_ops::p384_point_ops.field.sq x == + p384_field::p384_field_sq x }}; // This is pretty quick even without the rewriting and uninterpretation // used above. - let t = unfold_term ["thm"] {{ thm }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_point_ops_field_mul_simp2 <- do { - let {{ thm x = ecc::p384_curve.point_ops.field.mul x == - p384_field::p384_field_mul x }}; + let t = {{ \x -> ecc::p384_curve.point_ops.field.mul x == + p384_field::p384_field_mul x }}; // This is pretty quick even without the rewriting and uniterpretation // used above. - let t = unfold_term ["thm"] {{ thm }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_point_ops_field_sq_simp2 <- do { - let {{ thm x = ecc::p384_curve.point_ops.field.sq x == - p384_field::p384_field_sq x }}; + let t = {{ \x -> ecc::p384_curve.point_ops.field.sq x == + p384_field::p384_field_sq x }}; // This is pretty quick even without the rewriting and uniterpretation // used above. - let t = unfold_term ["thm"] {{ thm }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_curve_field_mul_simp <- do { - let {{ thm x y = ecc::p384_curve.point_ops.group_field.mul (x, y) == - mul_java::p384_group_mul (p384_field::p384_group_size, x, y) }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x y -> ecc::p384_curve.point_ops.group_field.mul (x, y) == + mul_java::p384_group_mul (p384_field::p384_group_size, x, y) }}; let t = rewrite ss0 t; //print_term t; prove_print (unint_z3 ["p384_group_mul"]) t; }; p384_curve_field_sq_simp <- do { - let {{ thm x = ecc::p384_curve.point_ops.group_field.sq x == - p384_field::p384_mod_mul (p384_field::p384_group_size, x, x) }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x -> ecc::p384_curve.point_ops.group_field.sq x == + p384_field::p384_mod_mul (p384_field::p384_group_size, x, x) }}; let t = rewrite ss0 t; //print_term t; prove_print (unint_z3 ["p384_mod_mul"]) t; }; p384_curve_field_div_simp <- do { - let {{ thm x y = ecc::p384_curve.point_ops.group_field.div (x,y) == - p384_field::p384_mod_div (p384_field::p384_group_size, x, y) }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x y -> ecc::p384_curve.point_ops.group_field.div (x,y) == + p384_field::p384_mod_div (p384_field::p384_group_size, x, y) }}; let t = rewrite ss0 t; //print_term t; prove_print (unint_z3 ["p384_mod_div"]) t; }; p384_curve_twin_mul_simp <- do { - let {{ thm x = ecc::p384_curve.twin_mul x == - p384_ec_mul::p384_ec_twin_mul x }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x -> ecc::p384_curve.twin_mul x == + p384_ec_mul::p384_ec_twin_mul x }}; let t = rewrite ss0 t; //print_term t; prove_print (unint_z3 ["p384_ec_twin_mul"]) t; }; p384_curve_is_equal_simp <- do { - let {{ thm x y = ecc::p384_curve.point_ops.group_field.is_equal (x, y) == - (x == y) }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x y -> ecc::p384_curve.point_ops.group_field.is_equal (x, y) == + (x == y) }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_curve_is_val_simp <- do { - let {{ thm x = ecc::p384_curve.point_ops.group_field.is_val x == - p384_field::p384_is_group_val x }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x -> ecc::p384_curve.point_ops.group_field.is_val x == + p384_field::p384_is_group_val x }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_curve_norm_simp <- do { - let {{ thm x = ecc::p384_curve.point_ops.group_field.normalize x == - (if x < p384_field::p384_group_size - then x - else x - p384_field::p384_group_size) }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ \x -> ecc::p384_curve.point_ops.group_field.normalize x == + (if x < p384_field::p384_group_size + then x + else x - p384_field::p384_group_size) }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_curve_field_zero_simp <- do { - let {{ thm = ecc::p384_curve.point_ops.group_field.field_zero == 0 }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ ecc::p384_curve.point_ops.group_field.field_zero == 0 }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; }; p384_curve_base_simp <- do { - let {{ thm = ecc::p384_curve.base == ecc::p384_base }}; - let t = unfold_term ["thm"] {{ thm }}; + let t = {{ ecc::p384_curve.base == ecc::p384_base }}; let t = rewrite ss0 t; //print_term t; prove_print z3 t; diff --git a/intTests/test1646/test01.log.good b/intTests/test1646/test01.log.good new file mode 100644 index 0000000000..5b50ca7d31 --- /dev/null +++ b/intTests/test1646/test01.log.good @@ -0,0 +1,5 @@ + Loading file "test01.saw" + x=a + test01.saw:8:5-8:6: Warning: Redeclaration of x + test01.saw:3:5-3:6: Warning: Previous declaration was here + x=a diff --git a/intTests/test1646/test1.saw b/intTests/test1646/test01.saw similarity index 63% rename from intTests/test1646/test1.saw rename to intTests/test1646/test01.saw index fe91352f73..cc9ffecd38 100644 --- a/intTests/test1646/test1.saw +++ b/intTests/test1646/test01.saw @@ -1,4 +1,4 @@ -// The second f call will print x=b. +// The second f call nowadays will print x=a. let x = "a"; diff --git a/intTests/test1646/test02.log.good b/intTests/test1646/test02.log.good new file mode 100644 index 0000000000..4e3cd46602 --- /dev/null +++ b/intTests/test1646/test02.log.good @@ -0,0 +1,5 @@ + Loading file "test02.saw" + x=a + test02.saw:8:5-8:6: Warning: Redeclaration of x + test02.saw:3:5-3:6: Warning: Previous declaration was here + x=a diff --git a/intTests/test1646/test2.saw b/intTests/test1646/test02.saw similarity index 51% rename from intTests/test1646/test2.saw rename to intTests/test1646/test02.saw index a57757ce67..5f51b70f43 100644 --- a/intTests/test1646/test2.saw +++ b/intTests/test1646/test02.saw @@ -1,4 +1,4 @@ -// The second f call will panic with an internal type error. +// The second f call nowadays just prints a. let x = "a"; @@ -6,4 +6,4 @@ let f () = print (str_concat "x=" x); f (); let x = 5; -f(); +f (); diff --git a/intTests/test1646/test03.log.good b/intTests/test1646/test03.log.good new file mode 100644 index 0000000000..ae4020811c --- /dev/null +++ b/intTests/test1646/test03.log.good @@ -0,0 +1,5 @@ + Loading file "test03.saw" + test03.saw:9:8-9:9: Warning: Redeclaration of x + test03.saw:4:8-4:9: Warning: Previous declaration was here + x=a + x=a diff --git a/intTests/test1646/test3.saw b/intTests/test1646/test03.saw similarity index 100% rename from intTests/test1646/test3.saw rename to intTests/test1646/test03.saw diff --git a/intTests/test1646/test04.log.good b/intTests/test1646/test04.log.good new file mode 100644 index 0000000000..80b2647e97 --- /dev/null +++ b/intTests/test1646/test04.log.good @@ -0,0 +1,5 @@ + Loading file "test04.saw" + test04.saw:9:8-9:9: Warning: Redeclaration of x + test04.saw:4:8-4:9: Warning: Previous declaration was here + x=a + x=a diff --git a/intTests/test1646/test4.saw b/intTests/test1646/test04.saw similarity index 100% rename from intTests/test1646/test4.saw rename to intTests/test1646/test04.saw diff --git a/intTests/test1646/test05.log.good b/intTests/test1646/test05.log.good new file mode 100644 index 0000000000..607fa10161 --- /dev/null +++ b/intTests/test1646/test05.log.good @@ -0,0 +1,3 @@ + Loading file "test05.saw" + x=a + x=b diff --git a/intTests/test1646/test5.saw b/intTests/test1646/test05.saw similarity index 100% rename from intTests/test1646/test5.saw rename to intTests/test1646/test05.saw diff --git a/intTests/test1646/test06.log.good b/intTests/test1646/test06.log.good new file mode 100644 index 0000000000..6e470ceed5 --- /dev/null +++ b/intTests/test1646/test06.log.good @@ -0,0 +1,13 @@ + Loading file "test06.saw" + x=a + test06.saw:8:16-8:17: Type mismatch. + Mismatch of type constructors. Expected: Int but got String + test06.saw:8:20-8:21: The type Int arises from the type of this term + test06.saw:3:20-3:23: The type String arises from the type of this term + + Expected: Int + Found: String + + within "x" (test06.saw:8:16-8:17) + +FAILED diff --git a/intTests/test1646/test6.saw b/intTests/test1646/test06.saw similarity index 100% rename from intTests/test1646/test6.saw rename to intTests/test1646/test06.saw diff --git a/intTests/test1646/test07.log.good b/intTests/test1646/test07.log.good new file mode 100644 index 0000000000..b541b3f4b9 --- /dev/null +++ b/intTests/test1646/test07.log.good @@ -0,0 +1,8 @@ + Loading file "test07.saw" + Type errors: + test07.saw:4:4-4:26: Invalid use of 'rebindable' + test07.saw:4:4-4:26: It is only allowed at the syntactic top level + test07.saw:9:4-9:26: Invalid use of 'rebindable' + test07.saw:9:4-9:26: It is only allowed at the syntactic top level + +FAILED diff --git a/intTests/test1646/test7.saw b/intTests/test1646/test07.saw similarity index 100% rename from intTests/test1646/test7.saw rename to intTests/test1646/test07.saw diff --git a/intTests/test1646/test08.log.good b/intTests/test1646/test08.log.good new file mode 100644 index 0000000000..e7e24e874d --- /dev/null +++ b/intTests/test1646/test08.log.good @@ -0,0 +1,8 @@ + Loading file "test08.saw" + Type errors: + test08.saw:4:4-4:26: Invalid use of 'rebindable' + test08.saw:4:4-4:26: It is only allowed at the syntactic top level + test08.saw:9:4-9:26: Invalid use of 'rebindable' + test08.saw:9:4-9:26: It is only allowed at the syntactic top level + +FAILED diff --git a/intTests/test1646/test8.saw b/intTests/test1646/test08.saw similarity index 100% rename from intTests/test1646/test8.saw rename to intTests/test1646/test08.saw diff --git a/intTests/test1646/test09.log.good b/intTests/test1646/test09.log.good new file mode 100644 index 0000000000..b3906ea246 --- /dev/null +++ b/intTests/test1646/test09.log.good @@ -0,0 +1,4 @@ + Loading file "test09.saw" + test09.saw:7:4-7:5: Warning: Redeclaration of x + test09.saw:4:16-4:17: Warning: Previous declaration was here + a diff --git a/intTests/test1646/test09.saw b/intTests/test1646/test09.saw new file mode 100644 index 0000000000..48b80a14b7 --- /dev/null +++ b/intTests/test1646/test09.saw @@ -0,0 +1,11 @@ +// This should print a. Binding x in a nested scope should have no +// effect. + +let rebindable x = "a"; + +do { + x <- return 3; + return (); +}; + +print x; diff --git a/intTests/test1646/test1.log.good b/intTests/test1646/test1.log.good deleted file mode 100644 index 94176e07f8..0000000000 --- a/intTests/test1646/test1.log.good +++ /dev/null @@ -1,5 +0,0 @@ - Loading file "test1.saw" - x=a - test1.saw:8:5-8:6: Warning: Redeclaration of x - test1.saw:3:5-3:6: Warning: Previous declaration was here - x=b diff --git a/intTests/test1646/test10.log.good b/intTests/test1646/test10.log.good new file mode 100644 index 0000000000..704f397d3c --- /dev/null +++ b/intTests/test1646/test10.log.good @@ -0,0 +1,4 @@ + Loading file "test10.saw" + test10.saw:7:8-7:9: Warning: Redeclaration of x + test10.saw:4:16-4:17: Warning: Previous declaration was here + a diff --git a/intTests/test1646/test10.saw b/intTests/test1646/test10.saw new file mode 100644 index 0000000000..28632b712c --- /dev/null +++ b/intTests/test1646/test10.saw @@ -0,0 +1,11 @@ +// This should print a. Binding x in a nested scope creates a new +// variable and should have no effect on the rebindable one. + +let rebindable x = "a"; + +do { + let x = 3; + return (); +}; + +print x; diff --git a/intTests/test1646/test11.log.good b/intTests/test1646/test11.log.good new file mode 100644 index 0000000000..8cd730fdca --- /dev/null +++ b/intTests/test1646/test11.log.good @@ -0,0 +1,5 @@ + Loading file "test11.saw" + test11.saw:6:8-6:9: Warning: Redeclaration of x + test11.saw:3:16-3:17: Warning: Previous declaration was here + 3 + b diff --git a/intTests/test1646/test11.saw b/intTests/test1646/test11.saw new file mode 100644 index 0000000000..9d7273fda5 --- /dev/null +++ b/intTests/test1646/test11.saw @@ -0,0 +1,12 @@ +// This should print 3 then b. + +let rebindable x = "a"; + +do { + let x = 3; + print x; + return (); +}; + +let rebindable x = "b"; +print x; diff --git a/intTests/test1646/test12.log.good b/intTests/test1646/test12.log.good new file mode 100644 index 0000000000..f7441a2570 --- /dev/null +++ b/intTests/test1646/test12.log.good @@ -0,0 +1,7 @@ + Loading file "test12.saw" + test12.saw:6:8-6:9: Warning: Redeclaration of x + test12.saw:3:16-3:17: Warning: Previous declaration was here + 3 + test12.saw:11:5-11:6: Warning: Redeclaration of x + test12.saw:3:16-3:17: Warning: Previous declaration was here + b diff --git a/intTests/test1646/test12.saw b/intTests/test1646/test12.saw new file mode 100644 index 0000000000..269f88b477 --- /dev/null +++ b/intTests/test1646/test12.saw @@ -0,0 +1,13 @@ +// This should print 3 then b. + +let rebindable x = "a"; + +do { + let x = 3; + print x; + return (); +}; + +let x = "b"; +print x; + diff --git a/intTests/test1646/test13.log.good b/intTests/test1646/test13.log.good new file mode 100644 index 0000000000..5537d3f2b8 --- /dev/null +++ b/intTests/test1646/test13.log.good @@ -0,0 +1,9 @@ + Loading file "test13.saw" + test13.saw:7:8-7:9: Warning: Redeclaration of x + test13.saw:4:16-4:17: Warning: Previous declaration was here + 3 + test13.saw:12:5-12:6: Warning: Redeclaration of x + test13.saw:4:16-4:17: Warning: Previous declaration was here + b + test13.saw:15:16-15:17: Cannot rebind x: Previous binding was not tagged 'rebindable' +FAILED diff --git a/intTests/test1646/test13.saw b/intTests/test1646/test13.saw new file mode 100644 index 0000000000..713e1eef4a --- /dev/null +++ b/intTests/test1646/test13.saw @@ -0,0 +1,16 @@ +// This is rejected; once the rebindable tag is dropped it can't be +// readded. + +let rebindable x = "a"; + +do { + let x = 3; + print x; + return (); +}; + +let x = "b"; +print x; + +let rebindable x = "c"; +print x; diff --git a/intTests/test1646/test14.log.good b/intTests/test1646/test14.log.good new file mode 100644 index 0000000000..c48add3cb8 --- /dev/null +++ b/intTests/test1646/test14.log.good @@ -0,0 +1,6 @@ + Loading file "test14.saw" + x=a + x=b + test14.saw:11:5-11:6: Warning: Redeclaration of x + test14.saw:8:16-8:17: Warning: Previous declaration was here + x=b diff --git a/intTests/test1646/test14.saw b/intTests/test1646/test14.saw new file mode 100644 index 0000000000..ccfbb96743 --- /dev/null +++ b/intTests/test1646/test14.saw @@ -0,0 +1,12 @@ +// The second f call should print x=b. So should the third. + +let rebindable x = "a"; + +let f () = print (str_concat "x=" x); +f (); + +let rebindable x = "b"; +f (); + +let x = "c"; +f (); diff --git a/intTests/test1646/test15.isaw b/intTests/test1646/test15.isaw new file mode 100644 index 0000000000..8e96a0289d --- /dev/null +++ b/intTests/test1646/test15.isaw @@ -0,0 +1,4 @@ +let rebindable x = 3 +let rebindable y = 4 +let y = 5 +:env diff --git a/intTests/test1646/test15.log.good b/intTests/test1646/test15.log.good new file mode 100644 index 0000000000..2d10dee2f4 --- /dev/null +++ b/intTests/test1646/test15.log.good @@ -0,0 +1,351 @@ + :1:5-1:6: Warning: Redeclaration of y + :1:16-1:17: Warning: Previous declaration was here +x : rebindable Int +y : rebindable Int + +abc : ProofScript () +abstract_symbolic : Term -> Term +add_cryptol_defs : [String] -> Simpset -> Simpset +add_cryptol_eqs : [String] -> Simpset -> Simpset +add_prelude_defs : [String] -> Simpset -> Simpset +add_prelude_eqs : [String] -> Simpset -> Simpset +add_x86_preserved_reg : String -> TopLevel () +addsimp : Theorem -> Simpset -> Simpset +addsimp_shallow : Theorem -> Simpset -> Simpset +addsimps : [Theorem] -> Simpset -> Simpset +admit : String -> ProofScript () +approxmc : Term -> TopLevel () +assume_unsat : ProofScript () +assume_valid : ProofScript () +auto_match : String -> String -> TopLevel () +basic_ss : Simpset +beta_reduce_goal : ProofScript () +beta_reduce_term : Term -> Term +bitblast : Term -> TopLevel AIG +bitwuzla : ProofScript () +boolector : ProofScript () +caseProofResult : {b} ProofResult -> (Theorem -> b) -> (Term -> b) -> b +caseSatResult : {b} SatResult -> b -> (Term -> b) -> b +check_convertible : Term -> Term -> TopLevel () +check_goal : ProofScript () +check_term : Term -> TopLevel () +clean_mismatched_versions_solver_cache : TopLevel () +codegen : String -> [String] -> String -> Term -> TopLevel () +concat : {a} [a] -> [a] -> [a] +core_axiom : String -> Theorem +core_thm : String -> Theorem +crucible_alloc : LLVMType -> LLVMSetup SetupValue +crucible_alloc_aligned : Int -> LLVMType -> LLVMSetup SetupValue +crucible_alloc_global : String -> LLVMSetup () +crucible_alloc_readonly : LLVMType -> LLVMSetup SetupValue +crucible_alloc_readonly_aligned : Int -> LLVMType -> LLVMSetup SetupValue +crucible_array : [SetupValue] -> SetupValue +crucible_conditional_points_to : Term -> SetupValue -> SetupValue -> LLVMSetup () +crucible_conditional_points_to_untyped : Term -> SetupValue -> SetupValue -> LLVMSetup () +crucible_declare_ghost_state : String -> TopLevel Ghost +crucible_elem : SetupValue -> Int -> SetupValue +crucible_equal : SetupValue -> SetupValue -> LLVMSetup () +crucible_execute_func : [SetupValue] -> LLVMSetup () +crucible_field : SetupValue -> String -> SetupValue +crucible_fresh_expanded_val : LLVMType -> LLVMSetup SetupValue +crucible_fresh_pointer : LLVMType -> LLVMSetup SetupValue +crucible_fresh_var : String -> LLVMType -> LLVMSetup Term +crucible_ghost_value : Ghost -> Term -> LLVMSetup () +crucible_global : String -> SetupValue +crucible_global_initializer : String -> SetupValue +crucible_java_extract : JavaClass -> String -> TopLevel Term +crucible_llvm_extract : LLVMModule -> String -> TopLevel Term +crucible_llvm_unsafe_assume_spec : LLVMModule -> String -> LLVMSetup () -> TopLevel LLVMSpec +crucible_llvm_verify : LLVMModule -> String -> [LLVMSpec] -> Bool -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec +crucible_null : SetupValue +crucible_packed_struct : [SetupValue] -> SetupValue +crucible_points_to : SetupValue -> SetupValue -> LLVMSetup () +crucible_points_to_untyped : SetupValue -> SetupValue -> LLVMSetup () +crucible_postcond : Term -> LLVMSetup () +crucible_precond : Term -> LLVMSetup () +crucible_return : SetupValue -> LLVMSetup () +crucible_spec_size : LLVMSpec -> Int +crucible_spec_solvers : LLVMSpec -> [String] +crucible_struct : [SetupValue] -> SetupValue +crucible_symbolic_alloc : Bool -> Int -> Term -> LLVMSetup SetupValue +crucible_term : Term -> SetupValue +cryptol_add_path : String -> TopLevel () +cryptol_extract : CryptolModule -> String -> TopLevel Term +cryptol_load : String -> TopLevel CryptolModule +cryptol_prims : () -> CryptolModule +cryptol_ss : () -> Simpset +cvc4 : ProofScript () +cvc5 : ProofScript () +declare_ghost_state : String -> TopLevel Ghost +default_x86_preserved_reg : TopLevel () +define : String -> Term -> TopLevel Term +disable_alloc_sym_init_check : TopLevel () +disable_crucible_assert_then_assume : TopLevel () +disable_crucible_profiling : TopLevel () +disable_debug_intrinsics : TopLevel () +disable_lax_arithmetic : TopLevel () +disable_lax_loads_and_stores : TopLevel () +disable_lax_pointer_ordering : TopLevel () +disable_smt_array_memory_model : TopLevel () +disable_what4_eval : TopLevel () +disable_what4_hash_consing : TopLevel () +disable_x86_what4_hash_consing : TopLevel () +dsec_print : Term -> Term -> TopLevel () +dump_file_AST : String -> TopLevel () +empty_ss : Simpset +enable_crucible_assert_then_assume : TopLevel () +enable_crucible_profiling : String -> TopLevel () +enable_debug_intrinsics : TopLevel () +enable_deprecated : TopLevel () +enable_experimental : TopLevel () +enable_lax_arithmetic : TopLevel () +enable_lax_loads_and_stores : TopLevel () +enable_lax_pointer_ordering : TopLevel () +enable_smt_array_memory_model : TopLevel () +enable_what4_hash_consing : TopLevel () +env : TopLevel () +eval_bool : Term -> Bool +eval_int : Term -> Int +eval_list : Term -> [Term] +eval_size : Type -> Int +exec : String -> [String] -> String -> TopLevel String +exit : Int -> TopLevel () +external_aig_solver : String -> [String] -> ProofScript () +external_cnf_solver : String -> [String] -> ProofScript () +fail : {a} String -> TopLevel a +fails : {a} TopLevel a -> TopLevel () +false : Bool +for : {m, a, b} [a] -> (a -> m b) -> m [b] +fresh_symbolic : String -> Type -> TopLevel Term +get_env : String -> String +get_nopts : () -> Int +get_opt : Int -> String +goal_eval : ProofScript () +goal_eval_unint : [String] -> ProofScript () +goal_num : ProofScript Int +head : {a} [a] -> a +hoist_ifs : Term -> TopLevel Term +include : String -> TopLevel () +int_to_term : Int -> Term +is_convertible : Term -> Term -> TopLevel Bool +java_array : Int -> JavaType -> JavaType +java_bool : JavaType +java_byte : JavaType +java_char : JavaType +java_class : String -> JavaType +java_double : JavaType +java_float : JavaType +java_int : JavaType +java_load_class : String -> TopLevel JavaClass +java_long : JavaType +java_short : JavaType +jvm_alloc_array : Int -> JavaType -> JVMSetup JVMValue +jvm_alloc_object : String -> JVMSetup JVMValue +jvm_array_is : JVMValue -> Term -> JVMSetup () +jvm_assert : Term -> JVMSetup () +jvm_elem_is : JVMValue -> Int -> JVMValue -> JVMSetup () +jvm_equal : JVMValue -> JVMValue -> JVMSetup () +jvm_execute_func : [JVMValue] -> JVMSetup () +jvm_extract : JavaClass -> String -> TopLevel Term +jvm_field_is : JVMValue -> String -> JVMValue -> JVMSetup () +jvm_fresh_var : String -> JavaType -> JVMSetup Term +jvm_ghost_value : Ghost -> Term -> JVMSetup () +jvm_modifies_array : JVMValue -> JVMSetup () +jvm_modifies_elem : JVMValue -> Int -> JVMSetup () +jvm_modifies_field : JVMValue -> String -> JVMSetup () +jvm_modifies_static_field : String -> JVMSetup () +jvm_null : JVMValue +jvm_postcond : Term -> JVMSetup () +jvm_precond : Term -> JVMSetup () +jvm_return : JVMValue -> JVMSetup () +jvm_static_field_is : String -> JVMValue -> JVMSetup () +jvm_term : Term -> JVMValue +jvm_unint : [String] -> JVMSetup () +jvm_unsafe_assume_spec : JavaClass -> String -> JVMSetup () -> TopLevel JVMSpec +jvm_verify : JavaClass -> String -> [JVMSpec] -> Bool -> JVMSetup () -> ProofScript () -> TopLevel JVMSpec +lambda : Term -> Term -> Term +lambdas : [Term] -> Term -> Term +length : {a} [a] -> Int +list_term : [Term] -> Term +llvm_alias : String -> LLVMType +llvm_alloc : LLVMType -> LLVMSetup SetupValue +llvm_alloc_aligned : Int -> LLVMType -> LLVMSetup SetupValue +llvm_alloc_global : String -> LLVMSetup () +llvm_alloc_readonly : LLVMType -> LLVMSetup SetupValue +llvm_alloc_readonly_aligned : Int -> LLVMType -> LLVMSetup SetupValue +llvm_array : Int -> LLVMType -> LLVMType +llvm_array_value : [SetupValue] -> SetupValue +llvm_assert : Term -> LLVMSetup () +llvm_cast_pointer : SetupValue -> LLVMType -> SetupValue +llvm_cfg : LLVMModule -> String -> TopLevel CFG +llvm_conditional_points_to : Term -> SetupValue -> SetupValue -> LLVMSetup () +llvm_conditional_points_to_at_type : Term -> SetupValue -> LLVMType -> SetupValue -> LLVMSetup () +llvm_conditional_points_to_untyped : Term -> SetupValue -> SetupValue -> LLVMSetup () +llvm_declare_ghost_state : String -> TopLevel Ghost +llvm_double : LLVMType +llvm_elem : SetupValue -> Int -> SetupValue +llvm_equal : SetupValue -> SetupValue -> LLVMSetup () +llvm_execute_func : [SetupValue] -> LLVMSetup () +llvm_extract : LLVMModule -> String -> TopLevel Term +llvm_field : SetupValue -> String -> SetupValue +llvm_float : LLVMType +llvm_fresh_expanded_val : LLVMType -> LLVMSetup SetupValue +llvm_fresh_pointer : LLVMType -> LLVMSetup SetupValue +llvm_fresh_var : String -> LLVMType -> LLVMSetup Term +llvm_ghost_value : Ghost -> Term -> LLVMSetup () +llvm_global : String -> SetupValue +llvm_global_initializer : String -> SetupValue +llvm_int : Int -> LLVMType +llvm_load_module : String -> TopLevel LLVMModule +llvm_null : SetupValue +llvm_packed_struct_type : [LLVMType] -> LLVMType +llvm_packed_struct_value : [SetupValue] -> SetupValue +llvm_pointer : LLVMType -> LLVMType +llvm_points_to : SetupValue -> SetupValue -> LLVMSetup () +llvm_points_to_at_type : SetupValue -> LLVMType -> SetupValue -> LLVMSetup () +llvm_points_to_untyped : SetupValue -> SetupValue -> LLVMSetup () +llvm_postcond : Term -> LLVMSetup () +llvm_precond : Term -> LLVMSetup () +llvm_return : SetupValue -> LLVMSetup () +llvm_sizeof : LLVMModule -> LLVMType -> Int +llvm_spec_size : LLVMSpec -> Int +llvm_spec_solvers : LLVMSpec -> [String] +llvm_struct : String -> LLVMType +llvm_struct_type : [LLVMType] -> LLVMType +llvm_struct_value : [SetupValue] -> SetupValue +llvm_symbolic_alloc : Bool -> Int -> Term -> LLVMSetup SetupValue +llvm_term : Term -> SetupValue +llvm_type : String -> LLVMType +llvm_unint : [String] -> LLVMSetup () +llvm_union : SetupValue -> String -> SetupValue +llvm_unsafe_assume_spec : LLVMModule -> String -> LLVMSetup () -> TopLevel LLVMSpec +llvm_verify : LLVMModule -> String -> [LLVMSpec] -> Bool -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec +load_aig : String -> TopLevel AIG +mathsat : ProofScript () +mir_unint : [String] -> MIRSetup () +nat_to_term : Int -> Term +nth : {a} [a] -> Int -> a +null : {a} [a] -> Bool +offline_aig : String -> ProofScript () +offline_aig_external : String -> ProofScript () +offline_cnf : String -> ProofScript () +offline_cnf_external : String -> ProofScript () +offline_extcore : String -> ProofScript () +offline_smtlib2 : String -> ProofScript () +offline_unint_smtlib2 : [String] -> String -> ProofScript () +offline_w4_unint_bitwuzla : [String] -> String -> ProofScript () +offline_w4_unint_cvc4 : [String] -> String -> ProofScript () +offline_w4_unint_cvc5 : [String] -> String -> ProofScript () +offline_w4_unint_yices : [String] -> String -> ProofScript () +offline_w4_unint_z3 : [String] -> String -> ProofScript () +parse_core : String -> Term +parse_core_mod : String -> String -> Term +parser_printer_roundtrip : String -> TopLevel () +print : {a} a -> TopLevel () +print_goal : ProofScript () +print_goal_consts : ProofScript () +print_goal_depth : Int -> ProofScript () +print_goal_inline : [Int] -> ProofScript () +print_goal_size : ProofScript () +print_goal_summary : ProofScript () +print_solver_cache : String -> TopLevel () +print_solver_cache_stats : TopLevel () +print_term : Term -> TopLevel () +print_term_depth : Int -> Term -> TopLevel () +print_type : Term -> TopLevel () +prove : ProofScript () -> Term -> TopLevel ProofResult +prove_core : ProofScript () -> String -> TopLevel Theorem +prove_extcore : ProofScript () -> Term -> TopLevel Theorem +prove_print : ProofScript () -> Term -> TopLevel Theorem +qc_print : Int -> Term -> TopLevel () +quickcheck : Int -> ProofScript () +read_aig : String -> TopLevel Term +read_bytes : String -> TopLevel Term +read_core : String -> TopLevel Term +replace : Term -> Term -> Term -> TopLevel Term +return : {m, a} a -> m a +rewrite : Simpset -> Term -> Term +rme : ProofScript () +run : {a} TopLevel a -> a +sat : ProofScript () -> Term -> TopLevel SatResult +sat_print : ProofScript () -> Term -> TopLevel () +save_aig : String -> AIG -> TopLevel () +save_aig_as_cnf : String -> AIG -> TopLevel () +sbv_abc : ProofScript () +sbv_bitwuzla : ProofScript () +sbv_boolector : ProofScript () +sbv_cvc4 : ProofScript () +sbv_cvc5 : ProofScript () +sbv_mathsat : ProofScript () +sbv_unint_bitwuzla : [String] -> ProofScript () +sbv_unint_cvc4 : [String] -> ProofScript () +sbv_unint_cvc5 : [String] -> ProofScript () +sbv_unint_yices : [String] -> ProofScript () +sbv_unint_z3 : [String] -> ProofScript () +sbv_yices : ProofScript () +sbv_z3 : ProofScript () +set_ascii : Bool -> TopLevel () +set_base : Int -> TopLevel () +set_color : Bool -> TopLevel () +set_memoization_hash : Int -> TopLevel () +set_memoization_hash_incremental : Int -> TopLevel () +set_memoization_incremental : TopLevel () +set_min_sharing : Int -> TopLevel () +set_solver_cache_path : String -> TopLevel () +set_solver_cache_timeout : Int -> TopLevel () +sharpSAT : Term -> TopLevel Integer +show : {a} a -> String +show_cfg : CFG -> String +show_term : Term -> String +simplify : Simpset -> ProofScript () +simplify_local : [Int] -> Simpset -> ProofScript () +size_to_term : Type -> Term +str_concat : String -> String -> String +str_concats : [String] -> String +tail : {a} [a] -> [a] +term_apply : Term -> [Term] -> Term +term_eval : Term -> Term +term_eval_unint : [String] -> Term -> Term +term_size : Term -> Int +term_tree_size : Term -> Int +test_solver_cache_stats : Int -> Int -> Int -> Int -> Int -> TopLevel () +time : {a} TopLevel a -> TopLevel a +trivial : ProofScript () +true : Bool +type : Term -> Type +undefined : {a} a +unfold_term : [String] -> Term -> Term +unfolding : [String] -> ProofScript () +unfolding_fix_once : [String] -> ProofScript () +unint_bitwuzla : [String] -> ProofScript () +unint_cvc4 : [String] -> ProofScript () +unint_cvc5 : [String] -> ProofScript () +unint_yices : [String] -> ProofScript () +unint_z3 : [String] -> ProofScript () +w4 : ProofScript () +w4_abc_aiger : ProofScript () +w4_abc_smtlib2 : ProofScript () +w4_abc_verilog : ProofScript () +w4_offline_smtlib2 : String -> ProofScript () +w4_unint_bitwuzla : [String] -> ProofScript () +w4_unint_cvc4 : [String] -> ProofScript () +w4_unint_cvc5 : [String] -> ProofScript () +w4_unint_rme : [String] -> ProofScript () +w4_unint_yices : [String] -> ProofScript () +w4_unint_z3 : [String] -> ProofScript () +w4_unint_z3_using : String -> [String] -> ProofScript () +with_time : {a} TopLevel a -> TopLevel (Int, a) +write_aig : String -> Term -> TopLevel () +write_aig_external : String -> Term -> TopLevel () +write_cnf : String -> Term -> TopLevel () +write_cnf_external : String -> Term -> TopLevel () +write_core : String -> Term -> TopLevel () +write_goal : String -> ProofScript () +write_saig : String -> Term -> TopLevel () +write_saig' : String -> Term -> Int -> TopLevel () +write_smtlib2 : String -> Term -> TopLevel () +write_smtlib2_w4 : String -> Term -> TopLevel () +yices : ProofScript () +z3 : ProofScript () + +y : Int diff --git a/intTests/test1646/test2.log.good b/intTests/test1646/test2.log.good deleted file mode 100644 index 6b34e90901..0000000000 --- a/intTests/test1646/test2.log.good +++ /dev/null @@ -1,8 +0,0 @@ - Loading file "test2.saw" - x=a - test2.saw:8:5-8:6: Warning: Redeclaration of x - test2.saw:3:5-3:6: Warning: Previous declaration was here - fromValue Text -CallStack (from HasCallStack): - error, called at saw-script/src/SAWScript/Interpreter.hs -FAILED diff --git a/intTests/test1646/test3.log.good b/intTests/test1646/test3.log.good deleted file mode 100644 index 8d4035fdd6..0000000000 --- a/intTests/test1646/test3.log.good +++ /dev/null @@ -1,5 +0,0 @@ - Loading file "test3.saw" - test3.saw:9:8-9:9: Warning: Redeclaration of x - test3.saw:4:8-4:9: Warning: Previous declaration was here - x=a - x=a diff --git a/intTests/test1646/test4.log.good b/intTests/test1646/test4.log.good deleted file mode 100644 index a64bdf5c47..0000000000 --- a/intTests/test1646/test4.log.good +++ /dev/null @@ -1,5 +0,0 @@ - Loading file "test4.saw" - test4.saw:9:8-9:9: Warning: Redeclaration of x - test4.saw:4:8-4:9: Warning: Previous declaration was here - x=a - x=a diff --git a/intTests/test1646/test5.log.good b/intTests/test1646/test5.log.good deleted file mode 100644 index 2aa2944713..0000000000 --- a/intTests/test1646/test5.log.good +++ /dev/null @@ -1,3 +0,0 @@ - Loading file "test5.saw" - x=a - x=b diff --git a/intTests/test1646/test6.log.good b/intTests/test1646/test6.log.good deleted file mode 100644 index e3d16fe2de..0000000000 --- a/intTests/test1646/test6.log.good +++ /dev/null @@ -1,13 +0,0 @@ - Loading file "test6.saw" - x=a - test6.saw:8:16-8:17: Type mismatch. - Mismatch of type constructors. Expected: Int but got String - test6.saw:8:20-8:21: The type Int arises from the type of this term - test6.saw:3:20-3:23: The type String arises from the type of this term - - Expected: Int - Found: String - - within "x" (test6.saw:8:16-8:17) - -FAILED diff --git a/intTests/test1646/test7.log.good b/intTests/test1646/test7.log.good deleted file mode 100644 index 8d094e0390..0000000000 --- a/intTests/test1646/test7.log.good +++ /dev/null @@ -1,8 +0,0 @@ - Loading file "test7.saw" - Type errors: - test7.saw:4:4-4:26: Invalid use of 'rebindable' - test7.saw:4:4-4:26: It is only allowed at the syntactic top level - test7.saw:9:4-9:26: Invalid use of 'rebindable' - test7.saw:9:4-9:26: It is only allowed at the syntactic top level - -FAILED diff --git a/intTests/test1646/test8.log.good b/intTests/test1646/test8.log.good deleted file mode 100644 index 8cf4e9e85a..0000000000 --- a/intTests/test1646/test8.log.good +++ /dev/null @@ -1,8 +0,0 @@ - Loading file "test8.saw" - Type errors: - test8.saw:4:4-4:26: Invalid use of 'rebindable' - test8.saw:4:4-4:26: It is only allowed at the syntactic top level - test8.saw:9:4-9:26: Invalid use of 'rebindable' - test8.saw:9:4-9:26: It is only allowed at the syntactic top level - -FAILED diff --git a/intTests/test2242_2243/README b/intTests/test2242_2243/README new file mode 100644 index 0000000000..a4872a631e --- /dev/null +++ b/intTests/test2242_2243/README @@ -0,0 +1,9 @@ +Examples from #2242 (scoping regression in proof_subshell) and #2243 +(bindings escape proof_subshell). + +It might be better to use test-and-diff.sh here so as to capture the +output; however, it doesn't work. For a TopLevel subshell, the input +for the subshell needs to be on stdin, even if you use .isaw files +with saw -B, and test-and-diff.sh can't do that. For a ProofScript +subshell, it's even worse: for some reason one gets "Proof subshells +not supported". diff --git a/intTests/test2242_2243/leak01.saw b/intTests/test2242_2243/leak01.saw new file mode 100644 index 0000000000..c3a1488c8d --- /dev/null +++ b/intTests/test2242_2243/leak01.saw @@ -0,0 +1,10 @@ +// Example of plain subshell leaking a binding from #2243 + +enable_experimental; + +let f () = do { subshell (); print "(exit)"; return (); }; +let x = 3; +f (); +print "should be 3"; +print x; +prove_print z3 {{ `x == 3 }}; diff --git a/intTests/test2242_2243/leak01.stdin b/intTests/test2242_2243/leak01.stdin new file mode 100644 index 0000000000..08f32c2eef --- /dev/null +++ b/intTests/test2242_2243/leak01.stdin @@ -0,0 +1 @@ +let x = 5 diff --git a/intTests/test2242_2243/leak02.saw b/intTests/test2242_2243/leak02.saw new file mode 100644 index 0000000000..3d292f0a55 --- /dev/null +++ b/intTests/test2242_2243/leak02.saw @@ -0,0 +1,11 @@ +// Proof subshell analogue of leak01 + +enable_experimental; + +let f () = do { proof_subshell (); let _ = run (print "(exit)"); return (); }; +let x = 3; +prove_print (f ()) {{ `x == 3 }}; + +print "should be 3"; +print x; +prove_print z3 {{ `x == 3 }}; diff --git a/intTests/test2242_2243/leak02.stdin b/intTests/test2242_2243/leak02.stdin new file mode 100644 index 0000000000..ac23298015 --- /dev/null +++ b/intTests/test2242_2243/leak02.stdin @@ -0,0 +1,2 @@ +let x = 5 +z3 diff --git a/intTests/test2242_2243/leak03.saw b/intTests/test2242_2243/leak03.saw new file mode 100644 index 0000000000..a22c3d1c06 --- /dev/null +++ b/intTests/test2242_2243/leak03.saw @@ -0,0 +1,20 @@ +// Example from #2243 using the Cryptol scope. + +enable_experimental; + +let foo () = do { + prove_print do { + proof_subshell (); + let _ = run (print {{ quack }}); + return (); + } {{ True }}; +}; + +let bar () = do { + print {{ quack }}; +}; + +print "this should print 3"; +foo (); +print "this should fail"; +fails (bar ()); diff --git a/intTests/test2242_2243/leak03.stdin b/intTests/test2242_2243/leak03.stdin new file mode 100644 index 0000000000..447452620f --- /dev/null +++ b/intTests/test2242_2243/leak03.stdin @@ -0,0 +1,2 @@ +let quack = {{ 3 : [8] }} +trivial diff --git a/intTests/test2242_2243/present01.saw b/intTests/test2242_2243/present01.saw new file mode 100644 index 0000000000..8f91a449cb --- /dev/null +++ b/intTests/test2242_2243/present01.saw @@ -0,0 +1,13 @@ +// TopLevel analogue of present02. +// +// The stdin file feeds f () to subshell; if f is missing from +// the nested environment that won't work. + +enable_experimental; + +let foo (x : Integer) : TopLevel () = do { + let f () = print x; + subshell (); +}; + +foo 5; diff --git a/intTests/test2242_2243/present01.stdin b/intTests/test2242_2243/present01.stdin new file mode 100644 index 0000000000..39270e49c8 --- /dev/null +++ b/intTests/test2242_2243/present01.stdin @@ -0,0 +1 @@ +f () diff --git a/intTests/test2242_2243/present02.saw b/intTests/test2242_2243/present02.saw new file mode 100644 index 0000000000..1ce098a2f3 --- /dev/null +++ b/intTests/test2242_2243/present02.saw @@ -0,0 +1,16 @@ +// Simple example akin to the failure case from #2242. +// +// The stdin file feeds f () to proof_subshell; if f is missing from +// the nested environment that won't work. + +enable_experimental; + +let foo (x : Integer) : TopLevel Theorem = do { + let f () = z3; + + prove_print do { + proof_subshell (); + } {{ `x == 5 }}; +}; + +foo 5; diff --git a/intTests/test2242_2243/present02.stdin b/intTests/test2242_2243/present02.stdin new file mode 100644 index 0000000000..39270e49c8 --- /dev/null +++ b/intTests/test2242_2243/present02.stdin @@ -0,0 +1 @@ +f () diff --git a/intTests/test2242_2243/test.sh b/intTests/test2242_2243/test.sh new file mode 100644 index 0000000000..8f4083c91a --- /dev/null +++ b/intTests/test2242_2243/test.sh @@ -0,0 +1,8 @@ +set -e + +$SAW present01.saw < present01.stdin +$SAW present02.saw < present02.stdin + +$SAW leak01.saw < leak01.stdin +$SAW leak02.saw < leak02.stdin +$SAW leak03.saw < leak03.stdin diff --git a/intTests/test2304/.gitignore b/intTests/test2304/.gitignore new file mode 100644 index 0000000000..4619758def --- /dev/null +++ b/intTests/test2304/.gitignore @@ -0,0 +1,3 @@ +*.rawlog +*.log +*.diff diff --git a/intTests/test2304/Makefile b/intTests/test2304/Makefile new file mode 100644 index 0000000000..c9e12c62ae --- /dev/null +++ b/intTests/test2304/Makefile @@ -0,0 +1,5 @@ +all: ; +clean: + sh ./test.sh clean + +.PHONY: all clean diff --git a/intTests/test2304/test.sh b/intTests/test2304/test.sh new file mode 100644 index 0000000000..5fcd79d0a6 --- /dev/null +++ b/intTests/test2304/test.sh @@ -0,0 +1 @@ +exec ${TEST_SHELL:-bash} ../support/test-and-diff.sh "$@" diff --git a/intTests/test2304/test01.log.good b/intTests/test2304/test01.log.good new file mode 100644 index 0000000000..bd786801af --- /dev/null +++ b/intTests/test2304/test01.log.good @@ -0,0 +1,4 @@ + Loading file "test01.saw" + test01.saw:4:11-4:12: Warning: Redeclaration of x + test01.saw:2:8-2:9: Warning: Previous declaration was here + True diff --git a/intTests/test2304/test01.saw b/intTests/test2304/test01.saw new file mode 100644 index 0000000000..2a2bf41b03 --- /dev/null +++ b/intTests/test2304/test01.saw @@ -0,0 +1,8 @@ +do { + let x = {{ 3 : [8] }}; + do { + let x = {{ 4 : Integer }}; + return (); + }; + print {{ x == (3 : [8]) }}; +}; diff --git a/intTests/test2304/test02.log.good b/intTests/test2304/test02.log.good new file mode 100644 index 0000000000..9bb9092f09 --- /dev/null +++ b/intTests/test2304/test02.log.good @@ -0,0 +1,2 @@ + Loading file "test02.saw" + True diff --git a/intTests/test2304/test02.saw b/intTests/test2304/test02.saw new file mode 100644 index 0000000000..25c5ba1260 --- /dev/null +++ b/intTests/test2304/test02.saw @@ -0,0 +1,8 @@ +do { + let {{ x = 3 : [8] }}; + do { + let {{ x = 4 : Integer }}; + return (); + }; + print {{ x == (3 : [8]) }}; +}; diff --git a/intTests/test2304/test03.log.good b/intTests/test2304/test03.log.good new file mode 100644 index 0000000000..aa90314754 --- /dev/null +++ b/intTests/test2304/test03.log.good @@ -0,0 +1,3 @@ + Loading file "test03.saw" + Attempted to register the following name twice: cryptol:x#4785 +FAILED diff --git a/intTests/test2304/test03.saw b/intTests/test2304/test03.saw new file mode 100644 index 0000000000..bcdd08fd69 --- /dev/null +++ b/intTests/test2304/test03.saw @@ -0,0 +1,12 @@ +do { + let {{ x = 3 : [8] }}; + do { + let {{ x = 4 : Integer }}; + return (); + }; + do { + let {{ x = 5 : Integer }}; + return (); + }; + print {{ x == (3 : [8]) }}; +}; diff --git a/intTests/test2304/test04.log.good b/intTests/test2304/test04.log.good new file mode 100644 index 0000000000..86278ed34e --- /dev/null +++ b/intTests/test2304/test04.log.good @@ -0,0 +1,7 @@ + Loading file "test04.saw" + ("a",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 3) u1218 _P) + ("b",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 4) u1218 _P) + ("c",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 5) u1218 _P) diff --git a/intTests/test2304/test04.saw b/intTests/test2304/test04.saw new file mode 100644 index 0000000000..e6cc34ccdf --- /dev/null +++ b/intTests/test2304/test04.saw @@ -0,0 +1,12 @@ +let f (x: Integer) = {{ `x }}; +let g (x: Integer) = return {{ `x }}; +let h (x: Integer) = do { return {{ `x }}; }; + +let a = f 3; +print ("a", a); + +b <- g 4; +print ("b", b); + +c <- h 5; +print ("c", c); diff --git a/intTests/test2304/test05.log.good b/intTests/test2304/test05.log.good new file mode 100644 index 0000000000..2b3f0fcc58 --- /dev/null +++ b/intTests/test2304/test05.log.good @@ -0,0 +1,7 @@ + Loading file "test05.saw" + ("a",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 3) u1218 _P) + ("b",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 4) u1218 _P) + ("c",\(u1218 : isort 0) -> + \(_P : PLiteral u1218) -> ecNumber (TCNum 5) u1218 _P) diff --git a/intTests/test2304/test05.saw b/intTests/test2304/test05.saw new file mode 100644 index 0000000000..acb881f5f0 --- /dev/null +++ b/intTests/test2304/test05.saw @@ -0,0 +1,12 @@ +let f (x: Integer) (y: Integer) = {{ `x }}; +let g (x: Integer) (y: Integer) = return {{ `x }}; +let h (x: Integer) (y: Integer) = do { return {{ `x }}; }; + +let a = f 3 6; +print ("a", a); + +b <- g 4 7; +print ("b", b); + +c <- h 5 8; +print ("c", c); diff --git a/intTests/test_sawscript_builtins/undefined7.log.good b/intTests/test_sawscript_builtins/undefined7.log.good index 0b8d0d1ff0..cdbeb877c9 100644 --- a/intTests/test_sawscript_builtins/undefined7.log.good +++ b/intTests/test_sawscript_builtins/undefined7.log.good @@ -1,5 +1,4 @@ Loading file "undefined7.saw" - not dead yet interpret: undefined CallStack (from HasCallStack): error, called at saw-script/src/SAWScript/Interpreter.hs diff --git a/intTests/test_sawscript_builtins/undefined7.saw b/intTests/test_sawscript_builtins/undefined7.saw index 3983f0a14b..fbc884bfee 100644 --- a/intTests/test_sawscript_builtins/undefined7.saw +++ b/intTests/test_sawscript_builtins/undefined7.saw @@ -1,15 +1,7 @@ -// This currently doesn't crash unless you execute m. -// -// This is somewhat unexpected, as in theory it should trip on -// undefined evaluating the right hand side of "let m" in -// interpretExpr... or having not done so, file x in the environment -// and then never see it again and not crash at all. -// -// For the time being I'm going to let this pass as an acceptable -// weirdness, and with luck it'll change when other things in the -// interpreter get cleaned up. +// This crashes when m is bound. It will eval until it gets to +// the do-block, and that trips on the undefined. let m = let x = undefined in do { return (); }; -print "not dead yet"; -m; print "oops didn't die"; +m; +print "oops still didn't die"; diff --git a/intTests/test_sawscript_builtins/undefined8.log.good b/intTests/test_sawscript_builtins/undefined8.log.good new file mode 100644 index 0000000000..75aa39b6be --- /dev/null +++ b/intTests/test_sawscript_builtins/undefined8.log.good @@ -0,0 +1,5 @@ + Loading file "undefined8.saw" + interpret: undefined +CallStack (from HasCallStack): + error, called at saw-script/src/SAWScript/Interpreter.hs +FAILED diff --git a/intTests/test_sawscript_builtins/undefined8.saw b/intTests/test_sawscript_builtins/undefined8.saw new file mode 100644 index 0000000000..9c2974d611 --- /dev/null +++ b/intTests/test_sawscript_builtins/undefined8.saw @@ -0,0 +1,6 @@ +// This crashes immediately. + +let y = let x = undefined in (); +print "oops didn't die"; +print y; +print "oops still didn't die"; diff --git a/intTests/test_sawscript_builtins/undefined9.log.good b/intTests/test_sawscript_builtins/undefined9.log.good new file mode 100644 index 0000000000..536b0de089 --- /dev/null +++ b/intTests/test_sawscript_builtins/undefined9.log.good @@ -0,0 +1,5 @@ + Loading file "undefined9.saw" + interpret: undefined +CallStack (from HasCallStack): + error, called at saw-script/src/SAWScript/Interpreter.hs +FAILED diff --git a/intTests/test_sawscript_builtins/undefined9.saw b/intTests/test_sawscript_builtins/undefined9.saw new file mode 100644 index 0000000000..27d92c77cb --- /dev/null +++ b/intTests/test_sawscript_builtins/undefined9.saw @@ -0,0 +1,5 @@ +// This crashes immediately. + +let y = let x = undefined in return (); +print "oops didn't die"; + diff --git a/saw-central/src/SAWCentral/ASTUtil.hs b/saw-central/src/SAWCentral/ASTUtil.hs index ab1a5857f8..05b315e8ef 100644 --- a/saw-central/src/SAWCentral/ASTUtil.hs +++ b/saw-central/src/SAWCentral/ASTUtil.hs @@ -3,6 +3,7 @@ module SAWCentral.ASTUtil ( namedTyVars, SubstituteTyVars(..), + SubstituteTyVars'(..), isDeprecated ) where @@ -12,6 +13,9 @@ import qualified Data.Set as Set import Data.Map (Map) import qualified Data.Map as Map +import qualified SAWSupport.ScopedMap as ScopedMap +import SAWSupport.ScopedMap (ScopedMap) + import SAWCentral.Panic import SAWCentral.Position import SAWCentral.AST @@ -66,10 +70,10 @@ instance NamedTyVars Schema where -- class SubstituteTyVars t where - -- | @substituteTyVars m x@ applies the map @m@ to type variables in @x@. + -- | @substituteTyVars m x@ applies the (scoped) map @m@ to type variables in @x@. substituteTyVars :: Set PrimitiveLifecycle -> - Map Name (PrimitiveLifecycle, NamedType) -> + ScopedMap Name (PrimitiveLifecycle, NamedType) -> t -> t instance (SubstituteTyVars a) => SubstituteTyVars (Maybe a) where @@ -84,7 +88,7 @@ instance SubstituteTyVars Type where TyRecord pos fs -> TyRecord pos (fmap (substituteTyVars avail tyenv) fs) TyUnifyVar _ _ -> ty TyVar _ n -> - case Map.lookup n tyenv of + case ScopedMap.lookup n tyenv of Nothing -> ty Just (lc, expansion) -> if not (Set.member lc avail) then @@ -96,6 +100,44 @@ instance SubstituteTyVars Type where AbstractType -> ty ConcreteType ty' -> ty' +-- +-- The prime version uses an ordinary map. +-- +-- This is used by the typechecker for the time being until the +-- typechecker gets taught to use ScopedMap. +-- + +class SubstituteTyVars' t where + -- | @substituteTyVars' m x@ applies the (ordinary) map @m@ to type variables in @x@. + substituteTyVars' :: + Set PrimitiveLifecycle -> + Map Name (PrimitiveLifecycle, NamedType) -> + t -> t + +instance (SubstituteTyVars' a) => SubstituteTyVars' (Maybe a) where + substituteTyVars' avail tyenv = fmap (substituteTyVars' avail tyenv) + +instance (SubstituteTyVars' a) => SubstituteTyVars' [a] where + substituteTyVars' avail tyenv = map (substituteTyVars' avail tyenv) + +instance SubstituteTyVars' Type where + substituteTyVars' avail tyenv ty = case ty of + TyCon pos tc ts -> TyCon pos tc (substituteTyVars' avail tyenv ts) + TyRecord pos fs -> TyRecord pos (fmap (substituteTyVars' avail tyenv) fs) + TyUnifyVar _ _ -> ty + TyVar _ n -> + case Map.lookup n tyenv of + Nothing -> ty + Just (lc, expansion) -> + if not (Set.member lc avail) then + panic "substituteTyVars'" [ + "Found reference to non-visible typedef: " <> n, + "Lifecycle setting: " <> Text.pack (show lc) + ] + else case expansion of + AbstractType -> ty + ConcreteType ty' -> ty' + -- }}} diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index d19babe325..ddf33518a7 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -31,7 +31,7 @@ import qualified Control.Exception as Ex import qualified Data.ByteString as StrictBS import qualified Data.ByteString.Lazy as BS import qualified Data.IntMap as IntMap -import Data.List (isPrefixOf, isInfixOf, sort) +import Data.List (isPrefixOf, isInfixOf, sort, intersperse) import qualified Data.Map as Map import Data.Parameterized.Classes (KnownRepr(..)) import Data.Set (Set) @@ -60,6 +60,8 @@ import qualified CryptolSAWCore.Cryptol as Cryptol import qualified CryptolSAWCore.Simpset as Cryptol -- saw-support +import qualified SAWSupport.ScopedMap as ScopedMap +--import SAWSupport.ScopedMap (ScopedMap) import qualified SAWSupport.Pretty as PPS (MemoStyle(..), Opts(..), pShowText) -- saw-core @@ -558,7 +560,7 @@ resolveNameIO sc cenv nm = -- exception is thrown. resolveName :: SharedContext -> Text -> TopLevel [VarIndex] resolveName sc nm = - do cenv <- rwCryptol <$> getTopLevelRW + do cenv <- SV.getCryptolEnv scnms <- io (resolveNameIO sc cenv nm) case scnms of [] -> fail $ Text.unpack $ "Could not resolve name: " <> nm @@ -1590,7 +1592,7 @@ check_term :: TypedTerm -> TopLevel () check_term tt = do sc <- getSharedContext opts <- getTopLevelPPOpts - cenv <- rwCryptol <$> getTopLevelRW + cenv <- SV.getCryptolEnv let t = ttTerm tt ty <- io $ scTypeCheckError sc t expectedTy <- @@ -1700,14 +1702,32 @@ cexEvalFn sc args tm = do envCmd :: TopLevel () envCmd = do - rw <- SV.getMergedEnv - let avail = rwPrimsAvail rw - vals = rwValueInfo rw - keep (_x, (_pos, lc, _rb, _ty, _v, _doc)) = Set.member lc avail - vals' = filter keep $ Map.assocs vals - printit (x, (_pos, _lc, _rb, ty, _v, _doc)) = x <> " : " <> PPS.pShowText ty opts <- getOptions - io $ sequence_ [ printOutLn opts Info (Text.unpack $ printit item) | item <- vals' ] + avail <- gets rwPrimsAvail + SV.Environ varenv _tyenv _cryenv <- gets rwEnviron + rbenv <- gets rwRebindables + + -- print rebindables first if there are any + unless (Map.null rbenv) $ do + io $ printOutLn opts Info $ "Rebindable globals:" + io $ printOutLn opts Info $ "" + let printRB (x, (_pos, ty, _v)) = do + let str = x <> " : rebindable " <> PPS.pShowText ty + printOutLn opts Info $ Text.unpack str + io $ mapM_ printRB $ Map.assocs rbenv + + let printItem (x, (_pos, _lc, ty, _v, _doc)) = + printOutLn opts Info $ Text.unpack (x <> " : " <> PPS.pShowText ty) + -- Print only the visible objects + keep (_x, (_pos, lc, _ty, _v, _doc)) = Set.member lc avail + -- Insert a blank line in the output where there's a scope boundary + printScope mItems = case mItems of + Nothing -> printOutLn opts Info "" + Just items -> mapM_ printItem $ filter keep items + -- Reverse the list of scopes so the innermost prints last, + -- because that's what people will expect to see. + itemses = reverse $ ScopedMap.scopedAssocs varenv + io $ mapM_ printScope $ intersperse Nothing $ map Just itemses exitPrim :: Integer -> IO () exitPrim code = Exit.exitWith exitCode @@ -1766,7 +1786,7 @@ eval_bool t = do eval_int :: TypedTerm -> TopLevel Integer eval_int t = do sc <- getSharedContext - cenv <- fmap rwCryptol getTopLevelRW + cenv <- SV.getCryptolEnv let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv) unless (null (getAllExts (ttTerm t))) $ fail "term contains symbolic variables" @@ -1825,7 +1845,7 @@ term_theories unints t = do default_typed_term :: TypedTerm -> TopLevel TypedTerm default_typed_term tt = do sc <- getSharedContext - cenv <- fmap rwCryptol getTopLevelRW + cenv <- SV.getCryptolEnv let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv) opts <- getOptions io $ defaultTypedTerm opts sc cfg tt @@ -2074,64 +2094,62 @@ cryptol_prims = parsePrim :: (Text, Ident, Text) -> TopLevel (C.Name, TypedTerm) parsePrim (n, i, s) = do sc <- getSharedContext - rw <- getTopLevelRW - let cenv = rwCryptol rw + SV.CryptolEnvStack cenv cenvs <- SV.getCryptolEnvStack + unless (null cenvs) $ do + fail "cryptol_prims is an import operation and may not be done in a nested block" let mname = C.packModName ["Prims"] let ?fileReader = StrictBS.readFile (n', cenv') <- io $ CEnv.declareName cenv mname n s' <- io $ CEnv.parseSchema cenv' (noLoc s) t' <- io $ scGlobalDef sc i - putTopLevelRW $ rw { rwCryptol = cenv' } + SV.setCryptolEnv cenv' return (n', TypedTerm (TypedTermSchema s') t') cryptol_load :: (FilePath -> IO StrictBS.ByteString) -> FilePath -> TopLevel CEnv.ExtCryptolModule cryptol_load fileReader path = do sc <- getSharedContext - rw <- getTopLevelRW - let ce = rwCryptol rw + SV.CryptolEnvStack ce ces <- SV.getCryptolEnvStack + unless (null ces) $ do + fail "cryptol_load is an import operation and is not permitted in nested blocks" let ?fileReader = fileReader (m, ce') <- io $ CEnv.loadExtCryptolModule sc ce path - putTopLevelRW $ rw { rwCryptol = ce' } + SV.setCryptolEnv ce' return m cryptol_extract :: CEnv.ExtCryptolModule -> Text -> TopLevel TypedTerm cryptol_extract ecm var = do sc <- getSharedContext - rw <- getTopLevelRW - let ce = rwCryptol rw + ce <- SV.getCryptolEnv let ?fileReader = StrictBS.readFile io $ CEnv.extractDefFromExtCryptolModule sc ce ecm var +-- XXX: This is kind of a top-level style operation; should it be +-- prohibited in nested scopes? (Note that while we could update the +-- whole stack of Cryptol environments here, so the operation escapes +-- the current scope, we won't be able to hunt down and update copies +-- of the environment closed in with lambdas and do-blocks, so that's +-- probably a bad idea.) cryptol_add_path :: FilePath -> TopLevel () -cryptol_add_path path = - do rw <- getTopLevelRW - let ce = rwCryptol rw +cryptol_add_path path = do + ce <- SV.getCryptolEnv let me = CEnv.eModuleEnv ce let me' = me { C.meSearchPath = path : C.meSearchPath me } let ce' = ce { CEnv.eModuleEnv = me' } - let rw' = rw { rwCryptol = ce' } - putTopLevelRW rw' + SV.setCryptolEnv ce' cryptol_add_prim :: Text -> Text -> TypedTerm -> TopLevel () -cryptol_add_prim mnm nm trm = - do rw <- getTopLevelRW - let env = rwCryptol rw - let prim_name = - C.PrimIdent (C.textToModName mnm) nm - let env' = - env { CEnv.ePrims = - Map.insert prim_name (ttTerm trm) (CEnv.ePrims env) } - putTopLevelRW (rw { rwCryptol = env' }) +cryptol_add_prim mnm nm trm = do + ce <- SV.getCryptolEnv + let prim_name = C.PrimIdent (C.textToModName mnm) nm + prims' = Map.insert prim_name (ttTerm trm) (CEnv.ePrims ce) + SV.setCryptolEnv $ ce { CEnv.ePrims = prims' } cryptol_add_prim_type :: Text -> Text -> TypedTerm -> TopLevel () -cryptol_add_prim_type mnm nm tp = - do rw <- getTopLevelRW - let env = rwCryptol rw - let prim_name = - C.PrimIdent (C.textToModName mnm) nm - let env' = env { CEnv.ePrimTypes = - Map.insert prim_name (ttTerm tp) (CEnv.ePrimTypes env) } - putTopLevelRW (rw { rwCryptol = env' }) +cryptol_add_prim_type mnm nm tp = do + ce <- SV.getCryptolEnv + let prim_name = C.PrimIdent (C.textToModName mnm) nm + prim_types' = Map.insert prim_name (ttTerm tp) (CEnv.ePrimTypes ce) + SV.setCryptolEnv $ ce { CEnv.ePrimTypes = prim_types' } -- | Call 'Cryptol.importSchema' using a 'CEnv.CryptolEnv' importSchemaCEnv :: SharedContext -> CEnv.CryptolEnv -> Cryptol.Schema -> diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs index bbf490c314..33a7a1f843 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs @@ -484,18 +484,13 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = -- XXX could have a real position... let pos = PosInternal "llvm_compositional_extract" typed_extracted_func_const <- io $ mkTypedTerm shared_context extracted_func_const - rw <- getTopLevelRW - rw' <- - liftIO $ - extendEnv shared_context + extendEnv pos func_name ReadOnlyVar (tMono $ tTerm pos) Nothing -- FUTURE: slot for doc string, could put something here (VTerm typed_extracted_func_const) - rw - putTopLevelRW rw' let lemmaSet = Set.fromList (map (view MS.psSpecIdent) lemmas') diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs index dbea5dfa93..045b13f240 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs @@ -437,6 +437,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec opts <- getOptions basic_ss <- getBasicSS rw <- getTopLevelRW + cenv <- getCryptolEnv sym <- liftIO $ newSAWCoreExprBuilder sc False mdMap <- liftIO $ newIORef mempty SomeOnlineBackend bak <- liftIO $ @@ -458,7 +459,6 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec halloc <- getHandleAlloc let mvar = C.LLVM.llvmMemVar . view C.LLVM.transContext $ modTrans llvmModule sfs <- liftIO $ Macaw.newSymFuns sym - let cenv = rwCryptol rw liftIO $ sawRegisterSymFunInterp sawst (Macaw.fnAesEnc sfs) $ cryptolUninterpreted path nm cenv "aesenc" liftIO $ sawRegisterSymFunInterp sawst (Macaw.fnAesEncLast sfs) $ cryptolUninterpreted path nm cenv "aesenclast" liftIO $ sawRegisterSymFunInterp sawst (Macaw.fnAesDec sfs) $ cryptolUninterpreted path nm cenv "aesdec" diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs index 8fc4236b52..ad63d94458 100644 --- a/saw-central/src/SAWCentral/Value.hs +++ b/saw-central/src/SAWCentral/Value.hs @@ -51,18 +51,36 @@ module SAWCentral.Value ( showsPrecValue, -- used by SAWCentral.Builtins, SAWScript.Interpreter evaluateTypedTerm, - -- used by SAWScript.Interpreter (and in LocalEnv) - LocalBinding(..), - -- used by SAWScript.Interpreter, and appears in TopLevelRO - LocalEnv, - -- used by SAWScript.Interpreter, and in mergeLocalEnv - addTypedef, - -- used by SAWScript.REPL.Monad, and by getMergedEnv - mergeLocalEnv, - -- used by SAWCentral.Builtins, SAWScript.Interpreter, and by getCryptolEnv - getMergedEnv, getMergedEnv', - -- used by SAWCentral.Crucible.LLVM.FFI + -- used by SAWScript.Search, SAWScript.Typechecker + TyEnv, VarEnv, + -- used by SAWCentral.Builtins, SAWScript.ValueOps, SAWScript.Interpreter, + -- SAWScript.REPL.Command, SAWScript.REPL.Monad, SAWServer.SAWServer + Environ(..), + -- used by SAWScript.Interpreter + pushScope, popScope, + -- used by SAWCentral.Builtins, SAWScript.ValueOps, SAWScript.Interpreter, + -- SAWServer.SAWServer + CryptolEnvStack(..), + -- used by SAWCentral.Crucible.LLVM.FFI, SAWCentral.Crucible.LLVM.X86, + -- SAWCentral.Crucible.MIR.Builtins, SAWCentral.Builtins, + -- SAWScript.Interpreter, SAWScript.REPL.Monad getCryptolEnv, + -- used by SAWCentral.Builtins + getCryptolEnvStack, + -- used by SAWCentral.Builtins, SAWScript.Interpreter, SAWScript.REPL.Monad + setCryptolEnv, + -- used by SAWScript.REPL.Monad, SAWServer.Eval, + -- SAWServer.ProofScript, SAWServer.CryptolSetup, SAWServer.CryptolExpression, + -- SAWServer.LLVMVerify, SAWServer.JVMVerify, SAWServer.MIRVerify, SAWServer.Yosys, + rwGetCryptolEnv, + -- used by SAWScript.ValueOps + rwGetCryptolEnvStack, + -- used by SAWServer.CryptolSetup + rwSetCryptolEnv, + -- used by SAWScript.ValueOps + rwSetCryptolEnvStack, + -- used by SAWScript.REPL.Monad, SAWServer.SAWServer, SAWServer.Yosys + rwModifyCryptolEnv, -- used by SAWScript.Automatch, SAWScript.REPL.*, SAWScript.Interpreter, -- SAWServer.SAWServer TopLevelRO(..), @@ -85,8 +103,6 @@ module SAWCentral.Value ( pushTraceFrames, popTraceFrames, -- used by SAWScript.Interpreter RefChain, - -- used by SAWScript.Interpreter plus appears in getMergedEnv - getLocalEnv, -- used in various places in SAWCentral, and in selected builtins in -- SAWScript.Interpreter getPosition, @@ -133,8 +149,10 @@ module SAWCentral.Value ( -- used by SAWCentral.Crucible.LLVM.Builtins, SAWScript.Interpreter -- ... the use in LLVM is the abusive insertion done by llvm_compositional_extract -- XXX: we're going to need to clean that up - -- (also appears in mergeLocalEnv) extendEnv, + extendEnvMulti, + -- used by SAWScript.Interpreter + addTypedef, -- used by various places in SAWCentral.Crucible, SAWCentral.Builtins -- XXX: it wraps TopLevel rather than being part of it; is that necessary? CrucibleSetup, @@ -203,7 +221,6 @@ import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad.Reader (ReaderT(..), ask, asks) import Control.Monad.State (StateT(..), MonadState(..), gets, modify) import Control.Monad.Trans.Class (MonadTrans(lift)) -import Data.Foldable(foldrM) import Data.List.Extra ( dropEnd ) import qualified Data.Map as M import Data.Map ( Map ) @@ -218,8 +235,11 @@ import System.FilePath(()) import qualified Data.AIG as AIG +import qualified SAWSupport.ScopedMap as ScopedMap +import SAWSupport.ScopedMap (ScopedMap) import qualified SAWSupport.Pretty as PPS (Opts, defaultOpts, showBrackets, showBraces, showCommaSep) +import SAWCentral.Panic (panic) import SAWCentral.Trace (Trace) import qualified SAWCentral.Trace as Trace @@ -499,7 +519,7 @@ data Value | VArray [Value] | VTuple [Value] | VRecord (Map SS.Name Value) - | VLambda LocalEnv (Maybe SS.Name) SS.Pattern SS.Expr + | VLambda Environ (Maybe SS.Name) SS.Pattern SS.Expr -- | Function-shaped value that's a Haskell-level function. This -- is how builtins appear. Includes the name of the builtin and -- the list of arguments applied so far, as a Seq to allow @@ -513,7 +533,7 @@ data Value -- | Returned value in unspecified monad. | VReturn SS.Pos RefChain Value -- | Not-yet-executed do-block in unspecified monad. - | VDo RefChain LocalEnv ([SS.Stmt], SS.Expr) + | VDo RefChain Environ ([SS.Stmt], SS.Expr) -- | Single monadic bind in unspecified monad. -- -- This exists only to support the "for" builtin; see notes there @@ -736,60 +756,177 @@ evaluateTypedTerm _sc (TypedTerm tp _) = -- TopLevel Monad -------------------------------------------------------------- --- | Entry in the interpreter's local (as opposed to global) variable --- environment. --- --- The Maybe [Text] field is the help text for the value, if any. --- Note that currently there's no way I know of to actually provide --- help text for a local variable, nor is there any way to get at --- one with the REPL :help command to print it, but the interpreter's --- plumbing demands that the field exist... --- -data LocalBinding - = LocalLet SS.Pos SS.Name SS.Rebindable SS.Schema (Maybe [Text]) Value - | LocalTypedef SS.Name SS.Type - deriving (Show) - -type LocalEnv = [LocalBinding] +-- | The variable environment: a map from variable names to: +-- - the definition position +-- - the lifecycle setting (experimental/current/deprecated/etc) +-- - the type scheme +-- - the value +-- - the help text if any +type VarEnv = ScopedMap SS.Name (SS.Pos, SS.PrimitiveLifecycle, + SS.Schema, Value, Maybe [Text]) --- Note that the expansion type should have already been through the --- typechecker, so it's ok to panic if it turns out to be broken. -addTypedef :: SS.Name -> SS.Type -> TopLevelRW -> TopLevelRW -addTypedef name ty rw = - let primsAvail = rwPrimsAvail rw - typeInfo = rwTypeInfo rw - ty' = SS.substituteTyVars primsAvail typeInfo ty - typeInfo' = M.insert name (SS.Current, SS.ConcreteType ty') typeInfo - in - rw { rwTypeInfo = typeInfo' } - -mergeLocalEnv :: SharedContext -> LocalEnv -> TopLevelRW -> IO TopLevelRW -mergeLocalEnv sc env rw = foldrM addBinding rw env - where addBinding (LocalLet pos x rb ty md v) = extendEnv sc pos x rb ty md v - addBinding (LocalTypedef n ty) = pure . addTypedef n ty - --- XXX: it is not sane to both be in the TopLevel monad and return a TopLevelRW --- (especially since the one returned is specifically not the same as the one --- in the monad state) -getMergedEnv :: TopLevel TopLevelRW -getMergedEnv = - do sc <- getSharedContext - env <- getLocalEnv - rw <- getTopLevelRW - liftIO $ mergeLocalEnv sc env rw +-- | The type environment: a map from type names to: +-- - the lifecycle setting (experimental/current/deprecated/etc) +-- - the expansion, which might be another type (this is how +-- typedefs/type aliases appear) or "abstract" (this is how +-- builtin types that aren't special cases in the AST appear) +type TyEnv = ScopedMap SS.Name (SS.PrimitiveLifecycle, SS.NamedType) --- Variant of getMergedEnv that takes an explicit local part --- (this avoids trying to use it with withLocalEnv, which doesn't work) -getMergedEnv' :: LocalEnv -> TopLevel TopLevelRW -getMergedEnv' env = do - sc <- getSharedContext - rw <- getTopLevelRW - liftIO $ mergeLocalEnv sc env rw +-- | The full Cryptol environment. We maintain a stack of plain +-- Cryptol environments and push/pop them as we enter and leave +-- scopes; otherwise the Cryptol environment doesn't track SAWScript +-- scopes and horribly confusing wrong things happen. +data CryptolEnvStack = CryptolEnvStack CEnv.CryptolEnv [CEnv.CryptolEnv] +-- | Type for the ordinary interpreter environment. +-- +-- There's one environment that maps variable names to values, and +-- one that maps type names to types. A third handles the Cryptol +-- domain. All three get closed in with lambdas and do-blocks at the +-- appropriate times. +-- +-- Note that rebindable variables are sold separately. This is so +-- they don't get closed in; references to rebindable variables +-- always retrieve the most recent version. +data Environ = Environ { + eVarEnv :: VarEnv, + eTyEnv :: TyEnv, + eCryptol :: CryptolEnvStack +} + +-- | The extra environment for rebindable globals. +-- +-- Note: because no builtins are rebindable, there are no lifecycle +-- or help text fields. There is, currently at least, no way to +-- populate those for non-builtins. +type RebindableEnv = Map SS.Name (SS.Pos, SS.Schema, Value) + +-- | Enter a scope. +pushScope :: TopLevel () +pushScope = do + Environ varenv tyenv cryenv <- gets rwEnviron + let varenv' = ScopedMap.push varenv + tyenv' = ScopedMap.push tyenv + cryenv' = cryptolPush cryenv + modifyTopLevelRW (\rw -> rw { rwEnviron = Environ varenv' tyenv' cryenv' }) + +-- | Leave a scope. This will panic if you try to leave the last scope; +-- pushes and pops should be matched. +popScope :: TopLevel () +popScope = do + Environ varenv tyenv cryenv <- gets rwEnviron + let varenv' = ScopedMap.pop varenv + tyenv' = ScopedMap.pop tyenv + cryenv' = cryptolPop cryenv + modifyTopLevelRW (\rw -> rw { rwEnviron = Environ varenv' tyenv' cryenv' }) + + +-- | Get the current Cryptol environment. getCryptolEnv :: TopLevel CEnv.CryptolEnv getCryptolEnv = do - env <- getMergedEnv - return $ rwCryptol env + Environ _varenv _tyenv cryenvs <- gets rwEnviron + let CryptolEnvStack ce _ = cryenvs + return ce + +-- | Get the current full stack of Cryptol environments. +getCryptolEnvStack :: TopLevel CryptolEnvStack +getCryptolEnvStack = do + Environ _varenv _tyenv cryenvs <- gets rwEnviron + return cryenvs + +-- | Update the current Cryptol environment. +-- +-- Overwrites the previous value; the caller must ensure that the +-- value applied has not become stale. +setCryptolEnv :: CEnv.CryptolEnv -> TopLevel () +setCryptolEnv ce = do + Environ varenv tyenv cryenvs <- gets rwEnviron + let CryptolEnvStack _ ces = cryenvs + let cryenvs' = CryptolEnvStack ce ces + modify (\rw -> rw { rwEnviron = Environ varenv tyenv cryenvs' }) + +-- | Get the current Cryptol environment from a TopLevelRW. +-- +-- (Accessor method for use in SAWServer and SAWScript.REPL, which +-- have their own monads and thus different access to TopLevelRW.) +-- +-- XXX: SAWServer shouldn't be using, or need to use, TopLevelRW at +-- all. +rwGetCryptolEnv :: TopLevelRW -> CEnv.CryptolEnv +rwGetCryptolEnv rw = + let Environ _varenv _tyenv cryenvs = rwEnviron rw + CryptolEnvStack ce _ = cryenvs + in + ce + +-- | Get the current full stack of Cryptol environments from a +-- TopLevelRW. Used by the checkpointing logic, in a fairly dubious +-- way. (XXX) +rwGetCryptolEnvStack :: TopLevelRW -> CryptolEnvStack +rwGetCryptolEnvStack rw = + let Environ _varenv _tyenv cryenvs = rwEnviron rw in + cryenvs + +-- | Update the current Cryptol environment in a TopLevelRW. +-- +-- Overwrites the previous environment; caller must ensure they +-- haven't done anything to make the value they're working with +-- stale. +-- +-- (Accessor method for use in SAWServer and SAWScript.REPL, which +-- have their own monads and thus different access to TopLevelRW.) +-- +-- XXX: SAWServer shouldn't be using, or need to use, TopLevelRW at +-- all. +rwSetCryptolEnv :: CEnv.CryptolEnv -> TopLevelRW -> TopLevelRW +rwSetCryptolEnv ce rw = + let Environ varenv tyenv cryenvs = rwEnviron rw + CryptolEnvStack _ ces = cryenvs + cryenvs' = CryptolEnvStack ce ces + in + rw { rwEnviron = Environ varenv tyenv cryenvs' } + +-- | Update the current full stack of Cryptol environments in a +-- TopLevelRW. Used by the checkpointing logic, in a fairly +-- dubious way. (XXX) +-- +-- Overwrites the previous stack; caller must ensure they haven't +-- done anything to make the value they're working with stale. +rwSetCryptolEnvStack :: CryptolEnvStack -> TopLevelRW -> TopLevelRW +rwSetCryptolEnvStack cryenvs rw = + let Environ varenv tyenv _ = rwEnviron rw in + rw { rwEnviron = Environ varenv tyenv cryenvs } + +-- | Modify the current Cryptol environment in a TopLevelRW. +-- +-- (Accessor method for use in SAWServer and SAWScript.REPL, which +-- have their own monads and thus different access to TopLevelRW.) +-- +-- XXX: SAWServer shouldn't be using, or need to use, TopLevelRW at +-- all. +rwModifyCryptolEnv :: (CEnv.CryptolEnv -> CEnv.CryptolEnv) -> TopLevelRW -> TopLevelRW +rwModifyCryptolEnv f rw = + let Environ varenv tyenv cryenvs = rwEnviron rw + CryptolEnvStack ce ces = cryenvs + ce' = f ce + cryenvs' = CryptolEnvStack ce' ces + in + rw { rwEnviron = Environ varenv tyenv cryenvs' } + +-- | Push a new scope on the Cryptol environment stack. +cryptolPush :: CryptolEnvStack -> CryptolEnvStack +cryptolPush (CryptolEnvStack ce ces) = + -- Each entry is the whole environment, so duplicate the top entry + CryptolEnvStack ce (ce : ces) + +-- | Pop the current scope off the Cryptol environment stack. +cryptolPop :: CryptolEnvStack -> CryptolEnvStack +cryptolPop (CryptolEnvStack _ ces) = + -- Discard the top + case ces of + [] -> panic "cryptolPop" ["Cryptol environment scope stack ran out"] + ce : ces' -> CryptolEnvStack ce ces' + -- | TopLevel Read-Only Environment. data TopLevelRO = @@ -823,25 +960,9 @@ data JavaCodebase = data TopLevelRW = TopLevelRW { - -- | The variable environment: a map from variable names to: - -- - the definition position - -- - the lifecycle setting (experimental/current/deprecated/etc) - -- - whether the binding is rebindable - -- - the type scheme - -- - the value - -- - the help text if any - rwValueInfo :: Map SS.Name (SS.Pos, SS.PrimitiveLifecycle, SS.Rebindable, - SS.Schema, Value, Maybe [Text]) - - -- | The type environment: a map from type names to: - -- - the lifecycle setting (experimental/current/deprecated/etc) - -- - the expansion, which might be another type (this is how - -- typedefs/type aliases appear) or "abstract" (this is how - -- builtin types that aren't special cases in the AST appear) - , rwTypeInfo :: Map SS.Name (SS.PrimitiveLifecycle, SS.NamedType) - - -- | The Cryptol naming environment. - , rwCryptol :: CEnv.CryptolEnv + -- | The variable and type naming environment. + rwEnviron :: Environ + , rwRebindables :: RebindableEnv -- | The current execution position. This is only valid when the -- interpreter is calling out into saw-central to execute a @@ -853,8 +974,6 @@ data TopLevelRW = -- | The current stack trace. The most recent frame is at the front. , rwStackTrace :: Trace - , rwLocalEnv :: LocalEnv - , rwJavaCodebase :: JavaCodebase -- ^ Current state of Java sub-system. , rwProofs :: [Value] {- ^ Values, generated anywhere, that represent proofs. -} @@ -999,10 +1118,6 @@ popTraceFrames :: [a] -> TopLevel () popTraceFrames frames = mapM_ (\_ -> popTraceFrame) frames -getLocalEnv :: TopLevel LocalEnv -getLocalEnv = - gets rwLocalEnv - -- | Get the current execution position. getPosition :: TopLevel SS.Pos getPosition = @@ -1158,12 +1273,34 @@ addJVMTrans trans = do let jvmt = rwJVMTrans rw putTopLevelRW ( rw { rwJVMTrans = trans <> jvmt }) -extendEnv :: - SharedContext -> - SS.Pos -> SS.Name -> SS.Rebindable -> SS.Schema -> Maybe [Text] -> Value -> - TopLevelRW -> IO TopLevelRW -extendEnv sc pos name rb ty doc v rw = - do ce' <- +extendEnv :: SS.Pos -> SS.Name -> SS.Rebindable -> SS.Schema -> Maybe [Text] -> Value -> TopLevel () +extendEnv pos name rb ty doc v = do + sc <- gets rwSharedContext + let ident = T.mkIdent name + modname = T.packModName [name] + + -- Update the SAWScript environment. + Environ varenv tyenv cryenvs <- gets rwEnviron + rbenv <- gets rwRebindables + let (varenv', rbenv') = case rb of + SS.ReadOnlyVar -> + -- If we replace a rebindable variable at the top level with a + -- readonly one, the readonly version in varenv will hide it + -- ever after. We ought to remove it from rbenv; however, it's + -- not easy to know here whether we're at the top level or not. + -- FUTURE: maybe this will become easier in the long run. + let ve' = ScopedMap.insert name (pos, SS.Current, ty, v, doc) varenv in + (ve', rbenv) + SS.RebindableVar -> + -- The typechecker restricts this to happen only at the + -- top level and only if any existing variable is already + -- rebindable, so we don't have to update varenv. + let re' = M.insert name (pos, ty, v) rbenv in + (varenv, re') + + -- Mirror the value into the Cryptol environment if appropriate. + let CryptolEnvStack ce ces = cryenvs + ce' <- case v of VTerm t -> pure $ CEnv.bindTypedTerm (ident, t) ce @@ -1174,20 +1311,72 @@ extendEnv sc pos name rb ty doc v rw = VCryptolModule m -> pure $ CEnv.bindExtCryptolModule (modname, m) ce VString s -> - do tt <- typedTermOfString sc (Text.unpack s) + do tt <- io $ typedTermOfString sc (Text.unpack s) pure $ CEnv.bindTypedTerm (ident, tt) ce VBool b -> - do tt <- typedTermOfBool sc b + do tt <- io $ typedTermOfBool sc b pure $ CEnv.bindTypedTerm (ident, tt) ce _ -> pure ce - let valenv = rwValueInfo rw - valenv' = M.insert name (pos, SS.Current, rb, ty, v, doc) valenv - pure $ rw { rwValueInfo = valenv', rwCryptol = ce' } - where - ident = T.mkIdent name - modname = T.packModName [name] - ce = rwCryptol rw + let cryenvs' = CryptolEnvStack ce' ces + + -- Drop the new bits into place. + modify (\rw -> rw { + rwEnviron = Environ varenv' tyenv cryenvs', + rwRebindables = rbenv' + }) + +extendEnvMulti :: [(SS.Pos, SS.Name, SS.Rebindable, SS.Schema, Maybe [Text], Environ -> Value)] -> TopLevel () +extendEnvMulti bindings = do + + -- Update the SAWScript environment. + Environ varenv tyenv cryenv <- gets rwEnviron + + -- Insert all the bindings at once, and feed the final resulting + -- interpreter environment into each value. This circular + -- definition only works because of laziness and it's only legal + -- when the pieces are in a single let-block. + -- + -- Only allow lambda values because that's the only use case + -- (functions in mutually recursive "rec" sets) and it lets us + -- ignore the Cryptol environment. + -- + -- Be sure to insert v' (rather than v) so the panic check is + -- actually performed. + let insert (pos, name, rb, ty, doc, fv) tmpenv = + let v = fv environ' + v' = case v of + VLambda{} -> v + _ -> + panic "extendEnvMulti" [ + "Non-lambda value: " <> Text.pack (show v), + "Source position: " <> Text.pack (show pos) + ] + v'' = case rb of + SS.ReadOnlyVar -> v' + SS.RebindableVar -> + -- "rec" declarations can't be rebindable + panic "extendEnvMulti" [ + "Rebindable variable: " <> name, + "Source position: " <> Text.pack (show pos) + ] + in + ScopedMap.insert name (pos, SS.Current, ty, v'', doc) tmpenv + varenv' = foldr insert varenv bindings + environ' = Environ varenv' tyenv cryenv + + -- Drop the new bits into place. + modify (\rw -> rw { rwEnviron = environ' }) + +-- Note that the expansion type should have already been through the +-- typechecker, so it's ok to panic if it turns out to be broken. +addTypedef :: SS.Name -> SS.Type -> TopLevel () +addTypedef name ty = do + avail <- gets rwPrimsAvail + Environ varenv tyenv cryenv <- gets rwEnviron + let ty' = SS.substituteTyVars avail tyenv ty + tyenv' = ScopedMap.insert name (SS.Current, SS.ConcreteType ty') tyenv + modify (\rw -> rw { rwEnviron = Environ varenv tyenv' cryenv }) typedTermOfString :: SharedContext -> String -> IO TypedTerm typedTermOfString sc str = diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index dd383b5f97..f5a35f31ef 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -33,9 +33,8 @@ import qualified Control.Exception as X import Control.Monad (unless, (>=>), when) import Control.Monad.Reader (ask, asks) import Control.Monad.State (gets) -import Control.Monad.IO.Class (liftIO) import qualified Data.ByteString as BS -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe, mapMaybe) import Data.List (genericLength) import qualified Data.Map as Map import Data.Map ( Map ) @@ -64,6 +63,8 @@ import Mir.Intrinsics (MIR) import qualified Mir.Generator as MIR (RustModule) import qualified Mir.Mir as MIR +import qualified SAWSupport.ScopedMap as ScopedMap +--import SAWSupport.ScopedMap (ScopedMap) import qualified SAWSupport.Pretty as PPS (MemoStyle(..), Opts(..), defaultOpts, pShow, pShowText) import SAWCore.FiniteValue (FirstOrderValue(..)) @@ -131,6 +132,7 @@ import qualified Cryptol.Backend.Monad as V (runEval) import qualified Cryptol.Eval.Value as V (defaultPPOpts, ppValue) import qualified Cryptol.Eval.Concrete as V (Concrete(..)) +import qualified Prettyprinter as PP (pretty) import qualified Prettyprinter.Render.Text as PP (putDoc) import SAWScript.AutoMatch @@ -288,71 +290,38 @@ propagateRefChain chain1 v = -- -- XXX: at some point clean this up further. -- -bindPatternLocal :: - SS.Rebindable -> SS.Pattern -> Maybe SS.Schema -> Value -> - LocalEnv -> LocalEnv -bindPatternLocal rb pat ms v env = +bindPattern :: SS.Rebindable -> SS.Pattern -> Maybe SS.Schema -> Value -> TopLevel () +bindPattern rb pat ms v = case pat of SS.PWild _pos _ -> - env + pure () SS.PVar allpos _xpos _x Nothing -> - panic "bindPatternLocal" [ + panic "bindPattern" [ "Found pattern with no type in it", "Source position: " <> Text.pack (show allpos), "Pattern: " <> Text.pack (show pat) ] SS.PVar _allpos xpos x (Just ty) -> let s = fromMaybe (SS.tMono ty) ms in - extendLocal xpos x rb s Nothing v env + extendEnv xpos x rb s Nothing v SS.PTuple _pos ps -> case v of - VTuple vs -> foldr ($) env (zipWith3 (bindPatternLocal rb) ps mss vs) - where mss = case ms of - Nothing -> - repeat Nothing - Just (SS.Forall ks (SS.TyCon _ (SS.TupleCon _) ts)) -> - [ Just (SS.Forall ks t) | t <- ts ] - Just t -> - panic "bindPatternLocal" [ - "Expected tuple type, got " <> Text.pack (show t) - ] + VTuple vs -> do + let mss = case ms of + Nothing -> + repeat Nothing + Just (SS.Forall ks (SS.TyCon _ (SS.TupleCon _) ts)) -> + [ Just (SS.Forall ks t) | t <- ts ] + Just t -> + panic "bindPattern" [ + "Expected tuple type, got " <> Text.pack (show t) + ] + sequence_ $ zipWith3 (bindPattern rb) ps mss vs _ -> panic "bindPatternLocal" [ "Expected tuple value; got " <> Text.pack (show v) ] --- See notes in bindPatternLocal above regarding the schema argument. -bindPatternEnv :: SS.Pattern -> Maybe SS.Schema -> Value -> TopLevelRW -> TopLevel TopLevelRW -bindPatternEnv pat ms v env = - case pat of - SS.PWild _pos _ -> - pure env - SS.PVar allpos _xpos _x Nothing -> - panic "bindPatternEnv" [ - "Found pattern with no type in it", - "Source position: " <> Text.pack (show allpos), - "Pattern: " <> Text.pack (show pat) - ] - SS.PVar _allpos xpos x (Just ty) -> do - sc <- getSharedContext - let s = fromMaybe (SS.tMono ty) ms - liftIO $ extendEnv sc xpos x SS.ReadOnlyVar s Nothing v env - SS.PTuple _pos ps -> - case v of - VTuple vs -> foldr (=<<) (pure env) (zipWith3 bindPatternEnv ps mss vs) - where mss = case ms of - Nothing -> repeat Nothing - Just (SS.Forall ks (SS.TyCon _ (SS.TupleCon _) ts)) -> - [ Just (SS.Forall ks t) | t <- ts ] - Just t -> - panic "bindPatternEnv" [ - "Expected tuple type, got " <> Text.pack (show t) - ] - _ -> - panic "bindPatternEnv" [ - "Expected tuple value; got " <> Text.pack (show v) - ] - ------------------------------------------------------------ -- InterpreterMonad @@ -365,42 +334,54 @@ class (Monad m, MonadFail m) => InterpreterMonad m where actionFromValue :: FromValue a => FromValueHow -> Value -> m a mkValue :: SS.Pos -> RefChain -> m Value -> Value getMonadContext :: m SS.Context - withLocalEnvAny :: LocalEnv -> m a -> m a + pushScopeAny :: m () + popScopeAny :: m () + withEnvironAny :: Environ -> m a -> m a instance InterpreterMonad TopLevel where liftTopLevel m = m actionFromValue = fromValue mkValue pos chain m = VTopLevel pos chain m getMonadContext = return SS.TopLevel - withLocalEnvAny = withLocalEnv + pushScopeAny = pushScope + popScopeAny = popScope + withEnvironAny = withEnviron instance InterpreterMonad ProofScript where liftTopLevel m = scriptTopLevel m actionFromValue = fromValue mkValue pos chain m = VProofScript pos chain m getMonadContext = return SS.ProofScript - withLocalEnvAny = withLocalEnvProof + pushScopeAny = scriptTopLevel pushScope + popScopeAny = scriptTopLevel popScope + withEnvironAny = withEnvironProofScript instance InterpreterMonad LLVMCrucibleSetupM where liftTopLevel m = llvmTopLevel m actionFromValue = fromValue mkValue pos chain m = VLLVMCrucibleSetup pos chain m getMonadContext = return SS.LLVMSetup - withLocalEnvAny = withLocalEnvLLVM + pushScopeAny = llvmTopLevel pushScope + popScopeAny = llvmTopLevel popScope + withEnvironAny = withEnvironLLVM instance InterpreterMonad JVMSetupM where liftTopLevel m = jvmTopLevel m actionFromValue = fromValue mkValue pos chain m = VJVMSetup pos chain m getMonadContext = return SS.JavaSetup - withLocalEnvAny = withLocalEnvJVM + pushScopeAny = jvmTopLevel pushScope + popScopeAny = jvmTopLevel popScope + withEnvironAny = withEnvironJVM instance InterpreterMonad MIRSetupM where liftTopLevel m = mirTopLevel m actionFromValue = fromValue mkValue pos chain m = VMIRSetup pos chain m getMonadContext = return SS.MIRSetup - withLocalEnvAny = withLocalEnvMIR + pushScopeAny = mirTopLevel pushScope + popScopeAny = mirTopLevel popScope + withEnvironAny = withEnvironMIR ------------------------------------------------------------ @@ -441,7 +422,12 @@ applyValue pos v1info v1 v2 = VLambda env mname pat e -> do let name = fromMaybe "(lambda)" mname enter name - r <- withLocalEnv (bindPatternLocal SS.ReadOnlyVar pat Nothing v2 env) (interpretExpr e) + r <- withEnviron env $ do + pushScope + bindPattern SS.ReadOnlyVar pat Nothing v2 + r' <- interpretExpr e + popScope + return r' leave return $ insertRefChain pos name r VBuiltin name args wf -> case wf of @@ -490,21 +476,21 @@ interpretExpr expr = return $ VInteger z SS.Code pos str -> do sc <- getSharedContext - cenv <- fmap rwCryptol getMergedEnv + cenv <- getCryptolEnv --io $ putStrLn $ "Parsing code: " ++ show str --showCryptolEnv' cenv let str' = toInputText pos str t <- io $ CEnv.parseTypedTerm sc cenv str' return (VTerm t) SS.CType pos str -> do - cenv <- fmap rwCryptol getMergedEnv + cenv <- getCryptolEnv let str' = toInputText pos str s <- io $ CEnv.parseSchema cenv str' return (VType s) SS.Array _pos es -> VArray <$> traverse interpretExpr es SS.Block _pos stmts -> do - env <- getLocalEnv + env <- gets rwEnviron return $ VDo [] env stmts SS.Tuple _pos es -> VTuple <$> traverse interpretExpr es @@ -521,25 +507,34 @@ interpretExpr expr = a <- interpretExpr e return (tupleLookupValue pos a i) SS.Var pos x -> do - rw <- getMergedEnv - case Map.lookup x (rwValueInfo rw) of - Nothing -> - -- This should be rejected by the typechecker, so panic - panic "interpretExpr" [ - "Read of unknown variable " <> x - ] - Just (_defpos, lc, _rebindable, _ty, v, _doc) - | Set.member lc (rwPrimsAvail rw) -> do - let v' = injectPositionIntoMonadicValue pos v - v'' = insertRefChain pos x v' - return v'' - | otherwise -> - -- This case is also rejected by the typechecker - panic "interpretExpr" [ - "Read of inaccessible variable " <> x - ] + avail <- gets rwPrimsAvail + Environ varenv _tyenv _cryenv <- gets rwEnviron + rbenv <- gets rwRebindables + let info = case ScopedMap.lookup x varenv of + Nothing -> + -- Try the rebindable environment + case Map.lookup x rbenv of + Nothing -> Nothing + Just (_defpos, _ty, v) -> Just (Current, v) + Just (_defpos, lc, _ty, v, _doc) -> Just (lc, v) + case info of + Nothing -> + -- This should be rejected by the typechecker; panic + panic "interpretExpr" [ + "Read of unknown variable " <> x + ] + Just (lc, v) + | Set.member lc avail -> do + let v' = injectPositionIntoMonadicValue pos v + v'' = insertRefChain pos x v' + return v'' + | otherwise -> + -- This case is also rejected by the typechecker + panic "interpretExpr" [ + "Read of inaccessible variable " <> x + ] SS.Lambda _pos mname pat e -> do - env <- getLocalEnv + env <- gets rwEnviron return $ VLambda env mname pat e SS.Application pos e1 e2 -> do let v1info = "Expression: " <> PPS.pShowText e1 @@ -548,8 +543,11 @@ interpretExpr expr = let v2' = injectPositionIntoMonadicValue (SS.getPos e2) v2 applyValue pos v1info v1 v2' SS.Let _ dg e -> do - env' <- interpretDeclGroup SS.ReadOnlyVar dg - withLocalEnv env' (interpretExpr e) + pushScope + interpretDeclGroup SS.ReadOnlyVar dg + v <- interpretExpr e + popScope + return v SS.TSig _ e _ -> interpretExpr e SS.IfThenElse pos e1 e2 e3 -> do @@ -565,39 +563,73 @@ interpretExpr expr = "Expression: " <> PPS.pShowText e1 ] --- Eval a "decl", which is the RHS of a let-binding. --- Evaluates the body expression purely. -interpretDecl :: SS.Rebindable -> LocalEnv -> SS.Decl -> TopLevel LocalEnv -interpretDecl rebindable env (SS.Decl _ pat mt expr) = do - v <- interpretExpr expr - return (bindPatternLocal rebindable pat mt v env) - --- Eval the RHS of a single let-binding in a mutually recursive group. --- These are required to be functions; that's enforced by the --- typechecker. -interpretFunction :: LocalEnv -> SS.Expr -> Value -interpretFunction env expr = - case expr of - SS.Lambda _ mname pat e -> VLambda env mname pat e - SS.TSig _ e _ -> interpretFunction env e - _ -> - panic "interpretFunction" [ - "Not a function", - "Expression found: " <> PPS.pShowText expr - ] - -- Eval a "decl group", which is a let-binding or group of mutually -- recursive let-bindings. -interpretDeclGroup :: SS.Rebindable -> SS.DeclGroup -> TopLevel LocalEnv -interpretDeclGroup rebindable (SS.NonRecursive d) = do - env <- getLocalEnv - interpretDecl rebindable env d -interpretDeclGroup rebindable (SS.Recursive ds) = do - env <- getLocalEnv - let addDecl (SS.Decl _ pat mty e) = - bindPatternLocal rebindable pat mty (interpretFunction env' e) - env' = foldr addDecl env ds - return env' +-- +-- The bodies are interpreted purely. +interpretDeclGroup :: SS.Rebindable -> SS.DeclGroup -> TopLevel () +interpretDeclGroup rebindable dg = case dg of + SS.NonRecursive (SS.Decl _ pat mt expr) -> do + v <- interpretExpr expr + bindPattern rebindable pat mt v + SS.Recursive ds -> do + let + + -- Get a value for the body of one of the declarations. + -- Recursive declaration sets are only allowed to contain + -- functions; panic if we get anything else. + -- + -- We return a function taking an environment because we + -- need to close in the environment containing _all_ the + -- declarations _into_ all the declarations, which is a + -- circular knot that can only be constructed in very + -- specific ways. + extractFunction e0 = case e0 of + SS.Lambda _ mname pat e1 -> + \env -> VLambda env mname pat e1 + SS.TSig _ e1 _ -> + extractFunction e1 + _ -> + panic "interpretDeclGroup" [ + "Found non-function in a recursive declaration group", + -- XXX should print the name here! + "Expression found: " <> PPS.pShowText e0 + ] + + -- Get the name (and type) for one of the declarations. + -- Recursive declaration sets are only allowed to contain + -- functions, so the pattern cannot be a tuple. + extractName pat = case pat of + SS.PWild _ _ -> Nothing + SS.PVar _ xpos x (Just ty) -> Just (xpos, x, ty) + SS.PVar _ _ x Nothing -> + panic "interpretDeclGroup" [ + "Found variable with no type in a recursive decl group", + "Variable: " <> x + ] + SS.PTuple{} -> + panic "interpretDeclGroup" [ + "Found tuple pattern in a recursive declaration group", + "Pattern: " <> Text.pack (show (PP.pretty pat)) + ] + + -- Get all the info for a decl. + extractBoth (SS.Decl _ pat _mty e) = + case extractName pat of + Nothing -> Nothing + Just (xpos, x, ty) -> + let fv = extractFunction e in + Just (xpos, x, rebindable, SS.tMono ty, Nothing, fv) + + -- Extract all the info for all decls. + ds' = mapMaybe extractBoth ds + + -- Now add all the declarations. + -- + -- Note that the lambdas in all the declarations need the final + -- resulting environment that contains all the declarations, + -- which is something of a headache to arrange in Haskell. + extendEnvMulti ds' -- Bind a monadic value into the monadic execution sequence. -- @@ -648,7 +680,11 @@ interpretMonadAction fromHow v = case v of FromArgument -> pushTraceFrame SS.PosInsideBuiltin "(callback)" pushTraceFrames chain - r <- withLocalEnvAny env (interpretDoStmts body) + r <- withEnvironAny env $ do + pushScopeAny + r' <- interpretDoStmts body + popScopeAny + return r' liftTopLevel $ do popTraceFrames chain @@ -708,13 +744,12 @@ interpretMonadAction fromHow v = case v of -- (XXX: should that be stored into the monad context or not? Apparently -- not, currently.) -- -interpretDoStmt :: forall m. InterpreterMonad m => SS.Stmt -> m LocalEnv +interpretDoStmt :: forall m. InterpreterMonad m => SS.Stmt -> m () interpretDoStmt stmt = let ?fileReader = BS.readFile in -- XXX are the uses of push/popPosition here suitable? not super clear case stmt of SS.StmtBind pos pat e -> do - env <- liftTopLevel getLocalEnv -- Execute the expression purely first. ("purely") baseVal :: Value <- liftTopLevel $ interpretExpr e -- Now bind the resulting value to execute it. @@ -725,27 +760,21 @@ interpretDoStmt stmt = result :: Value <- bindMonadAction pos baseVal -- Bind (in the name-binding, not monad-binding sense) the -- result to the pattern. - return $ bindPatternLocal SS.ReadOnlyVar pat Nothing result env + liftTopLevel $ bindPattern SS.ReadOnlyVar pat Nothing result SS.StmtLet _pos rebindable dg -> do -- Process the declarations liftTopLevel $ interpretDeclGroup rebindable dg SS.StmtCode _ spos str -> do liftTopLevel $ do sc <- getSharedContext - rw <- getMergedEnv - + ce <- getCryptolEnv let str' = toInputText spos str - ce' <- io $ CEnv.parseDecls sc (rwCryptol rw) str' - -- FIXME: Local bindings get saved into the global cryptol environment here. - -- We should change parseDecls to return only the new bindings instead. - putTopLevelRW $ rw{rwCryptol = ce'} - -- return the current local environment unchanged - liftTopLevel getLocalEnv + ce' <- io $ CEnv.parseDecls sc ce str' + setCryptolEnv ce' SS.StmtImport _ _ -> fail "block-level import unimplemented" SS.StmtTypedef _ _ name ty -> do - env <- liftTopLevel $ getLocalEnv - return $ LocalTypedef name ty : env + liftTopLevel $ addTypedef name ty -- Eval some statements from a do-block. -- @@ -801,10 +830,11 @@ interpretDoStmts (stmts, lastexpr) = return $ mkValue pos [] result' stmt : more -> do - -- Execute the expression and get the updated environment - env' <- interpretDoStmt stmt + -- Execute the expression and update the environment + interpretDoStmt stmt -- Run the rest of the block with the updated environment - withLocalEnvAny env' (interpretDoStmts (more, lastexpr)) + v <- interpretDoStmts (more, lastexpr) + return v -- Execute a top-level bind. processStmtBind :: @@ -814,8 +844,7 @@ processStmtBind :: SS.Pattern -> SS.Expr -> m () -processStmtBind printBinds pos pat expr = do -- mx mt - rw <- liftTopLevel getMergedEnv +processStmtBind printBinds pos pat expr = do -- Eval the expression baseVal <- liftTopLevel $ interpretExpr expr @@ -845,7 +874,7 @@ processStmtBind printBinds pos pat expr = do -- mx mt -- When in the repl, print the result. when printBinds $ do - let opts = rwPPOpts rw + opts <- liftTopLevel $ gets rwPPOpts -- Extract the variable, if any, from the pattern. If there isn't -- any single variable use "it". @@ -868,9 +897,7 @@ processStmtBind printBinds pos pat expr = do -- mx mt liftTopLevel $ printOutLnTop Info $ Text.unpack $ name <> " : " <> PPS.pShowText ty _ -> return () - liftTopLevel $ - do rw' <- getTopLevelRW - putTopLevelRW =<< bindPatternEnv pat (Just (SS.tMono ty)) result rw' + liftTopLevel $ bindPattern SS.ReadOnlyVar pat (Just (SS.tMono ty)) result -- | Interpret a top-level statement in an interpreter monad (any of the SAWScript monads) -- This duplicates the logic in interpretDoStmt for no particularly good reason. @@ -881,11 +908,22 @@ interpretTopStmt :: InterpreterMonad m => interpretTopStmt printBinds stmt = do let ?fileReader = BS.readFile + avail <- liftTopLevel $ gets rwPrimsAvail ctx <- getMonadContext - rw <- liftTopLevel getMergedEnv - let valueInfo = rwValueInfo rw - valueInfo' = Map.map (\(pos, lc, rb, ty, _v, _doc) -> (pos, lc, rb, ty)) valueInfo - stmt' <- processTypeCheck $ checkStmt (rwPrimsAvail rw) valueInfo' (rwTypeInfo rw) ctx stmt + + stmt' <- do + -- XXX this is not the right way to do this + -- - shouldn't have to flatten the environments + -- - shouldn't be typechecking one statement at a time regardless + Environ varenv tyenv _cryenvs <- liftTopLevel $ gets rwEnviron + rbenv <- liftTopLevel $ gets rwRebindables + let varenv' = Map.map (\(pos, lc, ty, _v, _doc) -> (pos, lc, SS.ReadOnlyVar, ty)) $ ScopedMap.flatten varenv + rbenv' = Map.map (\(pos, ty, _v) -> (pos, SS.Current, SS.RebindableVar, ty)) rbenv + -- If anything appears in both, favor the real environment + varenv'' = Map.union varenv' rbenv' + + let tyenv' = ScopedMap.flatten tyenv + processTypeCheck $ checkStmt avail varenv'' tyenv' ctx stmt case stmt' of @@ -896,34 +934,32 @@ interpretTopStmt printBinds stmt = do processStmtBind printBinds pos pat expr SS.StmtLet _pos rebindable dg -> - liftTopLevel $ do - env <- interpretDeclGroup rebindable dg - rw' <- getMergedEnv' env - putTopLevelRW rw' + liftTopLevel $ interpretDeclGroup rebindable dg SS.StmtCode _ spos str -> liftTopLevel $ do sc <- getSharedContext + cenv <- getCryptolEnv --io $ putStrLn $ "Processing toplevel code: " ++ show str --showCryptolEnv - cenv' <- io $ CEnv.parseDecls sc (rwCryptol rw) $ toInputText spos str - putTopLevelRW $ rw { rwCryptol = cenv' } + cenv' <- io $ CEnv.parseDecls sc cenv $ toInputText spos str + setCryptolEnv cenv' --showCryptolEnv SS.StmtImport _ imp -> liftTopLevel $ do sc <- getSharedContext + cenv <- getCryptolEnv --showCryptolEnv let mLoc = iModule imp qual = iAs imp spec = iSpec imp - cenv' <- io $ CEnv.importCryptolModule sc (rwCryptol rw) mLoc qual CEnv.PublicAndPrivate spec - putTopLevelRW $ rw { rwCryptol = cenv' } + cenv' <- io $ CEnv.importCryptolModule sc cenv mLoc qual CEnv.PublicAndPrivate spec + setCryptolEnv cenv' --showCryptolEnv SS.StmtTypedef _ _ name ty -> - liftTopLevel $ do - putTopLevelRW $ addTypedef name ty rw + liftTopLevel $ addTypedef name ty -- Hook for AutoMatch stmtInterpreter :: StmtInterpreter @@ -933,7 +969,16 @@ stmtInterpreter ro rw stmts = -- so as to (a) get the right behavior (as long as interpretTopStmt -- and interpretDoStmt are different, which they are) and (b) avoid -- needing to provide a block result value. - fst <$> runTopLevel (withLocalEnv emptyLocal (mapM_ (interpretTopStmt False) stmts)) ro rw + -- + -- XXX what scope should this use? Prior to #2720 it substituted an + -- empty "local environment" for the current "local environment", + -- which would have dropped an ill-specified part of the namespace. + -- That wasn't particularly sensible and probably wasn't correct, + -- but we could reasonably here want either the current environment + -- or a copy of the environment captured when we start AutoMatch, + -- and it's not obvious which. For the moment, we'll use the current + -- environment because that doesn't require any fiddling. + fst <$> runTopLevel (mapM_ (interpretTopStmt False) stmts) ro rw interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel () interpretFile file runMain = @@ -963,9 +1008,9 @@ interpretFile file runMain = -- | Evaluate the value called 'main' from the current environment. interpretMain :: TopLevel () interpretMain = do - rw <- getTopLevelRW avail <- gets rwPrimsAvail - tyenv <- gets rwTypeInfo + Environ varenv tyenv _cryenv <- gets rwEnviron + rbenv <- gets rwRebindables let pos = SS.PosInternal "entry" -- We need the type to be "TopLevel a", not just "TopLevel ()". -- There are several (old) tests in the test suite whose main @@ -975,14 +1020,24 @@ interpretMain = do tyRet = SS.TyVar pos "a" tyMonadic = SS.tBlock pos (SS.tContext pos SS.TopLevel) tyRet tyExpected = SS.Forall [(pos, "a")] tyMonadic - case Map.lookup "main" (rwValueInfo rw) of + let main = case ScopedMap.lookup "main" varenv of + Just (_defpos, lc, tyFound, v, _doc) -> Just (lc, tyFound, v) + -- Having main be rebindable doesn't make much sense, but + -- it's easier to have this code than to spend time + -- explaining that it's not allowed. + Nothing -> case Map.lookup "main" rbenv of + Nothing -> Nothing + Just (_defpos, tyFound, v) -> Just (Current, tyFound, v) + case main of Nothing -> -- Don't fail or complain if there's no main. return () - Just (_defpos, Current, _rebindable, tyFound, v, _doc) -> case tyFound of + Just (Current, tyFound, v) -> case tyFound of SS.Forall _ (SS.TyCon _ SS.BlockCon [_, _]) -> + -- XXX shouldn't have to do this + let tyenv' = ScopedMap.flatten tyenv in -- It looks like a monadic value, so check more carefully. - case typesMatch avail tyenv tyFound tyExpected of + case typesMatch avail tyenv' tyFound tyExpected of False -> -- While we accept any TopLevel a, don't encourage people -- to do that. @@ -995,7 +1050,7 @@ interpretMain = do -- If the type is something entirely random, like a Term or a -- String or something, just ignore it. return () - Just (_defpos, lc, _rebindable, _ty, _v, _doc) -> + Just (lc, _ty, _v) -> -- There is no way for things other than primitives to get marked -- experimental or deprecated, so this isn't possible. If we allow -- users to deprecate their own functions in the future, change @@ -1057,16 +1112,15 @@ buildTopLevelEnv proxy opts scriptArgv = , biBasicSS = ss } ce0 <- CEnv.initCryptolEnv sc + let cryenv0 = CryptolEnvStack ce0 [] jvmTrans <- CJ.mkInitialJVMContext halloc let rw0 = TopLevelRW - { rwValueInfo = primValueEnv opts bic - , rwTypeInfo = primNamedTypeEnv - , rwCryptol = ce0 + { rwEnviron = primEnviron opts bic cryenv0 + , rwRebindables = Map.empty , rwPosition = SS.Unknown , rwStackTrace = Trace.empty - , rwLocalEnv = [] , rwProofs = [] , rwPPOpts = PPS.defaultOpts , rwSharedContext = sc @@ -1681,14 +1735,12 @@ add_primitives lc _bic _opts = do toplevelSubshell :: () -> TopLevel Value toplevelSubshell () = do m <- roSubshell <$> ask - env <- getLocalEnv - toValue "subshell" <$> withLocalEnv env m + toValue "subshell" <$> m proofScriptSubshell :: () -> ProofScript Value proofScriptSubshell () = do m <- scriptTopLevel $ asks roProofSubshell - env <- scriptTopLevel $ getLocalEnv - toValue "proof_subshell" <$> withLocalEnvProof env m + toValue "proof_subshell" <$> m -- The "for" builtin. -- @@ -2067,7 +2119,7 @@ print_value :: Value -> TopLevel () print_value (VString s) = printOutLnTop Info (Text.unpack s) print_value (VTerm t) = do sc <- getSharedContext - cenv <- fmap rwCryptol getTopLevelRW + cenv <- getCryptolEnv let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv) unless (null (getAllExts (ttTerm t))) $ fail "term contains symbolic variables" @@ -6424,7 +6476,7 @@ primNamedTypeEnv = fmap extract primTypes primValueEnv :: Options -> BuiltinContext -> - Map SS.Name (SS.Pos, PrimitiveLifecycle, SS.Rebindable, SS.Schema, Value, Maybe [Text]) + Map SS.Name (SS.Pos, PrimitiveLifecycle, SS.Schema, Value, Maybe [Text]) primValueEnv opts bic = Map.mapWithKey extract primitives where header = [ @@ -6445,5 +6497,20 @@ primValueEnv opts bic = Map.mapWithKey extract primitives header <> tag p <> name n p <> primitiveDoc p extract n p = let pos = SS.PosInternal "<>" in - (pos, primitiveLife p, SS.ReadOnlyVar, primitiveType p, + (pos, primitiveLife p, primitiveType p, (primitiveFn p) opts bic, Just $ doc n p) + +primEnviron :: Options -> BuiltinContext -> CryptolEnvStack -> Environ +primEnviron opts bic cryenvs = + + -- Do a scope push so the builtins live by themselves in their own + -- scope layer. This has the result of separating them from the + -- user's variables in the :env output (which is now grouped by + -- scope) and, because the builtin layer is readonly, might be + -- marginally more efficient as the user's globals are added. + + let tyenv = ScopedMap.push $ ScopedMap.seed primNamedTypeEnv + varenv = ScopedMap.push $ ScopedMap.seed $ primValueEnv opts bic + in + Environ varenv tyenv cryenvs + diff --git a/saw-script/src/SAWScript/REPL/Command.hs b/saw-script/src/SAWScript/REPL/Command.hs index 4fb23b57fd..bcb0504df9 100644 --- a/saw-script/src/SAWScript/REPL/Command.hs +++ b/saw-script/src/SAWScript/REPL/Command.hs @@ -33,19 +33,22 @@ module SAWScript.REPL.Command ( --import SAWCore.SharedTerm (SharedContext) +import qualified SAWSupport.ScopedMap as ScopedMap + +import SAWCentral.Position (getPos, Pos) +import SAWCentral.Value (Environ(..)) import SAWScript.REPL.Monad import SAWScript.REPL.Trie -import SAWCentral.Position (getPos, Pos) import SAWScript.Token (Token) import Cryptol.Parser (ParseError()) -import Control.Monad (guard, void) +import Control.Monad (guard, unless, void) import Data.Char (isSpace,isPunctuation,isSymbol) import Data.Function (on) -import Data.List (intercalate, nub) +import Data.List (intercalate, intersperse, nub) import qualified Data.Text as Text import System.FilePath((), isPathSeparator) import System.Directory(getHomeDirectory,getCurrentDirectory,setCurrentDirectory,doesDirectoryExist) @@ -74,7 +77,7 @@ import SAWScript.Interpreter (interpretTopStmt) import qualified SAWScript.Lexer (lexSAW) import qualified SAWScript.Parser (parseStmtSemi, parseExpression, parseSchemaPattern) import SAWCentral.TopLevel (TopLevelRW(..)) -import SAWCentral.AST (PrimitiveLifecycle(..), everythingAvailable) +import SAWCentral.AST (PrimitiveLifecycle(..), everythingAvailable, Rebindable(..)) -- Commands -------------------------------------------------------------------- @@ -199,14 +202,19 @@ typeOfCmd str Right expr -> return expr let pos = getPos expr decl = SS.Decl pos (SS.PWild pos Nothing) Nothing expr - rw <- getValueEnvironment + rw <- getTopLevelRW decl' <- do let primsAvail = rwPrimsAvail rw - valueInfo = rwValueInfo rw - squash (defpos, lc, rb, ty, _val, _doc) = (defpos, lc, rb, ty) - valueInfo' = Map.map squash valueInfo - typeInfo = rwTypeInfo rw - let (errs_or_results, warns) = checkDecl primsAvail valueInfo' typeInfo decl + -- XXX it should not be necessary to do this munging + Environ varenv tyenv _cryenvs = rwEnviron rw + squash (defpos, lc, ty, _val, _doc) = (defpos, lc, ReadOnlyVar, ty) + varenv' = Map.map squash $ ScopedMap.flatten varenv + tyenv' = ScopedMap.flatten tyenv + rbenv = rwRebindables rw + rbsquash (defpos, ty, _val) = (defpos, Current, RebindableVar, ty) + rbenv' = Map.map rbsquash rbenv + varenv'' = Map.union varenv' rbenv' + let (errs_or_results, warns) = checkDecl primsAvail varenv'' tyenv' decl let issueWarning (msgpos, msg) = -- XXX the print functions should be what knows how to show positions... putStrLn (show msgpos ++ ": Warning: " ++ msg) @@ -223,7 +231,7 @@ searchCmd str pat <- case SAWScript.Parser.parseSchemaPattern tokens of Left err -> fail (show err) Right pat -> return pat - rw <- getValueEnvironment + rw <- getTopLevelRW -- Always search the entire environment and recognize all type -- names in the user's pattern, regardless of whether @@ -240,19 +248,24 @@ searchCmd str -- for deprecated functions that take Terms. let primsAvail = rwPrimsAvail rw - valueInfo = rwValueInfo rw - squash (pos, lc, rb, ty, _val, _doc) = (pos, lc, rb, ty) - valueInfo' = Map.map squash valueInfo - typeInfo = rwTypeInfo rw - (errs_or_results, warns) = checkSchemaPattern everythingAvailable valueInfo' typeInfo pat + -- XXX it should not be necessary to do this munging + Environ varenv tyenv _cryenv = rwEnviron rw + rbenv = rwRebindables rw + squash (pos, lc, ty, _val, _doc) = (pos, lc, ReadOnlyVar, ty) + varenv' = Map.map squash $ ScopedMap.flatten varenv + tyenv' = ScopedMap.flatten tyenv + rbsquash (pos, ty, _val) = (pos, Current, RebindableVar, ty) + rbenv' = Map.map rbsquash rbenv + varenv'' = Map.union varenv' rbenv' + (errs_or_results, warns) = checkSchemaPattern everythingAvailable varenv'' tyenv' pat let issueWarning (msgpos, msg) = -- XXX the print functions should be what knows how to show positions... putStrLn (show msgpos ++ ": Warning: " ++ msg) io $ mapM_ issueWarning warns pat' <- either failTypecheck return $ errs_or_results - let search = compileSearchPattern typeInfo pat' + let search = compileSearchPattern tyenv pat' keep (_pos, _lc, _rb, ty) = matchSearchPattern search ty - allMatches = Map.filter keep valueInfo' + allMatches = Map.filter keep varenv' -- Divide the results into visible, experimental-not-visible, -- and deprecated-not-visible. @@ -339,34 +352,66 @@ quitCmd = stop envCmd :: REPL () envCmd = do - rw <- getValueEnvironment - let avail = rwPrimsAvail rw - valueInfo = rwValueInfo rw - keep (_pos, lc, _rb, _ty, _v, _doc) = Set.member lc avail - valueInfo' = Map.filter keep valueInfo - say (x, (_pos, _lc, _rb, ty, _val, _doc)) = - TextIO.putStrLn (x <> " : " <> PPS.pShowText ty) - io $ mapM_ say $ Map.assocs valueInfo' + rw <- getTopLevelRW + let Environ varenv _tyenv _cryenv = rwEnviron rw + rbenv = rwRebindables rw + avail = rwPrimsAvail rw + + -- print the rebindable globals first, if any + unless (Map.null rbenv) $ do + let rbsay (x, (_pos, ty, _v)) = do + let ty' = PPS.pShowText ty + TextIO.putStrLn (x <> " : rebindable " <> ty') + io $ mapM_ rbsay $ Map.assocs rbenv + io $ TextIO.putStrLn "" + + -- print the normal environment + let say (x, (_pos, _lc, ty, _v, _doc)) = do + let ty' = PPS.pShowText ty + TextIO.putStrLn (x <> " : " <> ty') + -- Print only the visible objects + keep (_x, (_pos, lc, _ty, _v, _doc)) = Set.member lc avail + -- Insert a blank line in the output where there's a scope boundary + printScope mItems = case mItems of + Nothing -> TextIO.putStrLn "" + Just items -> mapM_ say $ filter keep items + -- Reverse the list of scopes so the innermost prints last, + -- because that's what people will expect to see. + itemses = reverse $ ScopedMap.scopedAssocs varenv + io $ mapM_ printScope $ intersperse Nothing $ map Just itemses tenvCmd :: REPL () tenvCmd = do - rw <- getValueEnvironment + rw <- getTopLevelRW let avail = rwPrimsAvail rw - typeInfo = rwTypeInfo rw - typeInfo' = Map.filter (\(lc, _ty) -> Set.member lc avail) typeInfo - say (a, (_lc, ty)) = - TextIO.putStrLn (a <> " : " <> PPS.pShowText ty) - io $ mapM_ say $ Map.assocs typeInfo' + Environ _varenv tyenv _cryenv = rwEnviron rw + say (x, (_lc, ty)) = do + let ty' = PPS.pShowText ty + TextIO.putStrLn (x <> " : " <> ty') + -- Print only the visible objects + keep (_x, (lc, _ty)) = Set.member lc avail + -- Insert a blank line in the output where there's a scope boundary + printScope mItems = case mItems of + Nothing -> TextIO.putStrLn "" + Just items -> mapM_ say $ filter keep items + -- Reverse the list of scopes so the innermost prints last, + -- because that's what people will expect to see. + itemses = reverse $ ScopedMap.scopedAssocs tyenv + io $ mapM_ printScope $ intersperse Nothing $ map Just itemses helpCmd :: String -> REPL () helpCmd cmd | null cmd = io (mapM_ putStrLn (genHelp commandList)) | otherwise = - do env <- getEnvironment - case Map.lookup (Text.pack cmd) (rwValueInfo env) of - Just (_pos, _lc, _rb, _ty, _v, Just doc) -> + do rw <- getTopLevelRW + -- Note: there's no rebindable builtins and thus no way to + -- attach help text to anything rebindable, so we can ignore + -- the rebindables. + let Environ varenv _tyenv _cryenvs = rwEnviron rw + case ScopedMap.lookup (Text.pack cmd) varenv of + Just (_pos, _lc, _ty, _v, Just doc) -> io $ mapM_ TextIO.putStrLn doc - Just (_pos, _lc, _rb, _ty, _v, Nothing) -> do + Just (_pos, _lc, _ty, _v, Nothing) -> do io $ putStrLn $ "// No documentation is available." typeOfCmd cmd Nothing -> diff --git a/saw-script/src/SAWScript/REPL/Haskeline.hs b/saw-script/src/SAWScript/REPL/Haskeline.hs index 853f10558a..ede53f9a06 100644 --- a/saw-script/src/SAWScript/REPL/Haskeline.hs +++ b/saw-script/src/SAWScript/REPL/Haskeline.hs @@ -57,8 +57,8 @@ replBody mbBatch begin = enableSubshell m = REPL $ \refs -> - do let ro' = (eTopLevelRO refs){ roSubshell = subshell (runInputT replSettings (withInterrupt loop)) } - unREPL m refs{ eTopLevelRO = ro' } + do let ro' = (rTopLevelRO refs){ roSubshell = subshell (runInputT replSettings (withInterrupt loop)) } + unREPL m refs{ rTopLevelRO = ro' } loop = do prompt <- MTL.lift getPrompt diff --git a/saw-script/src/SAWScript/REPL/Monad.hs b/saw-script/src/SAWScript/REPL/Monad.hs index 4640170295..300d019e83 100644 --- a/saw-script/src/SAWScript/REPL/Monad.hs +++ b/saw-script/src/SAWScript/REPL/Monad.hs @@ -49,9 +49,8 @@ module SAWScript.REPL.Monad ( -- ** SAWScript stuff , getSharedContext , getTopLevelRO - , getValueEnvironment - , getEnvironment, modifyEnvironment, putEnvironment - , getEnvironmentRef + , getTopLevelRW, modifyTopLevelRW, putTopLevelRW + , getTopLevelRWRef , getProofStateRef , getSAWScriptValueNames , getSAWScriptTypeNames @@ -85,6 +84,8 @@ import qualified Control.Exception as X import System.IO.Error (isUserError, ioeGetErrorString) import System.Exit (ExitCode) +import qualified SAWSupport.ScopedMap as ScopedMap + import SAWCore.SharedTerm (Term) import CryptolSAWCore.CryptolEnv import qualified Data.AIG as AIG @@ -97,10 +98,8 @@ import SAWCore.SAWCore (SharedContext) import SAWCentral.Options (Options) import SAWCentral.Proof (ProofState, ProofResult(..), psGoals) import SAWCentral.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..), runTopLevel) -import SAWCentral.Value - ( AIGProxy(..), mergeLocalEnv - , ProofScript(..), showsProofResult, - ) +import SAWCentral.Value (AIGProxy(..), ProofScript(..), showsProofResult, Environ(..), + rwGetCryptolEnv, rwModifyCryptolEnv) import SAWScript.Interpreter (buildTopLevelEnv) import SAWScript.ValueOps (makeCheckpoint, restoreCheckpoint) @@ -113,11 +112,11 @@ deriving instance Typeable AIG.Proxy -- REPL Environment. data Refs = Refs - { eContinue :: IORef Bool - , eIsBatch :: Bool - , eTopLevelRO :: TopLevelRO - , environment :: IORef TopLevelRW - , proofState :: Maybe (IORef ProofState) + { rContinue :: IORef Bool + , rIsBatch :: Bool + , rTopLevelRO :: TopLevelRO + , rTopLevelRW :: IORef TopLevelRW + , rProofState :: Maybe (IORef ProofState) } -- | Initial, empty environment. @@ -127,11 +126,11 @@ defaultRefs isBatch opts = contRef <- newIORef True rwRef <- newIORef rw return Refs - { eContinue = contRef - , eIsBatch = isBatch - , eTopLevelRO = ro - , environment = rwRef - , proofState = Nothing + { rContinue = contRef + , rIsBatch = isBatch + , rTopLevelRO = ro + , rTopLevelRW = rwRef + , rProofState = Nothing } @@ -158,11 +157,11 @@ subshell (REPL m) = TopLevel_ $ do contRef <- newIORef True rwRef <- newIORef rw let refs = Refs - { eContinue = contRef - , eIsBatch = False - , eTopLevelRO = ro - , environment = rwRef - , proofState = Nothing + { rContinue = contRef + , rIsBatch = False + , rTopLevelRO = ro + , rTopLevelRW = rwRef + , rProofState = Nothing } m refs readIORef rwRef @@ -178,11 +177,11 @@ proof_subshell (REPL m) = rwRef <- newIORef rw proofRef <- newIORef proofSt let refs = Refs - { eContinue = contRef - , eIsBatch = False - , eTopLevelRO = ro - , environment = rwRef - , proofState = Just proofRef + { rContinue = contRef + , rIsBatch = False + , rTopLevelRO = ro + , rTopLevelRW = rwRef + , rProofState = Just proofRef } m refs (,) <$> readIORef rwRef <*> readIORef proofRef @@ -291,7 +290,7 @@ rethrowEvalError m = run `X.catch` rethrow exceptionProtect :: REPL () -> REPL () exceptionProtect cmd = - do chk <- io . makeCheckpoint =<< getEnvironment + do chk <- io . makeCheckpoint =<< getTopLevelRW cmd `catch` (handlerPP chk) `catchFail` (handlerFail chk) `catchOther` (handlerPrint chk) @@ -312,7 +311,7 @@ exceptionProtect cmd = liftTopLevel :: TopLevel a -> REPL a liftTopLevel m = do ro <- getTopLevelRO - ref <- getEnvironmentRef + ref <- getTopLevelRWRef io $ do rw <- readIORef ref (a, rw') <- runTopLevel m ro rw writeIORef ref rw' @@ -347,7 +346,7 @@ modifyRef r f = REPL (\refs -> modifyIORef (r refs) f) -- | Construct the prompt for the current environment. getPrompt :: REPL String getPrompt = - do batch <- REPL (return . eIsBatch) + do batch <- REPL (return . rIsBatch) if batch then return "" else getProofStateRef >>= \case @@ -357,14 +356,14 @@ getPrompt = return ("proof ("++show (length (psGoals ps))++")> ") shouldContinue :: REPL Bool -shouldContinue = readRef eContinue +shouldContinue = readRef rContinue stop :: REPL () -stop = modifyRef eContinue (const False) +stop = modifyRef rContinue (const False) unlessBatch :: REPL () -> REPL () unlessBatch body = - do batch <- REPL (return . eIsBatch) + do batch <- REPL (return . rIsBatch) unless batch body setREPLTitle :: REPL () @@ -456,56 +455,58 @@ setModuleEnv :: M.ModuleEnv -> REPL () setModuleEnv me = modifyCryptolEnv (\ce -> ce { eModuleEnv = me }) getCryptolEnv :: REPL CryptolEnv -getCryptolEnv = rwCryptol `fmap` getEnvironment +getCryptolEnv = do + rw <- getTopLevelRW + return $ rwGetCryptolEnv rw modifyCryptolEnv :: (CryptolEnv -> CryptolEnv) -> REPL () -modifyCryptolEnv f = modifyEnvironment (\rw -> rw { rwCryptol = f (rwCryptol rw) }) +modifyCryptolEnv f = + modifyTopLevelRW $ rwModifyCryptolEnv f setCryptolEnv :: CryptolEnv -> REPL () setCryptolEnv x = modifyCryptolEnv (const x) getSharedContext :: REPL SharedContext -getSharedContext = rwSharedContext <$> getEnvironment +getSharedContext = rwSharedContext <$> getTopLevelRW getTopLevelRO :: REPL TopLevelRO -getTopLevelRO = REPL (return . eTopLevelRO) +getTopLevelRO = REPL (return . rTopLevelRO) -getEnvironmentRef :: REPL (IORef TopLevelRW) -getEnvironmentRef = environment <$> getRefs +getTopLevelRWRef :: REPL (IORef TopLevelRW) +getTopLevelRWRef = rTopLevelRW <$> getRefs getProofStateRef :: REPL (Maybe (IORef ProofState)) -getProofStateRef = proofState <$> getRefs - -getEnvironment :: REPL TopLevelRW -getEnvironment = readRef environment +getProofStateRef = rProofState <$> getRefs -getValueEnvironment :: REPL TopLevelRW -getValueEnvironment = - do rw <- getEnvironment - io (mergeLocalEnv (rwSharedContext rw) (rwLocalEnv rw) rw) +getTopLevelRW :: REPL TopLevelRW +getTopLevelRW = readRef rTopLevelRW -putEnvironment :: TopLevelRW -> REPL () -putEnvironment = modifyEnvironment . const +putTopLevelRW :: TopLevelRW -> REPL () +putTopLevelRW = modifyTopLevelRW . const -modifyEnvironment :: (TopLevelRW -> TopLevelRW) -> REPL () -modifyEnvironment = modifyRef environment +modifyTopLevelRW :: (TopLevelRW -> TopLevelRW) -> REPL () +modifyTopLevelRW = modifyRef rTopLevelRW -- | Get visible variable names for Haskeline completion. getSAWScriptValueNames :: REPL [String] getSAWScriptValueNames = do - env <- getEnvironment - let avail = rwPrimsAvail env - visible (_, lc, _, _, _, _) = Set.member lc avail - let rnames = Map.keys $ Map.filter visible $ rwValueInfo env - return (map Text.unpack rnames) + rw <- getTopLevelRW + let avail = rwPrimsAvail rw + visible (_, lc, _, _, _) = Set.member lc avail + Environ valenv _tyenv _cryenv = rwEnviron rw + rbenv = rwRebindables rw + let rnames1 = ScopedMap.allKeys $ ScopedMap.filter visible valenv + rnames2 = Map.keys rbenv + return (map Text.unpack (rnames1 ++ rnames2)) -- | Get visible type names for Haskeline completion. getSAWScriptTypeNames :: REPL [String] getSAWScriptTypeNames = do - env <- getEnvironment - let avail = rwPrimsAvail env + rw <- getTopLevelRW + let avail = rwPrimsAvail rw visible (lc, _) = Set.member lc avail - let rnames = Map.keys $ Map.filter visible $ rwTypeInfo env + Environ _valenv tyenv _cryenv = rwEnviron rw + let rnames = ScopedMap.allKeys $ ScopedMap.filter visible tyenv return (map Text.unpack rnames) -- User Environment Interaction ------------------------------------------------ diff --git a/saw-script/src/SAWScript/Search.hs b/saw-script/src/SAWScript/Search.hs index 9bc3b771cf..42b8990bd1 100644 --- a/saw-script/src/SAWScript/Search.hs +++ b/saw-script/src/SAWScript/Search.hs @@ -22,8 +22,10 @@ import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set +import qualified SAWSupport.ScopedMap as ScopedMap import SAWCentral.AST import SAWCentral.ASTUtil (namedTyVars) +import SAWCentral.Value (TyEnv) import SAWScript.Panic (panic) -- @@ -472,17 +474,6 @@ matchFragList ctx cand0 tgtType patTypes = ------------------------------------------------------------ -- External interface {{{ --- short name for the environment type we use --- --- Let this be polymorphic in the things it carries because all we --- need from it is the keys. --- --- (XXX: this type really belongs to the interpreter and should really --- be in its public interface or shared from somewhere else, but that --- requires the interpreter to have an interface, which requires --- still-pending interpreter cleanup) -type TyEnv a = Map Name a - -- | Check and compile a type schema pattern. -- -- We get passed a list of forall bindings (will often be empty) @@ -493,10 +484,10 @@ type TyEnv a = Map Name a -- different match semantics from forall-bound type variables. See -- notes at the top of the file. -- -compileSearchPattern :: TyEnv a -> SchemaPattern -> SearchPattern +compileSearchPattern :: TyEnv -> SchemaPattern -> SearchPattern compileSearchPattern tyEnv (SchemaPattern forallList tys) = let foralls = Set.fromList $ map (\(_pos, name) -> name) forallList - boundVars = Map.keysSet tyEnv + boundVars = ScopedMap.allKeysSet tyEnv -- treat '_' as a bound var to avoid assorted confusion boundVars' = Set.insert "_" boundVars oneType ty freeVarsSoFar = diff --git a/saw-script/src/SAWScript/Typechecker.hs b/saw-script/src/SAWScript/Typechecker.hs index 4a79eba017..e068712e6a 100644 --- a/saw-script/src/SAWScript/Typechecker.hs +++ b/saw-script/src/SAWScript/Typechecker.hs @@ -41,7 +41,7 @@ import SAWSupport.Pretty (pShow) import qualified SAWSupport.Pretty as PPS import SAWCentral.AST -import SAWCentral.ASTUtil (namedTyVars, SubstituteTyVars(..), isDeprecated) +import SAWCentral.ASTUtil (namedTyVars, SubstituteTyVars'(..), isDeprecated) import SAWScript.Panic (panic) import SAWCentral.Position (Inference(..), Pos(..), Positioned(..), choosePos) @@ -416,11 +416,11 @@ applyCurrentSubst t = do -- -- The type t has already been checked, so it's ok to panic if it refers -- to something in the typedef collection that's not visible. -resolveCurrentTypedefs :: SubstituteTyVars t => t -> TI t +resolveCurrentTypedefs :: SubstituteTyVars' t => t -> TI t resolveCurrentTypedefs t = do avail <- asks primsAvail s <- gets tyEnv - return $ substituteTyVars avail s t + return $ substituteTyVars' avail s t -- Get the unification vars that are used in the current variable typing -- and named type environments. @@ -1156,7 +1156,7 @@ inferExpr (ln, expr) = case expr of at <- getFreshTyVar apos return (a, (Current, ConcreteType at)) substs <- mapM once as - let t' = substituteTyVars avail (M.fromList substs) t + let t' = substituteTyVars' avail (M.fromList substs) t return (Var pos x, t') | otherwise -> do recordError pos $ "Inaccessible variable: " ++ show x ++ " (" ++ show pos ++ ")" @@ -1307,7 +1307,7 @@ addTypedef :: Name -> Type -> TI () addTypedef a ty = do avail <- asks primsAvail env <- gets tyEnv - let ty' = substituteTyVars avail env ty + let ty' = substituteTyVars' avail env ty env' = M.insert a (Current, ConcreteType ty') env modify (\rw -> rw { tyEnv = env' }) @@ -1997,7 +1997,7 @@ typesMatch avail tenv schema'found schema'expected = return (a, (Current, ConcreteType ty'a)) substs <- mapM generate as -- Substitute them into the type - let ty' = substituteTyVars avail (M.fromList substs) ty + let ty' = substituteTyVars' avail (M.fromList substs) ty return ty' match = do -- Unpack the schemas and check if they match diff --git a/saw-script/src/SAWScript/ValueOps.hs b/saw-script/src/SAWScript/ValueOps.hs index e05b2e3db4..9e96a9f857 100644 --- a/saw-script/src/SAWScript/ValueOps.hs +++ b/saw-script/src/SAWScript/ValueOps.hs @@ -22,10 +22,6 @@ module SAWScript.ValueOps ( -- used by SAWScript.Interpreter tupleLookupValue, -- used by SAWScript.Interpreter - emptyLocal, - -- used by SAWScript.Interpreter - extendLocal, - -- used by SAWScript.Interpreter bracketTopLevel, -- unused but that probably won't stay that way TopLevelCheckpoint(..), @@ -38,17 +34,18 @@ module SAWScript.ValueOps ( -- used by SAWScript.Interpreter proof_checkpoint, -- used by SAWScript.Interpreter - withLocalEnv, - withLocalEnvProof, - withLocalEnvLLVM, - withLocalEnvJVM, - withLocalEnvMIR, + withEnviron, + withEnvironProofScript, + withEnvironLLVM, + withEnvironJVM, + withEnvironMIR, -- used in SAWScript.Interpreter withOptions, ) where import Prelude hiding (fail) +import Control.Monad (zipWithM) import Control.Monad.Catch (MonadThrow(..), try) import Control.Monad.State (get, gets, modify, put) import qualified Control.Exception as X @@ -66,7 +63,7 @@ import SAWCore.SharedTerm import CryptolSAWCore.CryptolEnv as CEnv import qualified SAWCentral.Position as SS -import qualified SAWCentral.AST as SS +--import qualified SAWCentral.AST as SS --import qualified SAWCentral.Crucible.JVM.MethodSpecIR () --import qualified SAWCentral.Crucible.MIR.MethodSpecIR () import SAWCentral.Options (Options, Verbosity(..)) @@ -118,12 +115,6 @@ tupleLookupValue pos v1 v2 = "Index value: " <> Text.pack (show v2) ] -emptyLocal :: LocalEnv -emptyLocal = [] - -extendLocal :: SS.Pos -> SS.Name -> SS.Rebindable -> SS.Schema -> Maybe [Text] -> Value -> LocalEnv -> LocalEnv -extendLocal pos x rb ty md v env = LocalLet pos x rb ty md v : env - -- | A version of 'Control.Exception.bracket' specialized to 'TopLevel'. We -- can't use 'Control.Monad.Catch.bracket' because it requires 'TopLevel' to -- implement 'Control.Monad.Catch.MonadMask', which it can't do. @@ -134,13 +125,25 @@ bracketTopLevel acquire release action = Left (bad :: X.SomeException) -> release resource >> throwM bad Right good -> release resource >> pure good +-- Note: this is used only by restoreCheckpoint and restoreCheckpoint is +-- not really expected to work. +-- +-- This is good, because whatever this function is doing does not seem +-- to make a great deal of sense. (Which has become more overt with recent +-- reorgs and cleanup, but hasn't itself changed.) combineRW :: TopLevelCheckpoint -> TopLevelRW -> IO TopLevelRW -combineRW (TopLevelCheckpoint chk scc) rw = - do cenv' <- CEnv.combineCryptolEnv (rwCryptol chk) (rwCryptol rw) +combineRW (TopLevelCheckpoint chk scc) rw = do + let CryptolEnvStack chk'cenv chk'cenvs = rwGetCryptolEnvStack chk + CryptolEnvStack rw'cenv rw'cenvs = rwGetCryptolEnvStack rw + -- Caution: this merge may have unexpected results if the + -- number of scopes doesn't match. But, it doesn't make sense + -- to do that in the first place. Caveat emptor... + cenv' <- CEnv.combineCryptolEnv chk'cenv rw'cenv + cenvs' <- zipWithM CEnv.combineCryptolEnv chk'cenvs rw'cenvs sc' <- restoreSharedContext scc (rwSharedContext rw) - return chk{ rwCryptol = cenv' - , rwSharedContext = sc' - } + let cryenv' = CryptolEnvStack cenv' cenvs' + let chk' = rwSetCryptolEnvStack cryenv' chk + return chk' { rwSharedContext = sc' } -- | Represents the mutable state of the TopLevel monad -- that can later be restored. @@ -179,29 +182,29 @@ proof_checkpoint = do scriptTopLevel (printOutLnTop Info "Restoring proof state from checkpoint") put ps -withLocalEnv :: LocalEnv -> TopLevel a -> TopLevel a -withLocalEnv env m = do - prevEnv <- gets rwLocalEnv - modify (\rw -> rw { rwLocalEnv = env }) +withEnviron :: Environ -> TopLevel a -> TopLevel a +withEnviron env m = do + prevEnv <- gets rwEnviron + modify (\rw -> rw { rwEnviron = env }) result <- m - modify (\rw -> rw { rwLocalEnv = prevEnv }) + modify (\rw -> rw { rwEnviron = prevEnv }) return result -withLocalEnvProof :: LocalEnv -> ProofScript a -> ProofScript a -withLocalEnvProof env (ProofScript m) = do - ProofScript (underExceptT (underStateT (withLocalEnv env)) m) +withEnvironProofScript :: Environ -> ProofScript a -> ProofScript a +withEnvironProofScript env (ProofScript m) = do + ProofScript (underExceptT (underStateT (withEnviron env)) m) -withLocalEnvLLVM :: LocalEnv -> LLVMCrucibleSetupM a -> LLVMCrucibleSetupM a -withLocalEnvLLVM env (LLVMCrucibleSetupM m) = do - LLVMCrucibleSetupM (underReaderT (underStateT (withLocalEnv env)) m) +withEnvironLLVM :: Environ -> LLVMCrucibleSetupM a -> LLVMCrucibleSetupM a +withEnvironLLVM env (LLVMCrucibleSetupM m) = do + LLVMCrucibleSetupM (underReaderT (underStateT (withEnviron env)) m) -withLocalEnvJVM :: LocalEnv -> JVMSetupM a -> JVMSetupM a -withLocalEnvJVM env (JVMSetupM m) = do - JVMSetupM (underReaderT (underStateT (withLocalEnv env)) m) +withEnvironJVM :: Environ -> JVMSetupM a -> JVMSetupM a +withEnvironJVM env (JVMSetupM m) = do + JVMSetupM (underReaderT (underStateT (withEnviron env)) m) -withLocalEnvMIR :: LocalEnv -> MIRSetupM a -> MIRSetupM a -withLocalEnvMIR env (MIRSetupM m) = do - MIRSetupM (underReaderT (underStateT (withLocalEnv env)) m) +withEnvironMIR :: Environ -> MIRSetupM a -> MIRSetupM a +withEnvironMIR env (MIRSetupM m) = do + MIRSetupM (underReaderT (underStateT (withEnviron env)) m) withOptions :: (Options -> Options) -> TopLevel a -> TopLevel a withOptions f (TopLevel_ m) = diff --git a/saw-server/src/SAWServer/CryptolExpression.hs b/saw-server/src/SAWServer/CryptolExpression.hs index b18f27cc44..8d7bb95c4f 100644 --- a/saw-server/src/SAWServer/CryptolExpression.hs +++ b/saw-server/src/SAWServer/CryptolExpression.hs @@ -30,7 +30,7 @@ import Cryptol.TypeCheck.Solver.SMT (withSolver) import Cryptol.Utils.Ident (interactiveName) import Cryptol.Utils.Logger (quietLogger) import Cryptol.Utils.PP ( defaultPPOpts, pp ) -import SAWCentral.Value (biSharedContext, TopLevelRW(..)) +import SAWCentral.Value (biSharedContext, rwGetCryptolEnv) import CryptolSAWCore.CryptolEnv ( getAllIfaceDecls, getNamingEnv, @@ -48,8 +48,8 @@ import CryptolServer.Exceptions (cryptolError) import SAWServer.SAWServer getTypedTerm :: Expression -> Argo.Command SAWState TypedTerm -getTypedTerm inputExpr = - do cenv <- rwCryptol . view sawTopLevelRW <$> Argo.getState +getTypedTerm inputExpr = do + cenv <- rwGetCryptolEnv . view sawTopLevelRW <$> Argo.getState fileReader <- Argo.getFileReader expr <- getCryptolExpr inputExpr sc <- biSharedContext . view sawBIC <$> Argo.getState diff --git a/saw-server/src/SAWServer/CryptolSetup.hs b/saw-server/src/SAWServer/CryptolSetup.hs index 4340489eec..c7e15c4cbe 100644 --- a/saw-server/src/SAWServer/CryptolSetup.hs +++ b/saw-server/src/SAWServer/CryptolSetup.hs @@ -18,7 +18,7 @@ import qualified Data.Text as T import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (textToModName) -import SAWCentral.Value (biSharedContext, rwCryptol) +import SAWCentral.Value (biSharedContext, rwGetCryptolEnv, rwSetCryptolEnv) import qualified CryptolSAWCore.CryptolEnv as CEnv import qualified Argo @@ -36,7 +36,8 @@ cryptolLoadModuleDescr = cryptolLoadModule :: CryptolLoadModuleParams -> Argo.Command SAWState OK cryptolLoadModule (CryptolLoadModuleParams modName) = do sc <- biSharedContext . view sawBIC <$> Argo.getState - cenv <- rwCryptol . view sawTopLevelRW <$> Argo.getState + rw <- view sawTopLevelRW <$> Argo.getState + let cenv = rwGetCryptolEnv rw let qual = Nothing -- TODO add field to params let importSpec = Nothing -- TODO add field to params fileReader <- Argo.getFileReader @@ -45,7 +46,7 @@ cryptolLoadModule (CryptolLoadModuleParams modName) = case cenv' of Left (ex :: SomeException) -> Argo.raise $ cryptolError (show ex) Right cenv'' -> - do Argo.modifyState $ over sawTopLevelRW $ \rw -> rw { rwCryptol = cenv'' } + do Argo.modifyState $ over sawTopLevelRW $ rwSetCryptolEnv cenv'' ok newtype CryptolLoadModuleParams = @@ -71,7 +72,8 @@ cryptolLoadFileDescr = cryptolLoadFile :: CryptolLoadFileParams -> Argo.Command SAWState OK cryptolLoadFile (CryptolLoadFileParams fileName) = do sc <- biSharedContext . view sawBIC <$> Argo.getState - cenv <- rwCryptol . view sawTopLevelRW <$> Argo.getState + rw <- view sawTopLevelRW <$> Argo.getState + let cenv = rwGetCryptolEnv rw let qual = Nothing -- TODO add field to params let importSpec = Nothing -- TODO add field to params fileReader <- Argo.getFileReader @@ -80,7 +82,7 @@ cryptolLoadFile (CryptolLoadFileParams fileName) = case cenv' of Left (ex :: SomeException) -> Argo.raise $ cryptolError (show ex) Right cenv'' -> - do Argo.modifyState $ over sawTopLevelRW $ \rw -> rw { rwCryptol = cenv'' } + do Argo.modifyState $ over sawTopLevelRW $ rwSetCryptolEnv cenv'' ok newtype CryptolLoadFileParams = diff --git a/saw-server/src/SAWServer/Eval.hs b/saw-server/src/SAWServer/Eval.hs index d7f211843f..399eab9dd8 100644 --- a/saw-server/src/SAWServer/Eval.hs +++ b/saw-server/src/SAWServer/Eval.hs @@ -80,7 +80,7 @@ eval :: eval f params = do state <- Argo.getState fileReader <- Argo.getFileReader - let cenv = SV.rwCryptol (view sawTopLevelRW state) + let cenv = SV.rwGetCryptolEnv (view sawTopLevelRW state) bic = view sawBIC state cexp <- getCryptolExpr $ evalExpr params (eterm, warnings) <- liftIO $ getTypedTermOfCExp fileReader (SV.biSharedContext bic) cenv cexp diff --git a/saw-server/src/SAWServer/JVMVerify.hs b/saw-server/src/SAWServer/JVMVerify.hs index c556f74f2f..8cb7221447 100644 --- a/saw-server/src/SAWServer/JVMVerify.hs +++ b/saw-server/src/SAWServer/JVMVerify.hs @@ -14,7 +14,7 @@ import qualified Data.Map as Map import SAWCentral.Crucible.JVM.Builtins ( jvm_unsafe_assume_spec, jvm_verify ) import SAWCentral.JavaExpr (JavaType(..)) -import SAWCentral.Value (rwCryptol) +import SAWCentral.Value (rwGetCryptolEnv) import qualified Argo import qualified Argo.Doc as Doc @@ -51,7 +51,7 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc state <- Argo.getState cls <- getJVMClass className let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) + cenv = rwGetCryptolEnv (view sawTopLevelRW state) fileReader <- Argo.getFileReader ghostEnv <- Map.fromList <$> getGhosts setup <- compileJVMContract fileReader bic ghostEnv cenv <$> traverse getCryptolExpr contract diff --git a/saw-server/src/SAWServer/LLVMVerify.hs b/saw-server/src/SAWServer/LLVMVerify.hs index f9623ff2ab..4f8491e6f8 100644 --- a/saw-server/src/SAWServer/LLVMVerify.hs +++ b/saw-server/src/SAWServer/LLVMVerify.hs @@ -16,7 +16,7 @@ import qualified Data.Map as Map import SAWCentral.Crucible.LLVM.Builtins ( llvm_unsafe_assume_spec, llvm_verify ) import SAWCentral.Crucible.LLVM.X86 ( llvm_verify_x86 ) -import SAWCentral.Value (rwCryptol) +import SAWCentral.Value (rwGetCryptolEnv) import qualified Argo import qualified Argo.Doc as Doc @@ -57,7 +57,7 @@ llvmVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scr state <- Argo.getState mod <- getLLVMModule modName let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) + cenv = rwGetCryptolEnv (view sawTopLevelRW state) fileReader <- Argo.getFileReader ghostEnv <- Map.fromList <$> getGhosts setup <- compileLLVMContract fileReader bic ghostEnv cenv <$> @@ -113,7 +113,7 @@ llvmVerifyX86 (X86VerifyParams modName objName fun globals _lemmaNames checkSat state <- Argo.getState mod <- getLLVMModule modName let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) + cenv = rwGetCryptolEnv (view sawTopLevelRW state) allocs = map (\(X86Alloc name size) -> (name, size)) globals proofScript <- interpretProofScript script fileReader <- Argo.getFileReader diff --git a/saw-server/src/SAWServer/MIRVerify.hs b/saw-server/src/SAWServer/MIRVerify.hs index 69ed710603..f29f6604d5 100644 --- a/saw-server/src/SAWServer/MIRVerify.hs +++ b/saw-server/src/SAWServer/MIRVerify.hs @@ -13,7 +13,7 @@ import qualified Data.Map as Map import SAWCentral.Crucible.MIR.Builtins ( mir_unsafe_assume_spec, mir_verify ) -import SAWCentral.Value (rwCryptol) +import SAWCentral.Value (rwGetCryptolEnv) import qualified Argo import qualified Argo.Doc as Doc @@ -52,7 +52,7 @@ mirVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scri state <- Argo.getState rm <- getMIRModule modName let bic = view sawBIC state - cenv = rwCryptol (view sawTopLevelRW state) + cenv = rwGetCryptolEnv (view sawTopLevelRW state) sawenv = view sawEnv state fileReader <- Argo.getFileReader ghostEnv <- Map.fromList <$> getGhosts diff --git a/saw-server/src/SAWServer/ProofScript.hs b/saw-server/src/SAWServer/ProofScript.hs index afa597b62a..90195b4041 100644 --- a/saw-server/src/SAWServer/ProofScript.hs +++ b/saw-server/src/SAWServer/ProofScript.hs @@ -259,7 +259,7 @@ prove :: ProveParams Expression -> Argo.Command SAWState ProveResult prove params = do state <- Argo.getState fileReader <- Argo.getFileReader - let cenv = SV.rwCryptol (view sawTopLevelRW state) + let cenv = SV.rwGetCryptolEnv (view sawTopLevelRW state) bic = view sawBIC state cexp <- getCryptolExpr (ppGoal params) (eterm, warnings) <- liftIO $ getTypedTermOfCExp fileReader (SV.biSharedContext bic) cenv cexp diff --git a/saw-server/src/SAWServer/SAWServer.hs b/saw-server/src/SAWServer/SAWServer.hs index a2275b688b..f5325c77ab 100644 --- a/saw-server/src/SAWServer/SAWServer.hs +++ b/saw-server/src/SAWServer/SAWServer.hs @@ -44,6 +44,7 @@ import Mir.Generator (RustModule) import Mir.Intrinsics (MIR) import Mir.Mir (Adt) +import qualified SAWSupport.ScopedMap as ScopedMap import qualified SAWSupport.Pretty as PPS (defaultOpts) import qualified SAWCentral.Trace as Trace (empty) @@ -63,7 +64,7 @@ import SAWCentral.Options (processEnv, defaultOptions) import SAWCentral.Position (Pos(..)) import SAWCentral.Prover.Rewrite (basic_ss) import SAWCentral.Proof (emptyTheoremDB) -import SAWCentral.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), SAWSimpset,JavaCodebase(..)) +import SAWCentral.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, Environ(..), TopLevelRO(..), TopLevelRW(..), SAWSimpset, JavaCodebase(..), CryptolEnvStack(..), rwModifyCryptolEnv) import SAWCentral.Yosys.State (YosysSequential) import SAWCentral.Yosys.Theorem (YosysImport, YosysTheorem) import qualified CryptolSAWCore.Prelude as CryptolSAW @@ -222,6 +223,7 @@ initialState readFileFn = , biBasicSS = ss } cenv <- initCryptolEnv sc + let cryenvs = CryptolEnvStack cenv [] halloc <- Crucible.newHandleAllocator jvmTrans <- CJ.mkInitialJVMContext halloc cwd <- getCurrentDirectory @@ -243,12 +245,10 @@ initialState readFileFn = , roProofSubshell = fail "SAW server does not support subshells." } rw = TopLevelRW - { rwValueInfo = mempty - , rwTypeInfo = mempty - , rwCryptol = cenv + { rwEnviron = Environ ScopedMap.empty ScopedMap.empty cryenvs + , rwRebindables = M.empty , rwPosition = PosInternal "SAWServer" , rwStackTrace = Trace.empty - , rwLocalEnv = [] , rwPPOpts = PPS.defaultOpts , rwSolverCache = mb_cache , rwTheoremDB = emptyTheoremDB @@ -457,8 +457,8 @@ getServerValEither (SAWEnv serverEnv) n = bindCryptolVar :: Text -> TypedTerm -> Argo.Command SAWState () bindCryptolVar x t = - do Argo.modifyState $ over sawTopLevelRW $ \rw -> - rw { rwCryptol = bindTypedTerm (Cryptol.mkIdent x, t) (rwCryptol rw) } + do Argo.modifyState $ over sawTopLevelRW $ rwModifyCryptolEnv $ \cenv -> + bindTypedTerm (Cryptol.mkIdent x, t) cenv getJVMClass :: ServerName -> Argo.Command SAWState JSS.Class getJVMClass n = diff --git a/saw-server/src/SAWServer/Yosys.hs b/saw-server/src/SAWServer/Yosys.hs index 91f9210ee5..158e3d527d 100644 --- a/saw-server/src/SAWServer/Yosys.hs +++ b/saw-server/src/SAWServer/Yosys.hs @@ -30,7 +30,7 @@ import SAWServer.OK (OK, ok) import SAWServer.ProofScript (ProofScript, interpretProofScript) import SAWServer.TopLevel (tl) -import SAWCentral.Value (getSharedContext, getTopLevelRW, rwCryptol) +import SAWCentral.Value (getSharedContext, getTopLevelRW, rwGetCryptolEnv, rwModifyCryptolEnv) import SAWCentral.Yosys (loadYosysIR, yosysIRToTypedTerms, yosys_verify, yosys_import_sequential, yosys_extract_sequential) import SAWCentral.Yosys.Theorem (YosysImport(..)) @@ -121,7 +121,7 @@ yosysVerify params = do l <- tl $ do rw <- getTopLevelRW sc <- getSharedContext - let cenv = rwCryptol rw + let cenv = rwGetCryptolEnv rw preconds <- forM precondExprs $ \pc -> do (eterm, warnings) <- liftIO $ getTypedTermOfCExp fileReader sc cenv pc case eterm of @@ -205,7 +205,8 @@ yosysExtractSequential params = do m <- getYosysSequential $ yosysExtractSequentialModule params s <- tl $ yosys_extract_sequential m (yosysExtractSequentialCycles params) let sn@(ServerName n) = yosysExtractSequentialServerName params - sawTopLevelRW %= \rw -> rw { rwCryptol = CEnv.bindTypedTerm (mkIdent n, s) $ rwCryptol rw } + doBind cenv = CEnv.bindTypedTerm (mkIdent n, s) cenv + sawTopLevelRW %= rwModifyCryptolEnv doBind setServerVal sn s ok diff --git a/saw-support/src/SAWSupport/Panic.hs b/saw-support/src/SAWSupport/Panic.hs new file mode 100644 index 0000000000..ab25d2e0c4 --- /dev/null +++ b/saw-support/src/SAWSupport/Panic.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE OverloadedStrings #-} +{- | +Module : SAWSupport.Panic +License : BSD3 +Maintainer : saw@galois.com +Stability : provisional +-} + +module SAWSupport.Panic (panic) where + +import Data.Text (Text) + +import SAWSupport.PanicSupport + +-- | Raise a fatal error. See commentary in PanicSupport. +-- Arguments are "location" (one string) and "description" (multiple +-- strings). +panic :: HasCallStack => Text -> [Text] -> a +panic loc descs = doPanic "saw-support" loc descs diff --git a/saw-support/src/SAWSupport/ScopedMap.hs b/saw-support/src/SAWSupport/ScopedMap.hs new file mode 100644 index 0000000000..6d314a94f2 --- /dev/null +++ b/saw-support/src/SAWSupport/ScopedMap.hs @@ -0,0 +1,160 @@ +{-# LANGUAGE OverloadedStrings #-} + +-- | +-- Module : SAWSupport.ScopedMap +-- Description : Scoped-aware finite map library +-- License : BSD3 +-- Maintainer : saw@galois.com +-- Stability : provisional +-- +-- Scope-aware map for use as an interpreter or typechecker +-- environment. +-- +-- The `ScopedMap` type is a stack of maps; each layer corresponds +-- to a scope as the client moves into and out of nested naming +-- environments. +-- +-- The current (innermost) scope is at the top of the stack / head of +-- the list. +-- +-- Update operations act on the current scope. Lookup operations +-- inspect the whole stack, starting at the innermost layer and +-- working out. +-- +-- The `push` and `pop` operations add and drop scopes respectively, +-- and should be used when the client enters and leaves a nested +-- naming environment. +-- +-- The `flatten` operation produces a single-layer Data.Map that +-- contains all the visible mappings. (That is, duplicate keys in +-- outer scopes are suppressed.) +-- +-- Other operations correspond to the ordinary operations on +-- Data.Map. Operations that generate collections (e.g. @keys@) come +-- in two versions: one that preserves the scope structure +-- (generally called @scoped@), and one that flattens it (generally +-- called @all@). +-- +-- In principle we should provide all the operations on Data.Map. +-- However, the implementation has been lazily evaluated and the +-- operations present are the ones that have been needed so far. +-- Add more as desired. + +module SAWSupport.ScopedMap ( + ScopedMap, -- opaque + push, + pop, + empty, + seed, + insert, + lookup, + filter, + scopedAssocs, + flatten, + allKeys, + allKeysSet + ) where + +import Prelude hiding (lookup, filter) + +import qualified Data.List.NonEmpty as N +import Data.List.NonEmpty (NonEmpty( (:|) )) +import Data.Foldable (toList) +--import qualified Data.Set as Set +import Data.Set (Set) +import qualified Data.Map as Map +import Data.Map (Map) + +import SAWSupport.Panic (panic) + + +-- | The type of scoped maps. +-- +-- The list of scopes is a `NonEmpty` to avoid unnecessary +-- degenerate cases. +newtype ScopedMap k v = ScopedMap (NonEmpty (Map k v)) + +-- | Push a new scope. +push :: Ord k => ScopedMap k v -> ScopedMap k v +push (ScopedMap scopes) = + ScopedMap $ N.cons Map.empty scopes + +-- | Pop and discard the most recent scope. +-- +-- Popping the last scope is an error and will panic. +pop :: Ord k => ScopedMap k v -> ScopedMap k v +pop (ScopedMap (_ :| more)) = case more of + [] -> + panic "pop" ["Popping topmost scope"] + s : more' -> + ScopedMap (s :| more') + +-- | An empty ScopedMap, with a single empty scope. +empty :: Ord k => ScopedMap k v +empty = + ScopedMap (Map.empty :| []) + +-- | Initialize a ScopedMap from a Map, which becomes the current (and +-- only) scope. +seed :: Ord k => Map k v -> ScopedMap k v +seed m = + ScopedMap (m :| []) + +-- | Insert into a ScopedMap. Always inserts in the innermost (most +-- recent) scope. +insert :: Ord k => k -> v -> ScopedMap k v -> ScopedMap k v +insert k v (ScopedMap (s :| more)) = + let s' = Map.insert k v s in + ScopedMap (s' :| more) + +-- | Look up a key in a ScopedMap. Checks all the scopes with the most +-- recent first. +lookup :: Ord k => k -> ScopedMap k v -> Maybe v +lookup k (ScopedMap (s0 :| more0)) = + let visit s more = case Map.lookup k s of + Just result -> Just result + Nothing -> case more of + [] -> Nothing + s' : more' -> visit s' more' + in + visit s0 more0 + +-- | Drop entries that don't match a predicate. +filter :: Ord k => (v -> Bool) -> ScopedMap k v -> ScopedMap k v +filter keep (ScopedMap (s :| more)) = + ScopedMap (Map.filter keep s :| map (Map.filter keep) more) + +-- | Return Map.assocs for each scope, preserving the scope boundaries. +-- The head of the returned list is the most recent scope. +scopedAssocs :: Ord k => ScopedMap k v -> [[(k, v)]] +scopedAssocs (ScopedMap scopes) = + map Map.assocs $ toList scopes + +-- FUTURE: add scopedKeys, scopedKeysSet + +-- | Convert to a plain map by folding the scopes together. Duplicate +-- bindings in more recent scopes take priority. +flatten :: Ord k => ScopedMap k v -> Map k v +flatten (ScopedMap (s0 :| more0)) = + let visit s more = + let result = case more of + [] -> Map.empty + s' : more' -> visit s' more' + in + -- Map.union gives its left argument priority given a + -- duplicate key. + Map.union s result + in + visit s0 more0 + +--FUTURE: add allAssocs + +-- | Return all keys, ignoring scope. +allKeys :: Ord k => ScopedMap k v -> [k] +allKeys m = + Map.keys $ flatten m + +-- | Return all keys as a set, ignoring scope. +allKeysSet :: Ord k => ScopedMap k v -> Set k +allKeysSet m = + Map.keysSet $ flatten m diff --git a/saw.cabal b/saw.cabal index 607c8ed4e7..8f9219de39 100644 --- a/saw.cabal +++ b/saw.cabal @@ -87,6 +87,9 @@ library saw-support exposed-modules: SAWSupport.PanicSupport SAWSupport.Pretty + SAWSupport.ScopedMap + other-modules: + SAWSupport.Panic ------------------------------------------------------------