Skip to content

different CN/solver interaction for SMT counter models #240

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

different CN/solver interaction for SMT counter models #240

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
904208a
different CN/solver interaction for SMT counter models
cp526 Jul 2, 2025
5b53fa1
dune fmt
cp526 Jul 2, 2025
be958f6
fix test output
cp526 Jul 2, 2025
2088dd1
CVC5 setting for sets
cp526 Jul 2, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
61 changes: 46 additions & 15 deletions lib/check.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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? *)
Expand Down Expand Up @@ -434,7 +435,9 @@ 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 ()

Expand Down Expand Up @@ -463,7 +466,9 @@ let check_both_eq_alloc loc arg1 arg2 ub =
match provable @@ LC.T both_alloc with
| `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 } })
| `True -> return ()


Expand All @@ -485,7 +490,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 ()

Expand Down Expand Up @@ -660,7 +671,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
Expand All @@ -675,7 +688,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@ () =
Expand Down Expand Up @@ -882,7 +897,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) ->
Expand Down Expand Up @@ -915,7 +932,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
Expand Down Expand Up @@ -972,15 +991,19 @@ 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
(match provable (LC.T (bool_ false here)) with
| `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
Expand Down Expand Up @@ -1137,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 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 =
Expand Down Expand Up @@ -1421,7 +1444,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
let@ model = model () in
fail (fun ctxt ->
let ict = act_to.ct in
{ loc; msg = Int_unrepresentable { value = arg; ict; ctxt; model } })
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) ->
Expand Down Expand Up @@ -1622,9 +1646,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
Expand Down Expand Up @@ -1964,10 +1989,16 @@ 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;
msg =
Unproven_constraint
{ constr = lc; info = (loc, None); requests = []; ctxt; model }
{ constr = lc; info = (loc, None); requests = []; report }
}))
| Inline _nms -> return ()
| Print it ->
Expand Down
83 changes: 44 additions & 39 deletions lib/explain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -331,46 +331,51 @@ let state (ctxt : C.t) log model_with_q extras =
(Rp.add_labeled Rp.lab_uninteresting uninteresting Rp.labeled_empty)
in
let invalid_resources =
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: "
(* 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: "
^^^ 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
Expand Down
52 changes: 40 additions & 12 deletions lib/resourceInference.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,15 @@ 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)
Expand Down Expand Up @@ -120,10 +128,17 @@ 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)
Expand All @@ -142,16 +157,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, [])

Expand Down Expand Up @@ -477,7 +492,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

Expand Down Expand Up @@ -555,16 +576,23 @@ 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 }
TypeErrors.Allocation_not_live { reason; ptr; maybe_report = Some report }
in
{ loc; msg })

Expand Down
12 changes: 11 additions & 1 deletion lib/simple_smt.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -544,6 +544,16 @@ let check s =
| 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} *)

(** Get all definitions currently in scope. Only valid after a [Sat] result.
Expand Down Expand Up @@ -901,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
Expand Down
Loading
Loading