diff --git a/bin/main.ml b/bin/main.ml index 571a43c..09c677d 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -86,7 +86,12 @@ let run_smt_check env doc = let domain_bounds = Pantagruel.Smt.compute_domain_bounds !check_bound env in let config = Pantagruel.Smt. - { bound = !check_bound; steps = !check_steps; domain_bounds } + { + bound = !check_bound; + steps = !check_steps; + domain_bounds; + inject_guards = true; + } in let queries = Pantagruel.Smt.generate_queries config env doc in if !dump_smt_dir <> "" then begin diff --git a/lib/smt.ml b/lib/smt.ml index 96240d4..8b343e8 100644 --- a/lib/smt.ml +++ b/lib/smt.ml @@ -3,7 +3,12 @@ open Ast open Types -type config = { bound : int; steps : int; domain_bounds : int Env.StringMap.t } +type config = { + bound : int; + steps : int; + domain_bounds : int Env.StringMap.t; + inject_guards : bool; +} (** Configuration for bounded checking. [steps] controls k-step BMC depth. [domain_bounds] maps domain names to per-domain minimum bounds (derived from nullary constant counts). *) @@ -681,10 +686,63 @@ and substitute_guards subst gs = | GExpr e -> (subst, acc @ [ GExpr (substitute_vars subst e) ])) (subst, []) gs +(** Substitute primed names in an expression (for invariant checking in next + state). Tracks locally-bound names (from quantifiers) to avoid priming them. +*) +let rec prime_expr ?(bound = []) (e : expr) : expr = + match e with + | EVar name -> if List.mem name bound then e else EPrimed name + | EApp (func, args) -> + EApp (prime_expr ~bound func, List.map (prime_expr ~bound) args) + | EBinop (op, e1, e2) -> + EBinop (op, prime_expr ~bound e1, prime_expr ~bound e2) + | EUnop (op, e) -> EUnop (op, prime_expr ~bound e) + | ETuple es -> ETuple (List.map (prime_expr ~bound) es) + | EProj (e, i) -> EProj (prime_expr ~bound e, i) + | EForall (ps, gs, body) -> + let bound' = List.map (fun (p : param) -> p.param_name) ps @ bound in + let bound'', gs' = prime_guards ~bound:bound' gs in + EForall (ps, gs', prime_expr ~bound:bound'' body) + | EExists (ps, gs, body) -> + let bound' = List.map (fun (p : param) -> p.param_name) ps @ bound in + let bound'', gs' = prime_guards ~bound:bound' gs in + EExists (ps, gs', prime_expr ~bound:bound'' body) + | EEach (ps, gs, body) -> + let bound' = List.map (fun (p : param) -> p.param_name) ps @ bound in + let bound'', gs' = prime_guards ~bound:bound' gs in + EEach (ps, gs', prime_expr ~bound:bound'' body) + | ECond arms -> + ECond + (List.map + (fun (arm, cons) -> (prime_expr ~bound arm, prime_expr ~bound cons)) + arms) + | EOverride (name, pairs) -> + EOverride + ( name, + List.map + (fun (k, v) -> (prime_expr ~bound k, prime_expr ~bound v)) + pairs ) + | EInitially e -> EInitially (prime_expr ~bound e) + | EPrimed _ | ELitBool _ | ELitNat _ | ELitReal _ | ELitString _ | EDomain _ + | EQualified _ -> + e + +and prime_guards ~bound gs = + List.fold_left + (fun (bound, acc) g -> + match g with + | GParam p -> (p.param_name :: bound, acc @ [ GParam p ]) + | GIn (name, e) -> + (name :: bound, acc @ [ GIn (name, prime_expr ~bound e) ]) + | GExpr e -> (bound, acc @ [ GExpr (prime_expr ~bound e) ])) + (bound, []) gs + (** Collect guard expressions from applications of guarded functions in an expression. Stops at nested quantifiers (they handle their own guards). - Returns a list of AST guard expressions with actual args substituted. *) -let collect_body_guards env (e : expr) : expr list = + Returns a list of AST guard expressions with actual args substituted. + [~bound] tracks quantifier-bound variable names so that [prime_expr] inside + primed-application handling doesn't incorrectly prime them. *) +let collect_body_guards ?(bound = []) env (e : expr) : expr list = let guards = ref [] in let rec walk = function | EApp (EVar name, args) -> @@ -703,6 +761,25 @@ let collect_body_guards env (e : expr) : expr list = rule_guards | None -> ()); List.iter walk args + | EApp (EPrimed name, args) -> + (* Primed application: collect guards in primed form *) + (match Env.lookup_rule_guards name env with + | Some (formal_params, rule_guards) -> + let subst = + List.combine + (List.map (fun (p : param) -> p.param_name) formal_params) + args + in + List.iter + (fun (g : guard) -> + match g with + | GExpr ge -> + guards := + prime_expr ~bound (substitute_vars subst ge) :: !guards + | _ -> ()) + rule_guards + | None -> ()); + List.iter walk args | EApp (func, args) -> walk func; List.iter walk args @@ -718,6 +795,20 @@ let collect_body_guards env (e : expr) : expr list = rule_guards | None -> ()) | _ -> ()) + | EPrimed name -> ( + (* Nullary auto-applied primed rule with guards *) + match Env.lookup_term name env with + | Some { kind = Env.KRule (TyFunc ([], Some _)); _ } -> ( + match Env.lookup_rule_guards name env with + | Some (_, rule_guards) -> + List.iter + (fun (g : guard) -> + match g with + | GExpr ge -> guards := prime_expr ~bound ge :: !guards + | _ -> ()) + rule_guards + | None -> ()) + | _ -> ()) | EBinop (_, e1, e2) -> walk e1; walk e2 @@ -739,7 +830,7 @@ let collect_body_guards env (e : expr) : expr list = arms (* Stop at nested quantifiers — they inject their own guards *) | EForall _ | EExists _ | EEach _ -> () - | EPrimed _ | ELitBool _ | ELitNat _ | ELitReal _ | ELitString _ | EDomain _ + | ELitBool _ | ELitNat _ | ELitReal _ | ELitString _ | EDomain _ | EQualified _ -> () in @@ -1222,7 +1313,20 @@ and translate_quantifier config env quant params guards body = in let all_bindings = bindings @ List.rev guard_bindings in (* Collect guards from guarded function applications in body *) - let app_guards = collect_body_guards env body in + let bound_names = + List.map (fun (p : param) -> p.param_name) params + @ List.concat_map + (fun g -> + match g with + | GParam p -> [ p.param_name ] + | GIn (n, _) -> [ n ] + | GExpr _ -> []) + guards + in + let app_guards = + if config.inject_guards then collect_body_guards ~bound:bound_names env body + else [] + in let app_guard_strs = List.map (translate_expr config env) app_guards in let body_str = translate_expr config env body in let conditions = @@ -1285,18 +1389,20 @@ let translate_proposition config env (e : expr) = (* Quantifiers handle their own guard injection *) translate_expr config env e | _ -> ( - let app_guards = collect_body_guards env e in - let smt_expr = translate_expr config env e in - match app_guards with - | [] -> smt_expr - | _ -> - let guard_strs = List.map (translate_expr config env) app_guards in - let guard_conj = - match guard_strs with - | [ g ] -> g - | gs -> Printf.sprintf "(and %s)" (String.concat " " gs) - in - Printf.sprintf "(=> %s %s)" guard_conj smt_expr) + if not config.inject_guards then translate_expr config env e + else + let app_guards = collect_body_guards env e in + let smt_expr = translate_expr config env e in + match app_guards with + | [] -> smt_expr + | _ -> + let guard_strs = List.map (translate_expr config env) app_guards in + let guard_conj = + match guard_strs with + | [ g ] -> g + | gs -> Printf.sprintf "(and %s)" (String.concat " " gs) + in + Printf.sprintf "(=> %s %s)" guard_conj smt_expr) (** Classify chapters into invariant chapters and action chapters *) type chapter_class = @@ -1392,57 +1498,6 @@ let conjoin_propositions config env props = in Printf.sprintf "(and %s)" (String.concat " " parts) -(** Substitute primed names in an expression (for invariant checking in next - state). Tracks locally-bound names (from quantifiers) to avoid priming them. -*) -let rec prime_expr ?(bound = []) (e : expr) : expr = - match e with - | EVar name -> if List.mem name bound then e else EPrimed name - | EApp (func, args) -> - EApp (prime_expr ~bound func, List.map (prime_expr ~bound) args) - | EBinop (op, e1, e2) -> - EBinop (op, prime_expr ~bound e1, prime_expr ~bound e2) - | EUnop (op, e) -> EUnop (op, prime_expr ~bound e) - | ETuple es -> ETuple (List.map (prime_expr ~bound) es) - | EProj (e, i) -> EProj (prime_expr ~bound e, i) - | EForall (ps, gs, body) -> - let bound' = List.map (fun (p : param) -> p.param_name) ps @ bound in - let bound'', gs' = prime_guards ~bound:bound' gs in - EForall (ps, gs', prime_expr ~bound:bound'' body) - | EExists (ps, gs, body) -> - let bound' = List.map (fun (p : param) -> p.param_name) ps @ bound in - let bound'', gs' = prime_guards ~bound:bound' gs in - EExists (ps, gs', prime_expr ~bound:bound'' body) - | EEach (ps, gs, body) -> - let bound' = List.map (fun (p : param) -> p.param_name) ps @ bound in - let bound'', gs' = prime_guards ~bound:bound' gs in - EEach (ps, gs', prime_expr ~bound:bound'' body) - | ECond arms -> - ECond - (List.map - (fun (arm, cons) -> (prime_expr ~bound arm, prime_expr ~bound cons)) - arms) - | EOverride (name, pairs) -> - EOverride - ( name, - List.map - (fun (k, v) -> (prime_expr ~bound k, prime_expr ~bound v)) - pairs ) - | EInitially e -> EInitially (prime_expr ~bound e) - | EPrimed _ | ELitBool _ | ELitNat _ | ELitReal _ | ELitString _ | EDomain _ - | EQualified _ -> - e - -and prime_guards ~bound gs = - List.fold_left - (fun (bound, acc) g -> - match g with - | GParam p -> (p.param_name :: bound, acc @ [ GParam p ]) - | GIn (name, e) -> - (name :: bound, acc @ [ GIn (name, prime_expr ~bound e) ]) - | GExpr e -> (bound, acc @ [ GExpr (prime_expr ~bound e) ])) - (bound, []) gs - (** Generate frame condition expressions: for every rule NOT in the action's context, produce the SMT expression asserting f_prime = f. Returns a list of (function_name, smt_expr) pairs. *) @@ -1713,12 +1768,13 @@ let generate_contradiction_query config env action = (Printf.sprintf "%s' = %s (frame)" fname fname) smt_expr) frame_exprs; - (* Named postconditions *) + (* Named postconditions — no guard injection in postconditions *) + let post_config = { config with inject_guards = false } in Buffer.add_string buf "\n; --- Postconditions ---\n"; List.iter (fun (p : expr located) -> add_named_assert na "postcond" (Pretty.str_expr p.value) - (translate_proposition config env p.value)) + (translate_proposition post_config env p.value)) action.a_propositions; let value_terms = build_value_terms config env action.a_params in Buffer.add_string buf "(check-sat)\n"; @@ -1760,13 +1816,14 @@ let generate_invariant_query config env ~all_invariants ~index List.iter (fun pc -> Buffer.add_string buf (Printf.sprintf "(assert %s)\n" pc)) preconditions; - (* Assert action postconditions (transition relation) *) + (* Assert action postconditions (transition relation) — no guard injection *) + let post_config = { config with inject_guards = false } in Buffer.add_string buf "\n; --- Action postconditions (transition) ---\n"; - let transition = conjoin_propositions config env action.a_propositions in + let transition = conjoin_propositions post_config env action.a_propositions in Buffer.add_string buf (Printf.sprintf "(assert %s)\n" transition); (* Assert frame conditions *) Buffer.add_string buf (generate_frame_conditions config env action.a_context); - (* Assert single invariant violated in next state *) + (* Assert single invariant violated in next state — guards injected *) Buffer.add_string buf "\n; --- Invariant violated in next state ---\n"; let primed_inv = { inv with value = prime_expr inv.value } in let inv_primed = translate_proposition config env primed_inv.value in @@ -2175,10 +2232,12 @@ let build_step_transition config env actions step = in (* Preconditions (from guards) — translated in base names *) let precond_parts = extract_preconditions config env action.a_guards in - (* Postconditions — translated with base name/prime *) + (* Postconditions — no guard injection in postconditions *) + let post_config = { config with inject_guards = false } in let postcond_parts = List.map - (fun (p : expr located) -> translate_proposition config env p.value) + (fun (p : expr located) -> + translate_proposition post_config env p.value) action.a_propositions in (* Frame conditions *) diff --git a/samples/smt-examples/guarded-frame.pant b/samples/smt-examples/guarded-frame.pant new file mode 100644 index 0000000..0415ba4 --- /dev/null +++ b/samples/smt-examples/guarded-frame.pant @@ -0,0 +1,31 @@ +> Regression test for declaration guard injection in SMT translation. +> Guards on declarations (e.g., "value t: Thing, active? t => Nat0") +> must be: +> 1. NOT injected into postconditions (which define the transition relation) +> 2. Correctly primed in post-state invariant checks +module GUARDED_FRAME. + +context Ctx. + +Thing. + +{Ctx} active? t: Thing => Bool. +{Ctx} value t: Thing, active? t => Nat0. + +--- + +all t: Thing | value t >= 0. + +initially all t: Thing | ~active? t. + +where + +Ctx ~> Create | t: Thing, n: Nat0, ~active? t. + +--- + +active?' t. +value' t = n. + +all t2: Thing, t2 != t | active?' t2 = active? t2. +all t2: Thing, t2 != t | value' t2 = value t2. diff --git a/test/test_smt.ml b/test/test_smt.ml index c258e04..d974c83 100644 --- a/test/test_smt.ml +++ b/test/test_smt.ml @@ -23,7 +23,14 @@ let parse_and_collect str = (* --- Expression translation tests --- *) -let config = Smt.{ bound = 3; steps = 5; domain_bounds = Env.StringMap.empty } +let config = + Smt. + { + bound = 3; + steps = 5; + domain_bounds = Env.StringMap.empty; + inject_guards = true; + } let test_lit_bool () = let env = Env.empty "" in @@ -830,14 +837,18 @@ let test_compute_domain_bounds () = let test_bound_for () = let bounds = Env.StringMap.singleton "Color" 5 in - let config = Smt.{ bound = 3; steps = 5; domain_bounds = bounds } in + let config = + Smt.{ bound = 3; steps = 5; domain_bounds = bounds; inject_guards = true } + in check int "Color uses override" 5 (Smt.bound_for config "Color"); check int "Account uses default" 3 (Smt.bound_for config "Account") let test_card_domain_with_bounds () = let env = Env.empty "" |> Env.add_domain "Color" Ast.dummy_loc ~chapter:0 in let bounds = Env.StringMap.singleton "Color" 5 in - let cfg = Smt.{ bound = 3; steps = 5; domain_bounds = bounds } in + let cfg = + Smt.{ bound = 3; steps = 5; domain_bounds = bounds; inject_guards = true } + in check string "#Domain with per-domain bound" "5" (Smt.translate_expr cfg env (Ast.EUnop (OpCard, EDomain "Color"))) @@ -919,7 +930,13 @@ let test_translate_in_zero_bound () = (* Bug #2: bound=0 used to produce "(or )" — invalid SMT-LIB2. Now produces "false" (nothing in empty domain). *) let zero_config = - Smt.{ bound = 0; steps = 0; domain_bounds = Env.StringMap.empty } + Smt. + { + bound = 0; + steps = 0; + domain_bounds = Env.StringMap.empty; + inject_guards = true; + } in let env = Env.empty "" |> Env.add_domain "D" Ast.dummy_loc ~chapter:0 in let result = @@ -978,7 +995,13 @@ let test_domain_closure_bound_one () = all b: Block | ~(b in ancestor b).\n" in let one_config = - Smt.{ bound = 1; steps = 0; domain_bounds = Env.StringMap.empty } + Smt. + { + bound = 1; + steps = 0; + domain_bounds = Env.StringMap.empty; + inject_guards = true; + } in let queries = Smt.generate_queries one_config env doc in let inv = @@ -1335,7 +1358,13 @@ let test_closure_axiom_generation () = all b: Block | ~(b in ancestor b).\n" in let small_config = - Smt.{ bound = 2; steps = 0; domain_bounds = Env.StringMap.empty } + Smt. + { + bound = 2; + steps = 0; + domain_bounds = Env.StringMap.empty; + inject_guards = true; + } in let queries = Smt.generate_queries small_config env doc in let inv = @@ -1524,6 +1553,134 @@ let test_guard_substitution () = check bool "has (active x)" true (contains result "(active x)"); check bool "no (active u)" false (contains result "(active u)") +let test_primed_guard_collection () = + (* collect_body_guards on EApp(EPrimed "value", [EVar "t"]) should return + the primed guard [active?' t] *) + let env = + Env.empty "" + |> Env.add_domain "Thing" Ast.dummy_loc ~chapter:0 + |> Env.add_rule "value" + (Types.TyFunc ([ Types.TyDomain "Thing" ], Some Types.TyNat0)) + Ast.dummy_loc ~chapter:0 + |> Env.add_rule "active?" + (Types.TyFunc ([ Types.TyDomain "Thing" ], Some Types.TyBool)) + Ast.dummy_loc ~chapter:0 + |> Env.add_rule_guards "value" + [ Ast.{ param_name = "t"; param_type = TName "Thing" } ] + [ GExpr (EApp (EVar "active?", [ EVar "t" ])) ] + in + let expr = Ast.EApp (EPrimed "value", [ EVar "t" ]) in + let guards = Smt.collect_body_guards ~bound:[ "t" ] env expr in + check int "one guard" 1 (List.length guards); + (* The guard should be primed: EPrimed "active?" applied to EVar "t" + (t is not primed because it's not a rule name) *) + let guard = List.hd guards in + match guard with + | Ast.EApp (EPrimed "active?", [ EVar "t" ]) -> + check bool "primed guard for active?" true true + | _ -> + failf "Expected EApp(EPrimed \"active?\", [EVar \"t\"]) but got %s" + (Ast.show_expr guard) + +let test_inject_guards_false_skips () = + (* translate_proposition with inject_guards = false produces no + implication wrapper even for guarded applications *) + let env = + Env.empty "" + |> Env.add_domain "User" Ast.dummy_loc ~chapter:0 + |> Env.add_rule "score" + (Types.TyFunc ([ Types.TyDomain "User" ], Some Types.TyNat)) + Ast.dummy_loc ~chapter:0 + |> Env.add_rule "active" + (Types.TyFunc ([ Types.TyDomain "User" ], Some Types.TyBool)) + Ast.dummy_loc ~chapter:0 + |> Env.add_rule_guards "score" + [ Ast.{ param_name = "u"; param_type = TName "User" } ] + [ GExpr (EApp (EVar "active", [ EVar "u" ])) ] + |> Env.add_var "x" (Types.TyDomain "User") + in + let expr = Ast.EBinop (OpGe, EApp (EVar "score", [ EVar "x" ]), ELitNat 0) in + let no_guard_config = { config with Smt.inject_guards = false } in + let result = Smt.translate_proposition no_guard_config env expr in + (* Should NOT have an implication wrapper *) + check bool "no implication" true (not (contains result "(=>")); + (* But with inject_guards = true, it should *) + let result_with = Smt.translate_proposition config env expr in + check bool "has implication with guards" true (contains result_with "(=>") + +let test_guarded_decl_e2e () = + (* Full spec from bug report: guarded declarations should not cause + spurious invariant preservation failures *) + let env, doc = + parse_and_collect + "module Test.\n\ + context Ctx.\n\ + Thing.\n\ + {Ctx} active? t: Thing => Bool.\n\ + {Ctx} value t: Thing, active? t => Nat0.\n\ + ---\n\ + all t: Thing | value t >= 0.\n\ + initially all t: Thing | ~active? t.\n\ + where\n\ + Ctx ~> Create | t: Thing, n: Nat0, ~active? t.\n\ + ---\n\ + active?' t.\n\ + value' t = n.\n\ + all t2: Thing, t2 != t | active?' t2 = active? t2.\n\ + all t2: Thing, t2 != t | value' t2 = value t2.\n" + in + let queries = Smt.generate_queries config env doc in + (* Should generate queries without error *) + check bool "has queries" true (List.length queries > 0); + (* Check that contradiction query exists *) + let has_contradiction = + List.exists (fun (q : Smt.query) -> q.kind = Smt.Contradiction) queries + in + check bool "has contradiction query" true has_contradiction; + (* Invariant preservation query postconditions should NOT have guards *) + let inv_queries = + List.filter + (fun (q : Smt.query) -> q.kind = Smt.InvariantPreservation) + queries + in + check bool "has invariant queries" true (List.length inv_queries > 0); + let inv_q = List.hd inv_queries in + (* The postcondition section should not have guard injection. + Check that the "Action postconditions" section doesn't contain + an implication from activep *) + let postcond_section = + let lines = String.split_on_char '\n' inv_q.smt2 in + let in_postcond = ref false in + let postcond_lines = ref [] in + List.iter + (fun line -> + if contains line "Action postconditions" then in_postcond := true + else if + contains line "Frame conditions" || contains line "Invariant violated" + then in_postcond := false; + if !in_postcond then postcond_lines := line :: !postcond_lines) + lines; + String.concat "\n" (List.rev !postcond_lines) + in + (* Postcondition assertions should not wrap with guard implication *) + check bool "postcond no guard implication" false + (contains postcond_section "(=> (activep"); + (* The primed invariant (negated) should contain primed guard *) + let violated_section = + let lines = String.split_on_char '\n' inv_q.smt2 in + let in_violated = ref false in + let violated_lines = ref [] in + List.iter + (fun line -> + if contains line "Invariant violated" then in_violated := true; + if !in_violated then violated_lines := line :: !violated_lines) + lines; + String.concat "\n" (List.rev !violated_lines) + in + check bool "primed invariant has primed guard" true + (contains violated_section "activep_prime"); + ignore doc + let guard_injection_tests = [ test_case "quantifier guard injection" `Quick @@ -1533,6 +1690,9 @@ let guard_injection_tests = test_case "nested quantifier guards" `Quick test_nested_quantifier_guards; test_case "unguarded rule unchanged" `Quick test_unguarded_rule_unchanged; test_case "guard substitution" `Quick test_guard_substitution; + test_case "primed guard collection" `Quick test_primed_guard_collection; + test_case "inject_guards false skips" `Quick test_inject_guards_false_skips; + test_case "guarded decl e2e" `Quick test_guarded_decl_e2e; ] (* --- Cond expression tests --- *)