From 7ee200a861d4d3b3b27afd45cb789f06f8c79a0b Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 20 Dec 2025 10:39:49 +0000 Subject: [PATCH 01/14] Add a disjoint analysis --- soteria/lib/bv_values/analyses.ml | 106 +++++++++++++++++++++++++++++ soteria/lib/bv_values/bv_solver.ml | 8 +-- 2 files changed, 110 insertions(+), 4 deletions(-) diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml index 83eec600e..c17f83477 100644 --- a/soteria/lib/bv_values/analyses.ml +++ b/soteria/lib/bv_values/analyses.ml @@ -611,3 +611,109 @@ module Equality : S = struct let add_constraint st v = wrap (add_constraint v) st let encode ?vars:_ _st = Iter.empty end + +module Disjoint = struct + module VSet = Set.Make (Svalue) + module VMap = Map.Make (Svalue) + + include Reversible.Make_mutable (struct + type t = VSet.t VMap.t + + let default = VMap.empty + end) + + let[@inline] sort (v1 : Svalue.t) (v2 : Svalue.t) = + if v1.tag < v2.tag then (v1, v2) else (v2, v1) + + let var_set v = + Svalue.iter_vars v + |> Iter.map fst + |> Iter.fold (fun set x -> Var.Set.add x set) Var.Set.empty + + (** Adds inequalities between all values in [vs] to the state [st], returning + the updated state along with the set of variables that are dirty (i.e. + something was learnt from this). *) + let add_inequalities vs st = + let dirty = ref VSet.empty in + let vs = List.sort (fun v1 v2 -> Int.compare v1.Hc.tag v2.Hc.tag) vs in + let rec aux st = function + | [] | [ _ ] -> st + | v1 :: rest -> + let st = + VMap.update v1 + (fun s -> + let s = Option.value s ~default:VSet.empty in + let s, is_new' = + List.fold_left + (fun (s, is_new) v2 -> + assert (v1.Hc.tag < v2.Hc.tag); + if VSet.mem v2 s then (s, is_new) + else ( + dirty := VSet.add v2 !dirty; + (VSet.add v2 s, true))) + (s, false) rest + in + if is_new' then dirty := VSet.add v1 !dirty; + Some s) + st + in + aux st rest + in + let st = aux st vs in + let dirty = + VSet.fold (fun v -> Var.Set.union (var_set v)) !dirty Var.Set.empty + in + (dirty, st) + + let[@inline] is_relevant : Svalue.t -> bool = function + | { node = { ty = TLoc _; _ }; _ } -> true + | _ -> false + + let add_constraint (v : Svalue.t) st = + match v.node.kind with + | Unop (Not, { node = { kind = Binop (Eq, l, r); _ }; _ }) + when is_relevant l && is_relevant r -> + let l, r = sort l r in + let vars, st = add_inequalities [ l; r ] st in + ((Svalue.Bool.v_true, vars), st) + | Nop (Distinct, vs) when List.hd vs |> is_relevant -> + let vars, st = add_inequalities vs st in + ((Svalue.Bool.v_true, vars), st) + | _ -> ((v, Var.Set.empty), st) + + let simplify (v : Svalue.t) st = + match v.node.kind with + | Binop (Eq, l, r) when is_relevant l && is_relevant r -> ( + let l, r = sort l r in + match VMap.find_opt l st with + | None -> v + | Some s -> if VSet.mem r s then Svalue.Bool.v_false else v) + | Unop (Not, { node = { kind = Binop (Eq, l, r); _ }; _ }) + when is_relevant l && is_relevant r -> ( + let l, r = sort l r in + match VMap.find_opt l st with + | None -> v + | Some s -> if VSet.mem r s then Svalue.Bool.v_true else v) + | _ -> v + + let simplify st v = wrap_read (simplify v) st + let add_constraint st v = wrap (add_constraint v) st + let mk_var n v = Typed.mk_var v (Typed.t_int n) + let uneq l r = Typed.not (Typed.sem_eq (Typed.type_ l) (Typed.type_ r)) + + let encode ?vars st : Typed.sbool Typed.t Iter.t = + let to_check = + Option.fold ~none:(fun _ -> true) ~some:Var.Hashset.mem vars + in + let to_check v = + Iter.exists to_check (Svalue.iter_vars v |> Iter.map fst) + in + wrap_read + (fun m f -> + VMap.iter + (fun v s -> + if to_check v then VSet.iter (fun v2 -> f (uneq v v2)) s + else VSet.iter (fun v2 -> if to_check v2 then f (uneq v v2)) s) + m) + st +end diff --git a/soteria/lib/bv_values/bv_solver.ml b/soteria/lib/bv_values/bv_solver.ml index 363cf04a0..eaff44eb6 100644 --- a/soteria/lib/bv_values/bv_solver.ml +++ b/soteria/lib/bv_values/bv_solver.ml @@ -550,8 +550,8 @@ struct |> Iter.to_list end +open Analyses +module Analysis = Merge (Interval) (Equality) module Z3 = Solvers.Z3.Make (Encoding) -module Z3_incremental_solver = Make_incremental (Analyses.None) (Z3) - -module Z3_solver = - Make (Analyses.Merge (Analyses.Interval) (Analyses.Equality)) (Z3) +module Z3_incremental_solver = Make_incremental (Analysis) (Z3) +module Z3_solver = Make (Analysis) (Z3) From b4f2d268227ba900146885f84e48bd62c74543ce Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 20 Dec 2025 16:01:14 +0000 Subject: [PATCH 02/14] Better reduce `Svalue.distinct` --- soteria/lib/bv_values/svalue.ml | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/soteria/lib/bv_values/svalue.ml b/soteria/lib/bv_values/svalue.ml index 4ca99b63e..6475e3122 100644 --- a/soteria/lib/bv_values/svalue.ml +++ b/soteria/lib/bv_values/svalue.ml @@ -717,12 +717,21 @@ module rec Bool : Bool = struct (* [Distinct l] when l is empty or of size 1 is always true *) match l with | [] | [ _ ] -> v_true - | l -> + | l -> ( let cross_product = List.to_seq l |> Seq.self_cross_product in - let sure_distinct = - Seq.for_all (fun (a, b) -> sure_neq a b) cross_product + let rec aux seq = + match seq () with + | Seq.Nil -> Some true + | Seq.Cons ((a, b), rest) -> + if equal a b then Some false + else if sure_neq a b then aux rest + else None in - if sure_distinct then v_true else Nop (Distinct, l) <| TBool + let res = aux cross_product in + match res with + | Some true -> v_true + | Some false -> v_false + | None -> Nop (Distinct, l) <| TBool) end (** {2 Bit vectors} *) From 31680baa41872ef7b8baffff6b942197b508e709 Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 20 Dec 2025 16:02:03 +0000 Subject: [PATCH 03/14] Handle `not (distinct _)` in eq analysis --- soteria/lib/bv_values/analyses.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml index c17f83477..948445893 100644 --- a/soteria/lib/bv_values/analyses.ml +++ b/soteria/lib/bv_values/analyses.ml @@ -605,6 +605,17 @@ module Equality : S = struct This also means this analysis is exempt from implementing [encode], since it doesn't store anything. *) ((v, Var.Set.empty), st) + | Unop (Not, { node = { kind = Nop (Distinct, hd :: tl); _ }; _ }) -> + let v1, st = get_or_make hd st in + let rec aux st = function + | [] -> st + | v2 :: rest -> + let v2, st = get_or_make v2 st in + merge v1 v2 st; + aux st rest + in + let st = aux st tl in + ((v, Var.Set.empty), st) | _ -> ((v, Var.Set.empty), st) let simplify st v = wrap_read (simplify v) st From b51431d098d8f0d1274c013fcf64789fae0b4527 Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 20 Dec 2025 16:03:37 +0000 Subject: [PATCH 04/14] Re-introduce `AddOvf` --- soteria/lib/bv_values/encoding.ml | 2 ++ soteria/lib/bv_values/eval.ml | 1 + soteria/lib/bv_values/svalue.ml | 21 ++++----------------- 3 files changed, 7 insertions(+), 17 deletions(-) diff --git a/soteria/lib/bv_values/encoding.ml b/soteria/lib/bv_values/encoding.ml index 679a3f67a..90fcd1b49 100644 --- a/soteria/lib/bv_values/encoding.ml +++ b/soteria/lib/bv_values/encoding.ml @@ -82,6 +82,8 @@ let smt_of_binop : Svalue.Binop.t -> sexp -> sexp -> sexp = function | Rem true -> bv_srem | Rem false -> bv_urem | Mod -> bv_smod + | AddOvf true -> bv_saddo + | AddOvf false -> bv_uaddo | MulOvf true -> bv_smulo | MulOvf false -> bv_umulo | Lt true -> bv_slt diff --git a/soteria/lib/bv_values/eval.ml b/soteria/lib/bv_values/eval.ml index 8d7003c1c..e83c05d88 100644 --- a/soteria/lib/bv_values/eval.ml +++ b/soteria/lib/bv_values/eval.ml @@ -19,6 +19,7 @@ let eval_binop : Binop.t -> t -> t -> t = function | Div signed -> BitVec.div ~signed | Rem signed -> BitVec.rem ~signed | Mod -> BitVec.mod_ + | AddOvf signed -> BitVec.add_overflows ~signed | MulOvf signed -> BitVec.mul_overflows ~signed | Lt signed -> BitVec.lt ~signed | Leq signed -> BitVec.leq ~signed diff --git a/soteria/lib/bv_values/svalue.ml b/soteria/lib/bv_values/svalue.ml index 6475e3122..7893fdf09 100644 --- a/soteria/lib/bv_values/svalue.ml +++ b/soteria/lib/bv_values/svalue.ml @@ -140,6 +140,7 @@ module Binop = struct | Div of bool (* signed *) | Rem of bool (* signed *) | Mod + | AddOvf of bool (* signed *) | MulOvf of bool (* signed *) | Lt of bool (* signed *) | Leq of bool (* signed *) @@ -174,6 +175,7 @@ module Binop = struct | Div s -> Fmt.pf ft "/%a" pp_signed s | Rem s -> Fmt.pf ft "rem%a" pp_signed s | Mod -> Fmt.string ft "mod" + | AddOvf s -> Fmt.pf ft "+%a_ovf" pp_signed s | MulOvf s -> Fmt.pf ft "*%a_ovf" pp_signed s | Lt s -> Fmt.pf ft "<%a" pp_signed s | Leq s -> Fmt.pf ft "<=%a" pp_signed s @@ -1726,22 +1728,7 @@ and BitVec : BitVec = struct let max = max_for signed n in let other = other <| t_bv n in Bool.and_ b (Bool.sem_eq other (mk n max)) - | _ -> - let size = size_of v1.node.ty in - if signed then - let sign_of v = lt ~signed v (zero size) in - let sign_l = sign_of v1 in - let sign_r = sign_of v2 in - let msb_res = sign_of (add v1 v2) in - Bool.and_ - (Bool.sem_eq sign_l sign_r) - (Bool.not (Bool.sem_eq sign_l msb_res)) - else - let max = max_for signed size in - let max = mk size max in - Bool.or_ - (gt ~signed v1 (sub ~checked:true max v2)) - (gt ~signed v2 (sub ~checked:true max v1)) + | _ -> mk_commut_binop (AddOvf signed) v1 v2 <| TBool let mul_overflows ~signed v1 v2 = match (v1.node.kind, v2.node.kind) with @@ -1790,7 +1777,7 @@ and BitVec : BitVec = struct let maxn = Z.pred (Z.shift_left Z.one n) in let bound = Z.(maxn / z) in gt ~signed (x <| v1.node.ty) (mk n bound) - | _ -> Binop (MulOvf signed, v1, v2) <| TBool + | _ -> mk_commut_binop (MulOvf signed) v1 v2 <| TBool let neg_overflows v = let n = size_of v.node.ty in From 7eff7a373343ac71bcb7be7268eb968033977959 Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 20 Dec 2025 17:13:09 +0000 Subject: [PATCH 05/14] Reduce `n +sovf x` --- soteria/lib/bv_values/analyses.ml | 6 ++---- soteria/lib/bv_values/svalue.ml | 18 ++++++++++++++---- 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml index 948445893..21836b2ec 100644 --- a/soteria/lib/bv_values/analyses.ml +++ b/soteria/lib/bv_values/analyses.ml @@ -87,9 +87,6 @@ module Interval : S = struct type sign = Pos | Neg - (** Sign multiplication *) - let ( ** ) l r = if l = r then Pos else Neg - let pp_sign fmt = function | Pos -> Fmt.string fmt "+" | Neg -> Fmt.string fmt "-" @@ -404,7 +401,8 @@ module Interval : S = struct a disjunction! *) | Unop (Not, v) -> Option.map - (fun (v1, size, (sign, range)) -> (v1, size, (Neg ** sign, range))) + (fun (v1, size, (sign, range)) -> + (v1, size, ((if sign = Neg then Pos else Neg), range))) (as_range v) | _ -> None diff --git a/soteria/lib/bv_values/svalue.ml b/soteria/lib/bv_values/svalue.ml index 7893fdf09..3218ffc67 100644 --- a/soteria/lib/bv_values/svalue.ml +++ b/soteria/lib/bv_values/svalue.ml @@ -1713,14 +1713,24 @@ and BitVec : BitVec = struct | _, BitVec z when Z.equal z Z.zero -> Bool.v_false | BitVec z, _ when Stdlib.not signed -> let n = size_of v1.node.ty in - let z = bv_to_z signed n z in let m = max_for signed n in - gt ~signed v2 (mk_masked n Z.(m - z)) + gt ~signed v2 (mk n Z.(m - z)) | _, BitVec z when Stdlib.not signed -> let n = size_of v1.node.ty in - let z = bv_to_z signed n z in let m = max_for signed n in - gt ~signed v1 (mk_masked n Z.(m - z)) + gt ~signed v1 (mk n Z.(m - z)) + | (BitVec z, x | x, BitVec z) when signed -> + let x = if x == v1.node.kind then v1 else v2 in + let n = size_of v1.node.ty in + let z = bv_to_z signed n z in + if Z.gt z Z.zero then + (* z > 0 so overflows if max - z < x *) + let max = max_for signed n in + gt ~signed x (mk n (Z.sub max z)) + else + (* z < 0 so overflows if x < min - z *) + let min = min_for signed n in + lt ~signed x (mk_masked n (Z.sub min z)) | Unop (BvOfBool _, _), Unop (BvOfBool _, _) -> Bool.v_false | Unop (BvOfBool _, b), other | other, Unop (BvOfBool _, b) -> (* ite(b, 1, 0) + x only overflows if b && x == max *) From 6d30d85387e7888a6a40793bd9f497950ac57ca9 Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 20 Dec 2025 11:46:42 +0000 Subject: [PATCH 06/14] Remove `Declared_vars` from non-incr `Bv_solver` --- soteria/lib/bv_values/bv_solver.ml | 68 +++++++----------------------- 1 file changed, 15 insertions(+), 53 deletions(-) diff --git a/soteria/lib/bv_values/bv_solver.ml b/soteria/lib/bv_values/bv_solver.ml index eaff44eb6..a95433ee5 100644 --- a/soteria/lib/bv_values/bv_solver.ml +++ b/soteria/lib/bv_values/bv_solver.ml @@ -368,45 +368,9 @@ struct (to_encode, var_set) end - module Declared_vars = struct - module Var_counter = Var.Incr_counter_mut (struct - let start_at = 1 - end) - - (* Since we start addresses at one to improve trivial model hits, we need to offset to obtain an index. *) - let var_to_index v = Var.to_int v - 1 - - type t = { - counter : Var_counter.t; - types : Svalue.ty Dynarray.t; - (** The var_counter is keeping track of how many variables we actually - have in the context. We don't need to separate each bit of that - array by saved branch, we just fetch at the index for each - variable, and override when we change branch. *) - } - - let init () = { counter = Var_counter.init (); types = Dynarray.create () } - let save t = Var_counter.save t.counter - let backtrack_n t n = Var_counter.backtrack_n t.counter n - let reset t = Var_counter.reset t.counter - - let fresh t ty = - let next = Var_counter.get_next t.counter in - let next_i = var_to_index next in - let () = - if Dynarray.length t.types == next_i then Dynarray.add_last t.types ty - else if Dynarray.length t.types > next_i then - Dynarray.set t.types next_i ty - else failwith "Broke var-counter/declared-types invariant" - in - next - - let get_ty t var = Dynarray.get t.types (var_to_index var) - end - type t = { z3_exe : Intf.t; - vars : Declared_vars.t; + vars : Var_counter.t; save_counter : Save_counter.t; state : Solver_state.t; analysis : Analysis.t; @@ -418,19 +382,19 @@ struct { z3_exe; save_counter = Save_counter.init (); - vars = Declared_vars.init (); + vars = Var_counter.init (); state = Solver_state.init (); analysis = Analysis.init (); } let save solver = - Declared_vars.save solver.vars; + Var_counter.save solver.vars; Save_counter.save solver.save_counter; Solver_state.save solver.state; Analysis.save solver.analysis let backtrack_n solver n = - Declared_vars.backtrack_n solver.vars n; + Var_counter.backtrack_n solver.vars n; Solver_state.backtrack_n solver.state n; Save_counter.backtrack_n solver.save_counter n; Analysis.backtrack_n solver.analysis n @@ -442,12 +406,11 @@ struct let save_counter = !(solver.save_counter) in if save_counter < 0 then failwith "Solver reset: save_counter < 0???"; Save_counter.reset solver.save_counter; - Declared_vars.reset solver.vars; + Var_counter.reset solver.vars; Solver_state.reset solver.state; Analysis.reset solver.analysis - let fresh_var solver ty = - Declared_vars.fresh solver.vars (Typed.untype_type ty) + let fresh_var solver _ = Var_counter.get_next solver.vars let simplify solver v : 'a Typed.t = v @@ -498,30 +461,29 @@ struct let res = Eval.eval ~eval_var to_check in Svalue.equal res Svalue.Bool.v_true - let check_sat_raw solver relevant_vars to_check = + let check_sat_raw solver to_check = (* TODO: we shouldn't wait for ack for each command individually... *) + let var_tys = + Svalue.iter_vars to_check + |> Iter.fold (fun acc (v, ty) -> Var.Map.add v ty acc) Var.Map.empty + in if trivial_model_works to_check then Symex.Solver_result.Sat else ( (* We need to reset the state, so we can push the new constraints *) Intf.reset solver.z3_exe; - (* Declare all relevant variables *) - Var.Hashset.iter - (fun v -> - let ty = Declared_vars.get_ty solver.vars v in - Intf.declare_var solver.z3_exe v ty) - relevant_vars; + Var.Map.iter (Intf.declare_var solver.z3_exe) var_tys; (* Declare the constraint *) Intf.add_constraint solver.z3_exe to_check; (* Actually check sat *) Intf.check_sat solver.z3_exe) - let check_sat_raw_memo solver relevant_vars to_check = + let check_sat_raw_memo solver to_check = let to_check = Typed.untyped to_check in match Hashtbl.Hint.find_opt memo_sat_check_tbl to_check.Hc.tag with | Some result -> result | None -> - let result = check_sat_raw solver relevant_vars to_check in + let result = check_sat_raw solver to_check in Hashtbl.Hint.add memo_sat_check_tbl to_check.Hc.tag result; result @@ -539,7 +501,7 @@ struct Iter.fold Typed.and_ to_check (Analysis.encode ~vars:relevant_vars solver.analysis) in - let answer = check_sat_raw_memo solver relevant_vars to_check in + let answer = check_sat_raw_memo solver to_check in if answer = Sat then Solver_state.mark_checked solver.state; answer From e7a27f8c4c7f929c3bc76cb1b68192e225218300 Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 20 Dec 2025 15:34:57 +0000 Subject: [PATCH 07/14] Add `Analyses.filter` --- soteria/lib/bv_values/analyses.ml | 75 ++++++++++++++++++++++++++++- soteria/lib/bv_values/bv_solver.ml | 76 ++++++++++++++++++------------ 2 files changed, 121 insertions(+), 30 deletions(-) diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml index 21836b2ec..a82008688 100644 --- a/soteria/lib/bv_values/analyses.ml +++ b/soteria/lib/bv_values/analyses.ml @@ -16,6 +16,10 @@ module type S = sig data. *) val add_constraint : t -> Svalue.t -> Svalue.t * Var.Set.t + (** Filters the given iterator of symbolic values, keeping only those relevant + to the given variable according to the analysis. *) + val filter : t -> Var.t -> Svalue.ty -> Svalue.t Iter.t -> Svalue.t Iter.t + (** Encode all the information relevant to the given variables and conjuncts them with the given accumulator. *) val encode : ?vars:Var.Hashset.t -> t -> Typed.sbool Typed.t Iter.t @@ -45,6 +49,9 @@ module Merge (A1 : S) (A2 : S) : S = struct let v'', vars2 = A2.add_constraint a2 v' in (v'', Var.Set.union vars1 vars2) + let filter (a1, a2) var ty vs = + vs |> A1.filter a1 var ty |> A2.filter a2 var ty + let encode ?vars (a1, a2) : Typed.sbool Typed.t Iter.t = Iter.append (A1.encode ?vars a1) (A2.encode ?vars a2) end @@ -58,6 +65,7 @@ module None : S = struct let reset () = () let simplify () v = v let add_constraint () v = (v, Var.Set.empty) + let filter () _ _ vs = vs let encode ?vars:_ () = Iter.empty end @@ -484,8 +492,46 @@ module Interval : S = struct else log (fun m -> m "No change.@."); ((v' &&@ learnt, vars), st') + let filter var ty vs st = + match ty with + | Svalue.TBitVector _ -> ( + let range_opt = Var.Map.find_opt var st in + match range_opt with + | None -> vs + | Some range -> + let l, h = range.Data.pos in + Iter.filter + (fun (v : Svalue.t) -> + match v.node.kind with + | BitVec z -> + Z.Compare.(l <= z && z <= h) + && List.for_all + (fun (m, n) -> Z.Compare.(z < m || n < z)) + range.Data.negs + | _ -> true) + vs + (* if it turns out too slow to filter for a valid value, + we could also just iterate over every value in the range: *) + (* let rec iter z f = + f (Svalue.BitVec.mk n z); + + (* if a negative range exists, update to next value *) + let z = Z.succ z in + let neg = + List.find_opt + (fun (m, n) -> Z.Compare.(m <= z && z <= n)) + range.Data.negs + in + let z' = match neg with None -> z | Some (_, n) -> Z.succ n in + if Z.Compare.(z' <= h) then iter z' f + in + iter l *) + ) + | _ -> vs + let simplify st v = wrap_read (simplify v) st let add_constraint st v = wrap (add_constraint v) st + let filter st var ty vs = wrap_read (filter var ty vs) st let encode ?vars st : Typed.sbool Typed.t Iter.t = let to_check = @@ -616,8 +662,18 @@ module Equality : S = struct ((v, Var.Set.empty), st) | _ -> ((v, Var.Set.empty), st) + (** In equality analysis we can be certain of the value of a variable, so we + can entirely replace the set of possible values [vs] with the + representative value (if any). *) + let filter var ty vs st = + let v = Svalue.mk_var var ty in + match find_cheaper_opt v st with + | None -> vs + | Some v_repr -> Iter.singleton v_repr + let simplify st v = wrap_read (simplify v) st let add_constraint st v = wrap (add_constraint v) st + let filter st var ty vs = wrap_read (filter var ty vs) st let encode ?vars:_ _st = Iter.empty end @@ -631,6 +687,12 @@ module Disjoint = struct let default = VMap.empty end) + let pp ft st = + Fmt.( + iter_bindings VMap.iter + (pair ~sep:(any " -> ") Svalue.pp (iter VSet.iter Svalue.pp))) + ft st + let[@inline] sort (v1 : Svalue.t) (v2 : Svalue.t) = if v1.tag < v2.tag then (v1, v2) else (v2, v1) @@ -675,7 +737,9 @@ module Disjoint = struct (dirty, st) let[@inline] is_relevant : Svalue.t -> bool = function - | { node = { ty = TLoc _; _ }; _ } -> true + | { node = { ty = TLoc _; _ }; _ } + | { node = { kind = BitVec _ | Var _; _ }; _ } -> + true | _ -> false let add_constraint (v : Svalue.t) st = @@ -705,8 +769,17 @@ module Disjoint = struct | Some s -> if VSet.mem r s then Svalue.Bool.v_true else v) | _ -> v + let filter v ty st = + let v1 = Svalue.mk_var v ty in + Iter.filter (fun v2 -> + let v1, v2 = sort v1 v2 in + match VMap.find_opt v1 st with + | None -> true + | Some s -> not (VSet.mem v2 s)) + let simplify st v = wrap_read (simplify v) st let add_constraint st v = wrap (add_constraint v) st + let filter st var ty = wrap_read (filter var ty) st let mk_var n v = Typed.mk_var v (Typed.t_int n) let uneq l r = Typed.not (Typed.sem_eq (Typed.type_ l) (Typed.type_ r)) diff --git a/soteria/lib/bv_values/bv_solver.ml b/soteria/lib/bv_values/bv_solver.ml index a95433ee5..dacc428ab 100644 --- a/soteria/lib/bv_values/bv_solver.ml +++ b/soteria/lib/bv_values/bv_solver.ml @@ -432,34 +432,52 @@ struct let memo_sat_check_tbl : Symex.Solver_result.t Hashtbl.Hint.t = Hashtbl.Hint.create 1023 - let trivial_model_works to_check = - (* We try a trivial model where replacing each variable with name - [|n|] with the corresponding integer [n]; except if an assertion - [|n| == v] exists, in which case we replace it with the value [v]. - If the constraint evaluates to true, then it is satisfiable. *) - let v_eqs = Var.Hashtbl.create 8 in - Svalue.Bool.split_ands to_check (fun v -> - match v.node.kind with - | Binop - ( Eq, - { node = { kind = Var n; _ }; _ }, - ({ node = { kind = BitVec _; _ }; _ } as x) ) - | Binop - ( Eq, - ({ node = { kind = BitVec _; _ }; _ } as x), - { node = { kind = Var n; _ }; _ } ) -> - Var.Hashtbl.add v_eqs n x - | _ -> ()); - let eval_var v_var v (ty : Svalue.ty) = - match ty with - | TBitVector n | TLoc n -> ( - let i = Var.to_int v in - try Var.Hashtbl.find v_eqs v - with Not_found -> Svalue.BitVec.mk_masked n (Z.of_int i)) - | _ -> v_var + let trivial_model_works solver to_check var_tys = + let exception No_model in + let value_generator : Svalue.ty -> unit -> Svalue.t = function + | TLoc n -> + let max = Z.(shift_left one n) in + fun () -> Svalue.Ptr.loc_of_z n (Z.random_int max) + | TBitVector n -> + let max = Z.(shift_left one n) in + fun () -> Svalue.BitVec.mk n (Z.random_int max) + | TBool -> fun () -> Svalue.Bool.bool (Random.bool ()) + (* TODO: because we can't evaluate floats, we can never do a + trivial check for them. *) + | TFloat _ -> raise No_model + (* TODO: figure this out *) + | TPointer _ | TSeq _ -> raise No_model in - let res = Eval.eval ~eval_var to_check in - Svalue.equal res Svalue.Bool.v_true + let fuel = 3 in + try + let var_values = + Var.Map.fold + (fun v (ty : Svalue.ty) acc -> + let values = + Iter.forever (value_generator ty) + |> Analysis.filter solver.analysis v ty + |> Iter.take fuel + |> Iter.to_array + in + if Array.length values = 0 then raise No_model; + Var.Map.add v values acc) + var_tys Var.Map.empty + in + let rec aux i = + let rec eval_var _ v _ = + let values = Var.Map.find v var_values in + let index = i mod Array.length values in + match values.(index) with + | { node = { kind = Var var; ty }; _ } as v -> eval_var v var ty + | v -> v + in + let res = Eval.eval ~eval_var to_check in + if Svalue.equal res Svalue.Bool.v_true then true + else if i >= fuel then false + else aux (i + 1) + in + aux 0 + with No_model -> false let check_sat_raw solver to_check = (* TODO: we shouldn't wait for ack for each command individually... *) @@ -467,7 +485,7 @@ struct Svalue.iter_vars to_check |> Iter.fold (fun acc (v, ty) -> Var.Map.add v ty acc) Var.Map.empty in - if trivial_model_works to_check then Symex.Solver_result.Sat + if trivial_model_works solver to_check var_tys then Symex.Solver_result.Sat else ( (* We need to reset the state, so we can push the new constraints *) Intf.reset solver.z3_exe; @@ -513,7 +531,7 @@ struct end open Analyses -module Analysis = Merge (Interval) (Equality) +module Analysis = Merge (Merge (Interval) (Equality)) (Disjoint) module Z3 = Solvers.Z3.Make (Encoding) module Z3_incremental_solver = Make_incremental (Analysis) (Z3) module Z3_solver = Make (Analysis) (Z3) From 449005f1893822454d00b483c6325797213a06eb Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 20 Dec 2025 20:07:54 +0000 Subject: [PATCH 08/14] Fix interval analysis filter --- soteria/lib/bv_values/analyses.ml | 43 ++++++++++++------------------- 1 file changed, 16 insertions(+), 27 deletions(-) diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml index a82008688..4828119d7 100644 --- a/soteria/lib/bv_values/analyses.ml +++ b/soteria/lib/bv_values/analyses.ml @@ -494,39 +494,28 @@ module Interval : S = struct let filter var ty vs st = match ty with - | Svalue.TBitVector _ -> ( + | Svalue.TBitVector n -> ( let range_opt = Var.Map.find_opt var st in match range_opt with | None -> vs | Some range -> + (* In sparsely populated ranges (e.g. [0, 1000] - [1, 999]), filtering + can be very slow since the odds of getting a valid integer is so low. + Because of this, we reset the iterator and generate values ourselves. *) let l, h = range.Data.pos in - Iter.filter - (fun (v : Svalue.t) -> - match v.node.kind with - | BitVec z -> - Z.Compare.(l <= z && z <= h) - && List.for_all - (fun (m, n) -> Z.Compare.(z < m || n < z)) - range.Data.negs - | _ -> true) - vs - (* if it turns out too slow to filter for a valid value, - we could also just iterate over every value in the range: *) - (* let rec iter z f = - f (Svalue.BitVec.mk n z); - - (* if a negative range exists, update to next value *) - let z = Z.succ z in - let neg = - List.find_opt - (fun (m, n) -> Z.Compare.(m <= z && z <= n)) - range.Data.negs + let rec iter z f = + f (Svalue.BitVec.mk n z); + (* if a negative range exists, update to next value *) + let z = Z.succ z in + let neg = + List.find_opt + (fun (m, n) -> Z.Compare.(m <= z && z <= n)) + range.Data.negs + in + let z' = match neg with None -> z | Some (_, n) -> Z.succ n in + if Z.Compare.(z' <= h) then iter z' f in - let z' = match neg with None -> z | Some (_, n) -> Z.succ n in - if Z.Compare.(z' <= h) then iter z' f - in - iter l *) - ) + iter l) | _ -> vs let simplify st v = wrap_read (simplify v) st From e3b4b5cbf13818d44c602db55ba5c7d094cdb428 Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 20 Dec 2025 20:08:02 +0000 Subject: [PATCH 09/14] Tests --- soteria-c/test/cram/fixme.t/run.t | 4 +- soteria-c/test/cram/simple_bi.t/run.t | 39 ++++++--------- soteria-rust/test/cram/kani.t/run.t | 71 +++++++++++++-------------- 3 files changed, 51 insertions(+), 63 deletions(-) diff --git a/soteria-c/test/cram/fixme.t/run.t b/soteria-c/test/cram/fixme.t/run.t index 229dd08d6..a967efa74 100644 --- a/soteria-c/test/cram/fixme.t/run.t +++ b/soteria-c/test/cram/fixme.t/run.t @@ -6,8 +6,8 @@ raw = { args = []; pre = []; pc = - [(0x0000000000000000 != V|1|); (0x0000000000000000 != V|2|); - (V|1| == V|2|)]; + [(V|1| == V|2|); (0x0000000000000000 != V|1|); + (0x0000000000000000 != V|2|)]; post = { heap = [(V|2|, diff --git a/soteria-c/test/cram/simple_bi.t/run.t b/soteria-c/test/cram/simple_bi.t/run.t index 9477bb36c..76de7c33d 100644 --- a/soteria-c/test/cram/simple_bi.t/run.t +++ b/soteria-c/test/cram/simple_bi.t/run.t @@ -23,7 +23,7 @@ info = None })]; globs = [] } ]; - pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)]; + pc = [(V|2| <=u 0x7ffffffffffffffb); (0x0000000000000000 != V|1|)]; post = { heap = [(V|1|, @@ -122,7 +122,7 @@ NO_COLOR=true is necessary to avoid test output changing in CI. For some reason, info = None })]; globs = [] } ]; - pc = [(0x0000000000000000 != V|1|); (V|2| <=u 0x7ffffffffffffffb)]; + pc = [(V|2| <=u 0x7ffffffffffffffb); (0x0000000000000000 != V|1|)]; post = { heap = [(V|1|, @@ -254,8 +254,8 @@ if%sat1 had the wrong semantics and would not correctly backtrack. globs = [] } ]; pc = - [(0x0000000000000000 != V|2|); (0x00000001 <=u V|1|); - (V|1| <=u 0x7fffffff); (V|3| <=u 0x7ffffffffffffffb)]; + [(0x00000001 <=u V|1|); (V|1| <=u 0x7fffffff); + (V|3| <=u 0x7ffffffffffffffb); (0x0000000000000000 != V|2|)]; post = { heap = [(V|2|, @@ -308,8 +308,8 @@ if%sat1 had the wrong semantics and would not correctly backtrack. globs = [] } ]; pc = - [(0x0000000000000000 != V|1|); (V|3| == 0x00000001); - (V|2| <=u 0x7ffffffffffffffb); (V|3| == 0x00000001)]; + [(V|3| == 0x00000001); (V|2| <=u 0x7ffffffffffffffb); + (V|3| == 0x00000001); (0x0000000000000000 != V|1|)]; post = { heap = [(V|1|, @@ -340,12 +340,9 @@ if%sat1 had the wrong semantics and would not correctly backtrack. globs = [] } ]; pc = - [(0x0000000000000000 != V|1|); - (0x0000000000000000 <=s (V|2| + 0x0000000000000004)); - ((V|4| note: len_capacity_invariant: done in