From 904208a1f7cd917195d9f2ca150678e129cef043 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 2 Jul 2025 12:23:08 +0100 Subject: [PATCH 1/4] different CN/solver interaction for SMT counter models CN used to create a new solver instance for each model. This means solver models can be passed around as values and interacted with later, but also complicates the Solver module. With this change, CN models are just references to the current solver state (so creating a model no longer creates a new solver instance). This means the timing of when CN queries the model matters, and type error reports including countermodel information have to be produced when the model is still "live". This change temporarily disables the CheckPredicates logic, which relies on asking new solver queries, which then override the present model -- to be fixed. --- lib/check.ml | 65 ++++++-- lib/explain.ml | 2 + lib/resourceInference.ml | 47 ++++-- lib/simple_smt.ml | 9 + lib/solver.ml | 287 ++++++++++++++++---------------- lib/solver.mli | 5 - lib/typeErrors.ml | 177 ++++++++++---------- lib/typeErrors.mli | 60 ++++--- tests/cn/reverse.error.c.verify | 2 +- 9 files changed, 370 insertions(+), 284 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index 9bf499d54..0115b8332 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -391,7 +391,8 @@ let check_conv_int loc ~expect ct arg = let fail_unrepresentable () = let@ model = model () in fail (fun ctxt -> - { loc; msg = Int_unrepresentable { value = arg; ict = ct; ctxt; model } }) + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Int_unrepresentable { value = arg; ict = ct; report } }) in let bt = IT.get_bt arg in (* TODO: can we (later) optimise this? *) @@ -434,7 +435,10 @@ let check_has_alloc_id loc ptr ub_unspec = | `False -> let@ model = model () in let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in - fail (fun ctxt -> { loc; msg = Needs_alloc_id { ptr; ub; ctxt; model } }) + fail (fun ctxt -> + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Needs_alloc_id { ptr; ub; report } } + ) else return () @@ -462,8 +466,10 @@ let check_both_eq_alloc loc arg1 arg2 ub = let@ provable = provable loc in match provable @@ LC.T both_alloc with | `False -> - let@ model = model () in - fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }) + let@ model = model () in + fail (fun ctxt -> + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } }) | `True -> return () @@ -485,7 +491,13 @@ let check_live_alloc_bounds ?(skip_live = false) reason loc ub ptrs = let@ model = model () in fail (fun ctxt -> let term = if List.length ptrs = 1 then List.hd ptrs else IT.tuple_ ptrs here in - { loc; msg = Alloc_out_of_bounds { constr; term; ub; ctxt; model } }) + let report = + Explain.trace + ctxt + model + Explain.{ no_ex with unproven_constraint = Some (LC.T constr) } + in + { loc; msg = Alloc_out_of_bounds { constr; term; ub; report } }) else return () @@ -660,7 +672,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = | `False -> let@ model = model () in let ub = CF.Undefined.UB045a_division_by_zero in - fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })) + fail (fun ctxt -> + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } })) | OpRem_t -> let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in let@ () = WellTyped.ensure_bits_type loc expect in @@ -675,7 +689,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = | `False -> let@ model = model () in let ub = CF.Undefined.UB045b_modulo_by_zero in - fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })) + fail (fun ctxt -> + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } })) | OpEq -> let@ () = WellTyped.ensure_base_type loc ~expect Bool in let@ () = @@ -882,7 +898,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = | `False -> let@ model = model () in let ub = CF.Undefined.UB036_exceptional_condition in - fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }) + fail (fun ctxt -> + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } }) in return direct_x | PEconv_int (ct_expr, pe) | PEconv_loaded_int (ct_expr, pe) -> @@ -915,7 +933,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = | `False -> let@ model = model () in let ub = CF.Undefined.UB036_exceptional_condition in - fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })) + fail (fun ctxt -> + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } })) | PEis_representable_integer (pe, act) -> let@ () = WellTyped.check_ct act.loc act.ct in let@ () = WellTyped.ensure_base_type loc ~expect Bool in @@ -972,7 +992,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = | `True -> return (default_ expect loc) | `False -> let@ model = model () in - fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })) + fail (fun ctxt -> + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } })) | PEerror (err, _pe) -> let@ provable = provable loc in let here = Locations.other __LOC__ in @@ -980,7 +1002,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = | `True -> return (default_ expect loc) | `False -> let@ model = model () in - fail (fun ctxt -> { loc; msg = StaticError { err; ctxt; model } })) + fail (fun ctxt -> + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = StaticError { err; report } })) module Spine : sig @@ -1137,8 +1161,8 @@ let all_empty loc _original_resources = let@ simp_ctxt = simp_ctxt () in RI.debug_constraint_failure_diagnostics 6 model simp_ctxt constr; fail (fun ctxt -> - (* let ctxt = { ctxt with resources = original_resources } in *) - { loc; msg = Unused_resource { resource; ctxt; model } }) + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Unused_resource { resource; report } }) let load loc pointer ct = @@ -1420,8 +1444,9 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | `False -> let@ model = model () in fail (fun ctxt -> - let ict = act_to.ct in - { loc; msg = Int_unrepresentable { value = arg; ict; ctxt; model } }) + let ict = act_to.ct in + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Int_unrepresentable { value = arg; ict; report } }) in k actual_value) | PtrFromInt (act_from, act_to, pe) -> @@ -1622,9 +1647,10 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | `False -> let@ model = model () in fail (fun ctxt -> + let report = Explain.trace ctxt model Explain.no_ex in let msg = Write_value_unrepresentable - { ct = act.ct; location = parg; value = varg; ctxt; model } + { ct = act.ct; location = parg; value = varg; report } in { loc; msg }) in @@ -1964,10 +1990,13 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = RI.debug_constraint_failure_diagnostics 6 model simp_ctxt lc; let@ () = Diagnostics.investigate model lc in fail (fun ctxt -> - { loc; + let report = + Explain.trace ctxt model Explain.{ no_ex with unproven_constraint = Some lc } + in + { loc; msg = Unproven_constraint - { constr = lc; info = (loc, None); requests = []; ctxt; model } + { constr = lc; info = (loc, None); requests = []; report } })) | Inline _nms -> return () | Print it -> diff --git a/lib/explain.ml b/lib/explain.ml index 475e4e8be..4d4f378e5 100644 --- a/lib/explain.ml +++ b/lib/explain.ml @@ -331,6 +331,8 @@ let state (ctxt : C.t) log model_with_q extras = (Rp.add_labeled Rp.lab_uninteresting uninteresting Rp.labeled_empty) in let invalid_resources = + (* temporarily disable these checks *) + if true then Rp.labeled_empty else let g = ctxt.global in let defs = g.resource_predicates in let check (rt, o) = diff --git a/lib/resourceInference.ml b/lib/resourceInference.ml index ced0b4295..f488727ab 100644 --- a/lib/resourceInference.ml +++ b/lib/resourceInference.ml @@ -79,8 +79,14 @@ module General = struct | `False -> let@ model = model () in let msg ctxt = - TypeErrors.Merging_multiple_arrays { requests; situation; ctxt; model } + let orequest = + Option.map (fun r -> r.TypeErrors.RequestChain.resource) + (List.nth_opt (List.rev requests) 0) + in + let report = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in + TypeErrors.Merging_multiple_arrays { requests; situation; report } in + fail (fun ctxt -> { loc; msg = msg ctxt }) | `True -> return default) in @@ -120,10 +126,15 @@ module General = struct | `False -> let@ model = model () in fail (fun ctxt -> - (* let ctxt = { ctxt with resources = original_resources } in *) + let orequest = + Option.map + TypeErrors.RequestChain.(fun (r : elem) -> r.resource) + (List.nth_opt (List.rev request_chain) 0) + in + let report = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in let msg = TypeErrors.Missing_resource - { requests = request_chain; situation; model; ctxt } + { requests = request_chain; situation; report } in { loc; msg }) | `True -> assert false) @@ -142,16 +153,16 @@ module General = struct | `True -> return (ftyp, []) | `False -> let@ model = model () in - let@ all_cs = get_cs () in - let () = assert (not (LC.Set.mem c all_cs)) in debug_constraint_failure_diagnostics 6 model simp_ctxt c; let@ () = Diagnostics.investigate model c in fail (fun ctxt -> - (* let ctxt = { ctxt with resources = original_resources } in *) + let report = + Explain.trace ctxt model Explain.{ no_ex with unproven_constraint = Some c } + in { loc; msg = TypeErrors.Unproven_constraint - { constr = c; info; requests = snd uiinfo; ctxt; model } + { constr = c; info; requests = snd uiinfo; report } })) | I _rt -> return (ftyp, []) @@ -477,7 +488,13 @@ module Special = struct | `False -> let@ model = model () in fail (fun ctxt -> - let msg = TypeErrors.Missing_resource { requests; situation; model; ctxt } in + let orequest = + Option.map + TypeErrors.RequestChain.(fun (r : elem) -> r.resource) + (List.nth_opt (List.rev requests) 0) + in + let report = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in + let msg = TypeErrors.Missing_resource { requests; situation; report } in { loc; msg }) | `True -> assert false @@ -555,16 +572,24 @@ module Special = struct match found with | Ans.Found -> return () | No_res -> - fail (fun ctxt -> + fail (fun _ctxt -> let msg = - TypeErrors.Allocation_not_live { reason; ptr; model_constr = None; ctxt } + (* probably we want Report.report to work also if no model is + available *) + TypeErrors.Allocation_not_live { reason; ptr; maybe_report = None } in { loc; msg }) | Model (model, constr) -> fail (fun ctxt -> + let report = + Explain.trace + ctxt + model + Explain.{ no_ex with unproven_constraint = Some (LC.T constr) } + in let msg = TypeErrors.Allocation_not_live - { reason; ptr; model_constr = Some (model, constr); ctxt } + { reason; ptr; maybe_report = Some report } in { loc; msg }) diff --git a/lib/simple_smt.ml b/lib/simple_smt.ml index 66391d842..a23f0b0b9 100644 --- a/lib/simple_smt.ml +++ b/lib/simple_smt.ml @@ -543,6 +543,15 @@ let check s = | Sexp.Atom "unknown" -> Unknown | ans -> raise (UnexpectedSolverResponse ans) +(** Check if the current set of assumptions, plus the argument, are consistent. + Throws {!UnexpectedSolverResponse}. *) +let check_assuming s lcs = + match s.command (list [atom "check-sat-assuming"; list lcs]) with + | Sexp.Atom "unsat" -> Unsat + | Sexp.Atom "sat" -> Sat + | Sexp.Atom "unknown" -> Unknown + | ans -> raise (UnexpectedSolverResponse ans) + (** {2 Decoding Results} *) diff --git a/lib/solver.ml b/lib/solver.ml index 75632a2f8..0063bdf13 100644 --- a/lib/solver.ml +++ b/lib/solver.ml @@ -81,7 +81,7 @@ let empty_solver_frame () = } -let copy_solver_frame f = { f with commands = f.commands } +let _copy_solver_frame f = { f with commands = f.commands } type solver = { smt_solver : SMT.solver; (** The SMT solver connection. *) @@ -94,6 +94,31 @@ type solver = globals : Global.t } + +(* ---------------------------------------------------------------------------*) +(* GLOBAL STATE: Models *) +(* ---------------------------------------------------------------------------*) + +type model = IT.t -> IT.t option +type quantifiers = (Sym.t * BaseTypes.t) list +type model_with_q = model * quantifiers + +type model_state = + | No_model + | Model of solver * quantifiers (* the solver that produced the model *) + +let model_state = ref No_model + +let have_model () = + match !model_state with + | No_model -> false + | Model _ -> true + + + + + + module Debug = struct let dump_frame (f : solver_frame) = let to_string = Sexplib.Sexp.to_string_hum in @@ -155,6 +180,7 @@ let debug_ack_command s cmd = (** Start a new scope. *) let push s = + model_state := No_model; debug_ack_command s (SMT.push 1); s.prev_frames := !(s.cur_frame) :: !(s.prev_frames); s.cur_frame := empty_solver_frame () @@ -162,6 +188,7 @@ let push s = (** Return to the previous scope. Assumes that there is a previous scope. *) let pop s n = + model_state := No_model; if n = 0 then () else ( @@ -1091,8 +1118,32 @@ let rec translate_term s iterm = | _ -> assert false) + + + +let model () = + match !model_state with + | No_model -> assert false + | Model (solver, qs) -> + let _defs = SMT.get_model solver.smt_solver in + let eval = + fun it -> + assert (have_model ()); + let sexp = translate_term solver it in + let res = SMT.get_expr solver.smt_solver sexp in + let ctys = get_ctype_table solver in + Some (get_ivalue solver.globals ctys (get_bt it) (SMT.no_let res)) + in + (eval, qs) + + + + + + (** Add an assertion. Quantified predicates are ignored. *) let add_assumption solver global lc = + model_state := No_model; let s1 = { solver with globals = global } in match lc with | LC.T it -> ack_command solver (SMT.assume (translate_term s1 it)) @@ -1289,100 +1340,75 @@ let make globals = s -(* ---------------------------------------------------------------------------*) -(* GLOBAL STATE: Models *) -(* ---------------------------------------------------------------------------*) - -type model = int - -type model_fn = IT.t -> IT.t option - -type model_with_q = model * (Sym.t * BaseTypes.t) list - -type model_table = (model, model_fn) Hashtbl.t - -let models_tbl : model_table = Hashtbl.create 1 - -let empty_model = - let model = Option.some in - Hashtbl.add models_tbl 0 model; - 0 - - -type model_state = - | Model of model_with_q - | No_model - -let model_state = ref No_model - -let model () = match !model_state with No_model -> assert false | Model mo -> mo - -(** Evaluate terms in the context of a model computed by the solver. *) -let model_evaluator, reset_model_evaluator_state = - (* internal state for the model evaluator, reuses the solver across consecutive calls for efficiency *) - let model_evaluator_solver : Simple_smt.solver option ref = ref None in - let currently_loaded_model = ref 0 in - let model_id = ref 0 in - let new_model_id () = - (* Start with 1, as 0 is the id of the empty model *) - model_id := !model_id + 1; - !model_id - in - let reset_model_evaluator_state () = - currently_loaded_model := 0; - model_evaluator_solver := None; - model_id := 0 - in - let model_evaluator solver mo = - match SMT.to_list mo with - | None -> failwith "model is an atom" - | Some defs -> - let scfg = solver.smt_solver.config in - let cfg = { scfg with log = Logger.make "model" } in - let smt_solver, new_solver = - match !model_evaluator_solver with - | Some smt_solver -> (smt_solver, false) - | None -> - let s = SMT.new_solver cfg in - model_evaluator_solver := Some s; - (s, true) - in - let model_id = new_model_id () in - let gs = solver.globals in - let evaluator = - { smt_solver; - cur_frame = ref (empty_solver_frame ()); - prev_frames = - ref - (List.map copy_solver_frame (!(solver.cur_frame) :: !(solver.prev_frames))) - (* We keep the prev_frames because things that were declared, would now be - defined by the model. Also, we need the infromation about the C type - mapping. *); - name_seed = solver.name_seed; - globals = gs - } - in - if new_solver then ( - declare_solver_basics evaluator; - push evaluator); - let model_fn e = - if not (!currently_loaded_model = model_id) then ( - currently_loaded_model := model_id; - pop evaluator 1; - push evaluator; - List.iter (debug_ack_command evaluator) defs); - let inp = translate_term evaluator e in - match SMT.check smt_solver with - | SMT.Sat -> - let res = SMT.get_expr smt_solver inp in - let ctys = get_ctype_table evaluator in - Some (get_ivalue gs ctys (get_bt e) (SMT.no_let res)) - | _ -> None - in - Hashtbl.add models_tbl model_id model_fn; - model_id - in - (model_evaluator, reset_model_evaluator_state) + + + +(* (\** Evaluate terms in the context of a model computed by the solver. *\) *) +(* let model_evaluator, reset_model_evaluator_state = *) +(* (\* internal state for the model evaluator, reuses the solver across consecutive calls for efficiency *\) *) +(* let model_evaluator_solver : Simple_smt.solver option ref = ref None in *) +(* let currently_loaded_model = ref 0 in *) +(* let model_id = ref 0 in *) +(* let new_model_id () = *) +(* (\* Start with 1, as 0 is the id of the empty model *\) *) +(* model_id := !model_id + 1; *) +(* !model_id *) +(* in *) +(* let reset_model_evaluator_state () = *) +(* currently_loaded_model := 0; *) +(* model_evaluator_solver := None; *) +(* model_id := 0 *) +(* in *) +(* let model_evaluator solver mo = *) +(* match SMT.to_list mo with *) +(* | None -> failwith "model is an atom" *) +(* | Some defs -> *) +(* let scfg = solver.smt_solver.config in *) +(* let cfg = { scfg with log = Logger.make "model" } in *) +(* let smt_solver, new_solver = *) +(* match !model_evaluator_solver with *) +(* | Some smt_solver -> (smt_solver, false) *) +(* | None -> *) +(* let s = SMT.new_solver cfg in *) +(* model_evaluator_solver := Some s; *) +(* (s, true) *) +(* in *) +(* let model_id = new_model_id () in *) +(* let gs = solver.globals in *) +(* let evaluator = *) +(* { smt_solver; *) +(* cur_frame = ref (empty_solver_frame ()); *) +(* prev_frames = *) +(* ref *) +(* (List.map copy_solver_frame (!(solver.cur_frame) :: !(solver.prev_frames))) *) +(* (\* We keep the prev_frames because things that were declared, would now be *) +(* defined by the model. Also, we need the infromation about the C type *) +(* mapping. *\); *) +(* name_seed = solver.name_seed; *) +(* globals = gs *) +(* } *) +(* in *) +(* if new_solver then ( *) +(* declare_solver_basics evaluator; *) +(* push evaluator); *) +(* let model_fn e = *) +(* if not (!currently_loaded_model = model_id) then ( *) +(* currently_loaded_model := model_id; *) +(* pop evaluator 1; *) +(* push evaluator; *) +(* List.iter (debug_ack_command evaluator) defs); *) +(* let inp = translate_term evaluator e in *) +(* match SMT.check smt_solver with *) +(* | SMT.Sat -> *) +(* let res = SMT.get_expr smt_solver inp in *) +(* let ctys = get_ctype_table evaluator in *) +(* Some (get_ivalue gs ctys (get_bt e) (SMT.no_let res)) *) +(* | _ -> None *) +(* in *) +(* Hashtbl.add models_tbl model_id model_fn; *) +(* model_id *) +(* in *) +(* (model_evaluator, reset_model_evaluator_state) *) (* ---------------------------------------------------------------------------*) @@ -1443,11 +1469,7 @@ let try_hard = ref false let provableWithUnknown ~loc ~solver ~assumptions ~simp_ctxt lc = let _ = loc in - let set_model smt_solver qs = - let defs = SMT.get_model smt_solver in - let model = model_evaluator solver defs in - model_state := Model (model, qs) - in + let set_model (s : solver) qs = model_state := Model (s, qs) in match shortcut simp_ctxt lc with | `True -> model_state := No_model; @@ -1455,46 +1477,34 @@ let provableWithUnknown ~loc ~solver ~assumptions ~simp_ctxt lc = | `No_shortcut lc -> let { expr; qs; extra } = translate_goal solver assumptions lc in let nexpr = SMT.bool_not expr in - let inc = solver.smt_solver in - debug_ack_command solver (SMT.push 1); - debug_ack_command solver (SMT.assume (SMT.bool_ands (nexpr :: extra))); - (match SMT.check inc with + (match SMT.check_assuming solver.smt_solver (nexpr :: extra) with | SMT.Unsat -> - debug_ack_command solver (SMT.pop 1); model_state := No_model; `True - | SMT.Sat when !try_hard -> - debug_ack_command solver (SMT.pop 1); - let assumptions = LC.Set.elements assumptions in - let foralls = TryHard.translate_foralls solver assumptions in - let functions = TryHard.translate_functions solver in - debug_ack_command solver (SMT.push 1); - debug_ack_command - solver - (SMT.assume (SMT.bool_ands ((nexpr :: foralls) @ functions))); - Pp.(debug 3 (lazy !^"***** try-hard *****")); - (match SMT.check inc with - | SMT.Unsat -> - debug_ack_command solver (SMT.pop 1); - model_state := No_model; - Pp.(debug 3 (lazy !^"***** try-hard: provable *****")); - `True - | SMT.Sat -> - set_model inc qs; - debug_ack_command solver (SMT.pop 1); - Pp.(debug 3 (lazy !^"***** try-hard: unprovable *****")); - `Unknown (*TODO CHT*) - | SMT.Unknown -> - set_model inc qs; - debug_ack_command solver (SMT.pop 1); - Pp.(debug 3 (lazy !^"***** try-hard: unknown *****")); - `False) | SMT.Sat -> - set_model inc qs; - debug_ack_command solver (SMT.pop 1); - `False + (match !try_hard with + | true -> + let assumptions = LC.Set.elements assumptions in + let foralls = TryHard.translate_foralls solver assumptions in + let functions = TryHard.translate_functions solver in + Pp.(debug 3 (lazy !^"***** try-hard *****")); + (match SMT.check_assuming solver.smt_solver ((nexpr :: foralls) @ functions) with + | SMT.Unsat -> + model_state := No_model; + Pp.(debug 3 (lazy !^"***** try-hard: provable *****")); + `True + | SMT.Sat -> + set_model solver qs; + Pp.(debug 3 (lazy !^"***** try-hard: unprovable *****")); + `False + | SMT.Unknown -> + set_model solver qs; + Pp.(debug 3 (lazy !^"***** try-hard: unknown *****")); + `Unknown) + | false -> + set_model solver qs; + `False) | SMT.Unknown -> - debug_ack_command solver (SMT.pop 1); failwith "Unknown") @@ -1511,7 +1521,6 @@ let provable ~loc ~solver ~assumptions ~simp_ctxt ?(purpose = "") lc = result -(* ISD: Could these globs be different from the saved ones? *) -let eval mo t = - let model_fn = Hashtbl.find models_tbl mo in - model_fn t +(* TODO: remove this *) +let eval model t = + model t diff --git a/lib/solver.mli b/lib/solver.mli index 6f284ce67..05c7372ce 100644 --- a/lib/solver.mli +++ b/lib/solver.mli @@ -6,8 +6,6 @@ type model (** Model with quantifier instantiations *) type model_with_q = model * (Sym.t * BaseTypes.t) list -val empty_model : model - module Logger : sig val to_file : bool ref @@ -35,9 +33,6 @@ val pop : solver -> int -> unit but may be unnecessary https://github.com/rems-project/cerberus/issues/752 *) val num_scopes : solver -> int -(* Resets internal state for the model evaluator *) -val reset_model_evaluator_state : unit -> unit - (* Run the solver. Note that we pass the assumptions explicitly even though they are also available in the solver context, because CN is going some simplification on its own. *) val provableWithUnknown diff --git a/lib/typeErrors.ml b/lib/typeErrors.ml index f939401c3..df3793efa 100644 --- a/lib/typeErrors.ml +++ b/lib/typeErrors.ml @@ -94,19 +94,22 @@ type message = | Missing_resource of { requests : RequestChain.t; situation : situation; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report; } | Merging_multiple_arrays of { requests : RequestChain.t; situation : situation; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Unused_resource of { resource : Res.t; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report; } | Illtyped_binary_it of { left : IT.Surface.t; @@ -119,60 +122,68 @@ type message = { ct : Sctypes.t; location : IT.t; value : IT.t; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report; } | Int_unrepresentable of { value : IT.t; ict : Sctypes.t; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report; } | Unproven_constraint of { constr : LC.t; requests : RequestChain.t; info : Locations.info; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report; } | Undefined_behaviour of { ub : CF.Undefined.undefined_behaviour; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report; } | Needs_alloc_id of { ptr : IT.t; ub : CF.Undefined.undefined_behaviour; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Alloc_out_of_bounds of { term : IT.t; constr : IT.t; ub : CF.Undefined.undefined_behaviour; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report; } | Allocation_not_live of { reason : [ `Copy_alloc_id | `Ptr_cmp | `Ptr_diff | `ISO_array_shift | `ISO_member_shift ]; ptr : IT.t; - ctxt : Context.t * Explain.log; - model_constr : (Solver.model_with_q * IT.t) option + (* ctxt : Context.t * Explain.log; *) + maybe_report : Report.report option } (* | Implementation_defined_behaviour of document * state_report *) | Unspecified of CF.Ctype.ctype | StaticError of { err : string; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Generic of Pp.document [@deprecated "Please add a specific constructor"] (** TODO delete this *) | Generic_with_model of { err : document; - model : Solver.model_with_q; - ctxt : Context.t * Explain.log + (* model : Solver.model_with_q; *) + (* ctxt : Context.t * Explain.log *) + report : Report.report } [@deprecated "Please add a specific constructor"] | Unsupported of document | Empty_provenance @@ -445,17 +456,17 @@ let pp_message = function | Compile msg -> pp_compile msg | Builtins msg -> pp_builtins msg | Parse msg -> pp_parse msg - | Missing_resource { requests; situation; ctxt; model } -> + | Missing_resource { requests; situation; report } -> let short = !^"Missing resource" ^^^ for_situation situation in let descr = RequestChain.pp requests in - let orequest = - Option.map - (fun (r : RequestChain.elem) -> r.RequestChain.resource) - (List.nth_opt (List.rev requests) 0) - in - let state = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in - { short; descr; state = Some state } - | Merging_multiple_arrays { requests; situation; ctxt; model } -> + (* let orequest = *) + (* Option.map *) + (* (fun (r : RequestChain.elem) -> r.RequestChain.resource) *) + (* (List.nth_opt (List.rev requests) 0) *) + (* in *) + (* let state = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in *) + { short; descr; state = Some report } + | Merging_multiple_arrays { requests; situation; report } -> let short = !^"Cannot satisfy request for resource" ^^^ for_situation situation @@ -463,16 +474,12 @@ let pp_message = function ^^^ !^"It requires merging multiple arrays." in let descr = RequestChain.pp requests in - let orequest = - Option.map (fun r -> r.RequestChain.resource) (List.nth_opt (List.rev requests) 0) - in - let state = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in - { short; descr; state = Some state } - | Unused_resource { resource; ctxt; model } -> + { short; descr; state = Some report } + | Unused_resource { resource; report } -> let resource = Res.pp resource in let short = !^"Left-over unused resource" ^^^ squotes resource in - let state = Explain.trace ctxt model Explain.no_ex in - { short; descr = None; state = Some state } + (* let state = Explain.trace ctxt model Explain.no_ex in *) + { short; descr = None; state = Some report } | TooBigExponent { it } -> let it = IT.pp it in let short = !^"Exponent too big" in @@ -499,26 +506,25 @@ let pp_message = function ^^^ !^"Exponent must be non-negative" in { short; descr = Some descr; state = None } - | Write_value_unrepresentable { ct; location; value; ctxt; model } -> + | Write_value_unrepresentable { ct; location; value; report } -> let short = !^"Write value not representable at type" ^^^ Sctypes.pp ct in let location = IT.pp location in let value = IT.pp value in - let state = Explain.trace ctxt model Explain.no_ex in + (* let state = Explain.trace ctxt model Explain.no_ex in *) let descr = !^"Location" ^^ colon ^^^ location ^^ comma ^^^ !^"value" ^^ colon ^^^ value ^^ dot in - { short; descr = Some descr; state = Some state } - | Int_unrepresentable { value; ict; ctxt; model } -> + { short; descr = Some descr; state = Some report } + | Int_unrepresentable { value; ict; report } -> let short = !^"integer value not representable at type" ^^^ Sctypes.pp ict in let value = IT.pp value in let descr = !^"Value" ^^ colon ^^^ value in - let state = Explain.trace ctxt model Explain.no_ex in - { short; descr = Some descr; state = Some state } - | Unproven_constraint { constr; requests; info; ctxt; model } -> + { short; descr = Some descr; state = Some report } + | Unproven_constraint { constr = _; requests; info; report } -> let short = !^"Unprovable constraint" in - let state = - Explain.trace ctxt model Explain.{ no_ex with unproven_constraint = Some constr } - in + (* let state = *) + (* Explain.trace ctxt model Explain.{ no_ex with unproven_constraint = Some constr } *) + (* in *) let descr = let spec_loc, odescr = info in let head, pos = Locations.head_pos_of_location spec_loc in @@ -531,40 +537,40 @@ let pp_message = function | Some doc2 -> doc ^^ hardline ^^ doc2 | None -> doc in - { short; descr = Some descr; state = Some state } - | Undefined_behaviour { ub; ctxt; model } -> + { short; descr = Some descr; state = Some report } + | Undefined_behaviour { ub; report } -> let short = !^"Undefined behaviour" in - let state = Explain.trace ctxt model Explain.no_ex in + (* let state = Explain.trace ctxt model Explain.no_ex in *) let descr = match CF.Undefined.std_of_undefined_behaviour ub with | Some stdref -> !^(CF.Undefined.ub_short_string ub) ^^^ parens !^stdref | None -> !^(CF.Undefined.ub_short_string ub) in - { short; descr = Some descr; state = Some state } - | Needs_alloc_id { ptr; ub; ctxt; model } -> + { short; descr = Some descr; state = Some report } + | Needs_alloc_id { ptr; ub; report } -> let short = !^"Pointer " ^^ bquotes (IT.pp ptr) ^^ !^" needs allocation ID" in - let state = Explain.trace ctxt model Explain.no_ex in + (* let state = Explain.trace ctxt model Explain.no_ex in *) let descr = match CF.Undefined.std_of_undefined_behaviour ub with | Some stdref -> !^(CF.Undefined.ub_short_string ub) ^^^ parens !^stdref | None -> !^(CF.Undefined.ub_short_string ub) in - { short; descr = Some descr; state = Some state } - | Alloc_out_of_bounds { constr; term; ub; ctxt; model } -> + { short; descr = Some descr; state = Some report } + | Alloc_out_of_bounds { constr = _; term; ub; report } -> let short = bquotes (IT.pp term) ^^ !^" out of bounds" in - let state = - Explain.trace - ctxt - model - Explain.{ no_ex with unproven_constraint = Some (LC.T constr) } - in + (* let state = *) + (* Explain.trace *) + (* ctxt *) + (* model *) + (* Explain.{ no_ex with unproven_constraint = Some (LC.T constr) } *) + (* in *) let descr = match CF.Undefined.std_of_undefined_behaviour ub with | Some stdref -> !^(CF.Undefined.ub_short_string ub) ^^^ parens !^stdref | None -> !^(CF.Undefined.ub_short_string ub) in - { short; descr = Some descr; state = Some state } - | Allocation_not_live { reason; ptr; ctxt; model_constr } -> + { short; descr = Some descr; state = Some report } + | Allocation_not_live { reason; ptr; maybe_report } -> let adjust = function | IT.IT (CopyAllocId { loc; _ }, _, _) -> loc | IT.IT (ArrayShift { base; _ }, _, _) -> base @@ -582,17 +588,17 @@ let pp_message = function let short = !^"Pointer " ^^ bquotes (IT.pp ptr) ^^^ !^"needs to be live for" ^^^ !^reason in - let state = - Option.map - (fun (model, constr) -> - Explain.trace - ctxt - model - Explain.{ no_ex with unproven_constraint = Some (LC.T constr) }) - model_constr - in + (* let state = *) + (* Option.map *) + (* (fun (model, constr) -> *) + (* Explain.trace *) + (* ctxt *) + (* model *) + (* Explain.{ no_ex with unproven_constraint = Some (LC.T constr) }) *) + (* model_constr *) + (* in *) let descr = !^"Need an Alloc or RW in context with same allocation id" in - { short; descr = Some descr; state } + { short; descr = Some descr; state = maybe_report } (* | Implementation_defined_behaviour (impl, state) -> *) (* let short = !^"Implementation defined behaviour" in *) (* let descr = impl in *) @@ -600,18 +606,18 @@ let pp_message = function | Unspecified ctype -> let short = !^"Unspecified value of C-type" ^^^ CF.Pp_core_ctype.pp_ctype ctype in { short; descr = None; state = None } - | StaticError { err; ctxt; model } -> + | StaticError { err; report } -> let short = !^"Static error" in - let state = Explain.trace ctxt model Explain.no_ex in + (* let state = Explain.trace ctxt model Explain.no_ex in *) let descr = !^err in - { short; descr = Some descr; state = Some state } + { short; descr = Some descr; state = Some report } | ((Generic err) [@alert "-deprecated"]) -> let short = err in { short; descr = None; state = None } - | ((Generic_with_model { err; model; ctxt }) [@alert "-deprecated"]) -> + | ((Generic_with_model { err; report }) [@alert "-deprecated"]) -> let short = err in - let state = Explain.trace ctxt model Explain.no_ex in - { short; descr = None; state = Some state } + (* let state = Explain.trace ctxt model Explain.no_ex in *) + { short; descr = None; state = Some report } | Unsupported err -> let short = err in { short; descr = None; state = None } @@ -619,10 +625,9 @@ let pp_message = function let short = !^"Empty provenance" in { short; descr = None; state = None } | Illtyped_binary_it { left; right; binop } -> pp_illtyped_binary_it ~left ~right binop - | Inconsistent_assumptions (kind, ctxt_log) -> + | Inconsistent_assumptions (kind, _ctxt_log) -> let short = !^kind ^^ !^" makes inconsistent assumptions" in - let state = Some (Explain.trace ctxt_log (Solver.empty_model, []) Explain.no_ex) in - { short; descr = None; state } + { short; descr = None; state = None } | Byte_conv_needs_owned -> let short = !^"byte conversion only supports W/RW" in { short; descr = None; state = None } diff --git a/lib/typeErrors.mli b/lib/typeErrors.mli index 527659d98..1247a7c6c 100644 --- a/lib/typeErrors.mli +++ b/lib/typeErrors.mli @@ -37,19 +37,22 @@ type message = | Missing_resource of { requests : RequestChain.t; situation : Error_common.situation; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Merging_multiple_arrays of { requests : RequestChain.t; situation : Error_common.situation; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Unused_resource of { resource : Resource.t; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Illtyped_binary_it of { left : IndexTerms.Surface.t; @@ -62,59 +65,68 @@ type message = { ct : Sctypes.t; location : IndexTerms.t; value : IndexTerms.t; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Int_unrepresentable of { value : IndexTerms.t; ict : Sctypes.t; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Unproven_constraint of { constr : LogicalConstraints.t; requests : RequestChain.t; info : Locations.info; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Undefined_behaviour of { ub : Cerb_frontend.Undefined.undefined_behaviour; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Needs_alloc_id of { ptr : IndexTerms.t; ub : Cerb_frontend.Undefined.undefined_behaviour; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Alloc_out_of_bounds of { term : IndexTerms.t; constr : IndexTerms.t; ub : Cerb_frontend.Undefined.undefined_behaviour; - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Allocation_not_live of { reason : [ `Copy_alloc_id | `ISO_array_shift | `ISO_member_shift | `Ptr_cmp | `Ptr_diff ]; ptr : IndexTerms.t; - ctxt : Context.t * Explain.log; - model_constr : (Solver.model_with_q * IndexTerms.t) option + (* ctxt : Context.t * Explain.log; *) + (* model_constr : (Solver.model_with_q * IndexTerms.t) option *) + maybe_report : Report.report option } | Unspecified of Cerb_frontend.Ctype.ctype | StaticError of { err : string; (** TODO replace with an actual type *) - ctxt : Context.t * Explain.log; - model : Solver.model_with_q + (* ctxt : Context.t * Explain.log; *) + (* model : Solver.model_with_q *) + report : Report.report } | Generic of Pp.document [@deprecated "Please add a specific constructor"] (** TODO delete this *) | Generic_with_model of { err : Pp.document; - model : Solver.model_with_q; - ctxt : Context.t * Explain.log + (* model : Solver.model_with_q; *) + (* ctxt : Context.t * Explain.log *) + report : Report.report } [@deprecated "Please add a specific constructor"] (** TODO delete this too *) | Unsupported of Pp.document (** TODO add source location *) | Empty_provenance diff --git a/tests/cn/reverse.error.c.verify b/tests/cn/reverse.error.c.verify index 132f40521..87972383a 100644 --- a/tests/cn/reverse.error.c.verify +++ b/tests/cn/reverse.error.c.verify @@ -13,5 +13,5 @@ tests/cn/reverse.error.c:124:3: error: Missing resource for de-allocating ^~~~~~~~~ Resource needed: W(&n3) which requires: W(&&n3->head) - other location (File "lib/resourceInference.ml", line 205, characters 31-38) (arg head) + other location (File "lib/resourceInference.ml", line 216, characters 31-38) (arg head) State file: file:///tmp/state__reverse.error.c__main.html From 5b53fa10c6686a4bc60c4d80e96829afb8a3fbbf Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 2 Jul 2025 12:29:19 +0100 Subject: [PATCH 2/4] dune fmt --- lib/check.ml | 58 ++++++++++++++-------------- lib/explain.ml | 83 +++++++++++++++++++++------------------- lib/resourceInference.ml | 21 +++++----- lib/simple_smt.ml | 3 +- lib/solver.ml | 68 ++++++++++++-------------------- lib/typeErrors.ml | 14 +++---- 6 files changed, 119 insertions(+), 128 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index 0115b8332..a188aeb53 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -436,9 +436,8 @@ let check_has_alloc_id loc ptr ub_unspec = let@ model = model () in let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in fail (fun ctxt -> - let report = Explain.trace ctxt model Explain.no_ex in - { loc; msg = Needs_alloc_id { ptr; ub; report } } - ) + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Needs_alloc_id { ptr; ub; report } }) else return () @@ -466,10 +465,10 @@ let check_both_eq_alloc loc arg1 arg2 ub = let@ provable = provable loc in match provable @@ LC.T both_alloc with | `False -> - let@ model = model () in - fail (fun ctxt -> - let report = Explain.trace ctxt model Explain.no_ex in - { loc; msg = Undefined_behaviour { ub; report } }) + let@ model = model () in + fail (fun ctxt -> + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } }) | `True -> return () @@ -673,8 +672,8 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = let@ model = model () in let ub = CF.Undefined.UB045a_division_by_zero in fail (fun ctxt -> - let report = Explain.trace ctxt model Explain.no_ex in - { loc; msg = Undefined_behaviour { ub; report } })) + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } })) | OpRem_t -> let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in let@ () = WellTyped.ensure_bits_type loc expect in @@ -690,8 +689,8 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = let@ model = model () in let ub = CF.Undefined.UB045b_modulo_by_zero in fail (fun ctxt -> - let report = Explain.trace ctxt model Explain.no_ex in - { loc; msg = Undefined_behaviour { ub; report } })) + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } })) | OpEq -> let@ () = WellTyped.ensure_base_type loc ~expect Bool in let@ () = @@ -899,8 +898,8 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = let@ model = model () in let ub = CF.Undefined.UB036_exceptional_condition in fail (fun ctxt -> - let report = Explain.trace ctxt model Explain.no_ex in - { loc; msg = Undefined_behaviour { ub; report } }) + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } }) in return direct_x | PEconv_int (ct_expr, pe) | PEconv_loaded_int (ct_expr, pe) -> @@ -934,8 +933,8 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = let@ model = model () in let ub = CF.Undefined.UB036_exceptional_condition in fail (fun ctxt -> - let report = Explain.trace ctxt model Explain.no_ex in - { loc; msg = Undefined_behaviour { ub; report } })) + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } })) | PEis_representable_integer (pe, act) -> let@ () = WellTyped.check_ct act.loc act.ct in let@ () = WellTyped.ensure_base_type loc ~expect Bool in @@ -993,8 +992,8 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = | `False -> let@ model = model () in fail (fun ctxt -> - let report = Explain.trace ctxt model Explain.no_ex in - { loc; msg = Undefined_behaviour { ub; report } })) + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Undefined_behaviour { ub; report } })) | PEerror (err, _pe) -> let@ provable = provable loc in let here = Locations.other __LOC__ in @@ -1003,8 +1002,8 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m = | `False -> let@ model = model () in fail (fun ctxt -> - let report = Explain.trace ctxt model Explain.no_ex in - { loc; msg = StaticError { err; report } })) + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = StaticError { err; report } })) module Spine : sig @@ -1161,8 +1160,8 @@ let all_empty loc _original_resources = let@ simp_ctxt = simp_ctxt () in RI.debug_constraint_failure_diagnostics 6 model simp_ctxt constr; fail (fun ctxt -> - let report = Explain.trace ctxt model Explain.no_ex in - { loc; msg = Unused_resource { resource; report } }) + let report = Explain.trace ctxt model Explain.no_ex in + { loc; msg = Unused_resource { resource; report } }) let load loc pointer ct = @@ -1444,8 +1443,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | `False -> let@ model = model () in fail (fun ctxt -> - let ict = act_to.ct in - let report = Explain.trace ctxt model Explain.no_ex in + let ict = act_to.ct in + let report = Explain.trace ctxt model Explain.no_ex in { loc; msg = Int_unrepresentable { value = arg; ict; report } }) in k actual_value) @@ -1647,7 +1646,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = | `False -> let@ model = model () in fail (fun ctxt -> - let report = Explain.trace ctxt model Explain.no_ex in + let report = Explain.trace ctxt model Explain.no_ex in let msg = Write_value_unrepresentable { ct = act.ct; location = parg; value = varg; report } @@ -1990,10 +1989,13 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = RI.debug_constraint_failure_diagnostics 6 model simp_ctxt lc; let@ () = Diagnostics.investigate model lc in fail (fun ctxt -> - let report = - Explain.trace ctxt model Explain.{ no_ex with unproven_constraint = Some lc } - in - { loc; + let report = + Explain.trace + ctxt + model + Explain.{ no_ex with unproven_constraint = Some lc } + in + { loc; msg = Unproven_constraint { constr = lc; info = (loc, None); requests = []; report } diff --git a/lib/explain.ml b/lib/explain.ml index 4d4f378e5..1a2f5ff55 100644 --- a/lib/explain.ml +++ b/lib/explain.ml @@ -332,47 +332,50 @@ let state (ctxt : C.t) log model_with_q extras = in let invalid_resources = (* temporarily disable these checks *) - if true then Rp.labeled_empty else - let g = ctxt.global in - let defs = g.resource_predicates in - let check (rt, o) = - match (rt, o) with - | Req.Q _, _ -> None - | Req.P { name = Owned _; pointer = _; iargs = _ }, _ -> None - | Req.P { name = PName s; pointer = _; iargs }, Resource.O it -> - (match (Sym.Map.find_opt s defs, evaluate it) with - | Some def, Some cand -> - let here = Locations.other __LOC__ in - let ptr_val = Req.get_pointer rt in - let ptr_def = (IT.sym_ (def.pointer, IT.get_bt ptr_val, here), ptr_val) in - Some (CP.check_pred s def cand ctxt iargs (ptr_def :: vals), rt, it) - | Some _, None -> - Some - ( CP.Result.error (!^"Could not locate definition of variable" ^^^ IT.pp it), - rt, - it ) - | None, _ -> - Some - ( CP.Result.error (!^"Could not locate definition of predicate" ^^^ Sym.pp s), - rt, - it )) - in - let checked = List.filter_map check (C.get_rs ctxt) in - let nos, _ = List.partition (fun (r, _, _) -> CP.Result.is_no r) checked in - (* let yeses, unknown = List.partition (fun (r, _, _) -> is_yes r) rest in *) - (* Issue #900 *) - let pp_checked_res (p, req, cand) = - let _ = p in - let rslt = Req.pp req ^^^ !^"(" ^^^ IT.pp cand ^^^ !^")" in - Rp. - { original = rslt; - (* !^"Full predicate check output: " + if true then + Rp.labeled_empty + else ( + let g = ctxt.global in + let defs = g.resource_predicates in + let check (rt, o) = + match (rt, o) with + | Req.Q _, _ -> None + | Req.P { name = Owned _; pointer = _; iargs = _ }, _ -> None + | Req.P { name = PName s; pointer = _; iargs }, Resource.O it -> + (match (Sym.Map.find_opt s defs, evaluate it) with + | Some def, Some cand -> + let here = Locations.other __LOC__ in + let ptr_val = Req.get_pointer rt in + let ptr_def = (IT.sym_ (def.pointer, IT.get_bt ptr_val, here), ptr_val) in + Some (CP.check_pred s def cand ctxt iargs (ptr_def :: vals), rt, it) + | Some _, None -> + Some + ( CP.Result.error (!^"Could not locate definition of variable" ^^^ IT.pp it), + rt, + it ) + | None, _ -> + Some + ( CP.Result.error + (!^"Could not locate definition of predicate" ^^^ Sym.pp s), + rt, + it )) + in + let checked = List.filter_map check (C.get_rs ctxt) in + let nos, _ = List.partition (fun (r, _, _) -> CP.Result.is_no r) checked in + (* let yeses, unknown = List.partition (fun (r, _, _) -> is_yes r) rest in *) + (* Issue #900 *) + let pp_checked_res (p, req, cand) = + let _ = p in + let rslt = Req.pp req ^^^ !^"(" ^^^ IT.pp cand ^^^ !^")" in + Rp. + { original = rslt; + (* !^"Full predicate check output: " ^^^ CP.Result.pp (Pp.list LC.pp) (fun x -> x) p; *) - (* Issue #900 *) - simplified = [ rslt ] - } - in - Rp.add_labeled Rp.lab_invalid (List.map pp_checked_res nos) Rp.labeled_empty + (* Issue #900 *) + simplified = [ rslt ] + } + in + Rp.add_labeled Rp.lab_invalid (List.map pp_checked_res nos) Rp.labeled_empty) (* Currently only displays invalid predicates : Issue #900 *) (* (Rp.add_labeled Rp.lab_unknown diff --git a/lib/resourceInference.ml b/lib/resourceInference.ml index f488727ab..a92ca6729 100644 --- a/lib/resourceInference.ml +++ b/lib/resourceInference.ml @@ -80,13 +80,15 @@ module General = struct let@ model = model () in let msg ctxt = let orequest = - Option.map (fun r -> r.TypeErrors.RequestChain.resource) + Option.map + (fun r -> r.TypeErrors.RequestChain.resource) (List.nth_opt (List.rev requests) 0) in - let report = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in + let report = + Explain.trace ctxt model Explain.{ no_ex with request = orequest } + in TypeErrors.Merging_multiple_arrays { requests; situation; report } in - fail (fun ctxt -> { loc; msg = msg ctxt }) | `True -> return default) in @@ -131,7 +133,9 @@ module General = struct TypeErrors.RequestChain.(fun (r : elem) -> r.resource) (List.nth_opt (List.rev request_chain) 0) in - let report = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in + let report = + Explain.trace ctxt model Explain.{ no_ex with request = orequest } + in let msg = TypeErrors.Missing_resource { requests = request_chain; situation; report } @@ -156,9 +160,9 @@ module General = struct debug_constraint_failure_diagnostics 6 model simp_ctxt c; let@ () = Diagnostics.investigate model c in fail (fun ctxt -> - let report = - Explain.trace ctxt model Explain.{ no_ex with unproven_constraint = Some c } - in + let report = + Explain.trace ctxt model Explain.{ no_ex with unproven_constraint = Some c } + in { loc; msg = TypeErrors.Unproven_constraint @@ -588,8 +592,7 @@ module Special = struct Explain.{ no_ex with unproven_constraint = Some (LC.T constr) } in let msg = - TypeErrors.Allocation_not_live - { reason; ptr; maybe_report = Some report } + TypeErrors.Allocation_not_live { reason; ptr; maybe_report = Some report } in { loc; msg }) diff --git a/lib/simple_smt.ml b/lib/simple_smt.ml index a23f0b0b9..f62c3ee36 100644 --- a/lib/simple_smt.ml +++ b/lib/simple_smt.ml @@ -543,10 +543,11 @@ let check s = | Sexp.Atom "unknown" -> Unknown | ans -> raise (UnexpectedSolverResponse ans) + (** Check if the current set of assumptions, plus the argument, are consistent. Throws {!UnexpectedSolverResponse}. *) let check_assuming s lcs = - match s.command (list [atom "check-sat-assuming"; list lcs]) with + match s.command (list [ atom "check-sat-assuming"; list lcs ]) with | Sexp.Atom "unsat" -> Unsat | Sexp.Atom "sat" -> Sat | Sexp.Atom "unknown" -> Unknown diff --git a/lib/solver.ml b/lib/solver.ml index 0063bdf13..1f5b36ca2 100644 --- a/lib/solver.ml +++ b/lib/solver.ml @@ -94,30 +94,23 @@ type solver = globals : Global.t } - (* ---------------------------------------------------------------------------*) (* GLOBAL STATE: Models *) (* ---------------------------------------------------------------------------*) type model = IT.t -> IT.t option + type quantifiers = (Sym.t * BaseTypes.t) list + type model_with_q = model * quantifiers type model_state = | No_model - | Model of solver * quantifiers (* the solver that produced the model *) + | Model of solver * quantifiers (* the solver that produced the model *) let model_state = ref No_model -let have_model () = - match !model_state with - | No_model -> false - | Model _ -> true - - - - - +let have_model () = match !model_state with No_model -> false | Model _ -> true module Debug = struct let dump_frame (f : solver_frame) = @@ -1118,27 +1111,20 @@ let rec translate_term s iterm = | _ -> assert false) - - - let model () = match !model_state with | No_model -> assert false | Model (solver, qs) -> - let _defs = SMT.get_model solver.smt_solver in - let eval = - fun it -> - assert (have_model ()); - let sexp = translate_term solver it in - let res = SMT.get_expr solver.smt_solver sexp in - let ctys = get_ctype_table solver in - Some (get_ivalue solver.globals ctys (get_bt it) (SMT.no_let res)) - in - (eval, qs) - - - - + let _defs = SMT.get_model solver.smt_solver in + let eval = + fun it -> + assert (have_model ()); + let sexp = translate_term solver it in + let res = SMT.get_expr solver.smt_solver sexp in + let ctys = get_ctype_table solver in + Some (get_ivalue solver.globals ctys (get_bt it) (SMT.no_let res)) + in + (eval, qs) (** Add an assertion. Quantified predicates are ignored. *) @@ -1340,9 +1326,6 @@ let make globals = s - - - (* (\** Evaluate terms in the context of a model computed by the solver. *\) *) (* let model_evaluator, reset_model_evaluator_state = *) (* (\* internal state for the model evaluator, reuses the solver across consecutive calls for efficiency *\) *) @@ -1410,7 +1393,6 @@ let make globals = (* in *) (* (model_evaluator, reset_model_evaluator_state) *) - (* ---------------------------------------------------------------------------*) module TryHard = struct @@ -1482,30 +1464,31 @@ let provableWithUnknown ~loc ~solver ~assumptions ~simp_ctxt lc = model_state := No_model; `True | SMT.Sat -> - (match !try_hard with + (match !try_hard with | true -> let assumptions = LC.Set.elements assumptions in let foralls = TryHard.translate_foralls solver assumptions in let functions = TryHard.translate_functions solver in Pp.(debug 3 (lazy !^"***** try-hard *****")); - (match SMT.check_assuming solver.smt_solver ((nexpr :: foralls) @ functions) with - | SMT.Unsat -> + (match + SMT.check_assuming solver.smt_solver ((nexpr :: foralls) @ functions) + with + | SMT.Unsat -> model_state := No_model; Pp.(debug 3 (lazy !^"***** try-hard: provable *****")); `True - | SMT.Sat -> + | SMT.Sat -> set_model solver qs; Pp.(debug 3 (lazy !^"***** try-hard: unprovable *****")); `False - | SMT.Unknown -> + | SMT.Unknown -> set_model solver qs; Pp.(debug 3 (lazy !^"***** try-hard: unknown *****")); `Unknown) | false -> - set_model solver qs; - `False) - | SMT.Unknown -> - failwith "Unknown") + set_model solver qs; + `False) + | SMT.Unknown -> failwith "Unknown") (** The main way to query the solver. *) @@ -1522,5 +1505,4 @@ let provable ~loc ~solver ~assumptions ~simp_ctxt ?(purpose = "") lc = (* TODO: remove this *) -let eval model t = - model t +let eval model t = model t diff --git a/lib/typeErrors.ml b/lib/typeErrors.ml index df3793efa..a469826d3 100644 --- a/lib/typeErrors.ml +++ b/lib/typeErrors.ml @@ -96,7 +96,7 @@ type message = situation : situation; (* ctxt : Context.t * Explain.log; *) (* model : Solver.model_with_q *) - report : Report.report; + report : Report.report } | Merging_multiple_arrays of { requests : RequestChain.t; @@ -109,7 +109,7 @@ type message = { resource : Res.t; (* ctxt : Context.t * Explain.log; *) (* model : Solver.model_with_q *) - report : Report.report; + report : Report.report } | Illtyped_binary_it of { left : IT.Surface.t; @@ -124,14 +124,14 @@ type message = value : IT.t; (* ctxt : Context.t * Explain.log; *) (* model : Solver.model_with_q *) - report : Report.report; + report : Report.report } | Int_unrepresentable of { value : IT.t; ict : Sctypes.t; (* ctxt : Context.t * Explain.log; *) (* model : Solver.model_with_q *) - report : Report.report; + report : Report.report } | Unproven_constraint of { constr : LC.t; @@ -139,13 +139,13 @@ type message = info : Locations.info; (* ctxt : Context.t * Explain.log; *) (* model : Solver.model_with_q *) - report : Report.report; + report : Report.report } | Undefined_behaviour of { ub : CF.Undefined.undefined_behaviour; (* ctxt : Context.t * Explain.log; *) (* model : Solver.model_with_q *) - report : Report.report; + report : Report.report } | Needs_alloc_id of { ptr : IT.t; @@ -160,7 +160,7 @@ type message = ub : CF.Undefined.undefined_behaviour; (* ctxt : Context.t * Explain.log; *) (* model : Solver.model_with_q *) - report : Report.report; + report : Report.report } | Allocation_not_live of { reason : From be958f648a929f47b15a3fe73a35582d5fc77bb6 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 2 Jul 2025 12:42:23 +0100 Subject: [PATCH 3/4] fix test output --- tests/cn/reverse.error.c.verify | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/cn/reverse.error.c.verify b/tests/cn/reverse.error.c.verify index 87972383a..297292326 100644 --- a/tests/cn/reverse.error.c.verify +++ b/tests/cn/reverse.error.c.verify @@ -13,5 +13,5 @@ tests/cn/reverse.error.c:124:3: error: Missing resource for de-allocating ^~~~~~~~~ Resource needed: W(&n3) which requires: W(&&n3->head) - other location (File "lib/resourceInference.ml", line 216, characters 31-38) (arg head) + other location (File "lib/resourceInference.ml", line 220, characters 31-38) (arg head) State file: file:///tmp/state__reverse.error.c__main.html From 2088dd175717cfec797092e697c3d0b109d0b343 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 2 Jul 2025 14:20:25 +0100 Subject: [PATCH 4/4] CVC5 setting for sets --- lib/simple_smt.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/simple_smt.ml b/lib/simple_smt.ml index f62c3ee36..c770f9d40 100644 --- a/lib/simple_smt.ml +++ b/lib/simple_smt.ml @@ -911,7 +911,7 @@ let cvc5 : solver_config = { exe = "cvc5"; (* opts = [ "--incremental"; "--sets-ext"; "--force-logic=QF_AUFBVDTLIA" ]; *) (* NOTE cvc5 1.2.1 renamed --sets-ext to --sets-exp *) - opts = [ "--incremental"; "--sets-ext"; "--force-logic=QF_ALL" ]; + opts = [ "--incremental"; "--sets-exp"; "--force-logic=QF_ALL" ]; setup = []; exts = CVC5; log = quiet_log