From f3bcaca332cd3313e8d02edb9ea780e6892cf6e1 Mon Sep 17 00:00:00 2001 From: JTrenerry <105094182+JTrenerry@users.noreply.github.com> Date: Thu, 9 Apr 2026 13:59:45 +1000 Subject: [PATCH 1/8] SVA? --- lib/analysis/dune | 4 +- lib/analysis/lattice_collections.ml | 11 + lib/analysis/sva.ml | 339 ++++++++++++++++++++++++++++ lib/passes.ml | 13 ++ test/lang/test_value_soundness.ml | 2 + 5 files changed, 367 insertions(+), 2 deletions(-) create mode 100644 lib/analysis/sva.ml diff --git a/lib/analysis/dune b/lib/analysis/dune index 0ccdfcd0..13dcefb1 100644 --- a/lib/analysis/dune +++ b/lib/analysis/dune @@ -13,12 +13,12 @@ ide_live lattice_collections wrapped_intervals - known_bits gamma_domain + linear_const tnum_wint_reduced_product known_bits wp_dual - linear_const) + sva) (libraries intPQueue patricia-tree diff --git a/lib/analysis/lattice_collections.ml b/lib/analysis/lattice_collections.ml index 4ca40967..9d6ed174 100644 --- a/lib/analysis/lattice_collections.ml +++ b/lib/analysis/lattice_collections.ml @@ -78,6 +78,7 @@ module LatticeMap (K : MapKey) (V : TopLattice) = struct let name = V.name ^ "MapLattice" let bottom = BotMap KM.empty let top = TopMap KM.empty + let singleton k v = BotMap (KM.singleton k v) let top_vjoin _ x y = let j = V.join x y in @@ -195,6 +196,13 @@ module LatticeMap (K : MapKey) (V : TopLattice) = struct let to_list = function | BotMap m -> (`Bottom, KM.to_list m) | TopMap m -> (`Top, KM.to_list m) + + let mapi f = function + | BotMap m -> BotMap (KM.mapi f m) + | TopMap m -> TopMap (KM.mapi f m) + + let fold f m acc = + match m with BotMap m -> KM.fold f m acc | TopMap m -> KM.fold f m acc end : sig include StateAbstraction with type val_t = V.t and type key_t = K.t @@ -204,6 +212,9 @@ module LatticeMap (K : MapKey) (V : TopLattice) = struct val of_list_bot : (K.t * V.t) list -> t val cardinal : t -> int val to_list : t -> [ `Bottom | `Top ] * (K.t * V.t) list + val singleton : K.t -> V.t -> t + val mapi : (K.t -> V.t -> V.t) -> t -> t + val fold : (K.t -> V.t -> 'a -> 'a) -> t -> 'a -> 'a end) module V = V diff --git a/lib/analysis/sva.ml b/lib/analysis/sva.ml new file mode 100644 index 00000000..16fcec2f --- /dev/null +++ b/lib/analysis/sva.ml @@ -0,0 +1,339 @@ +(* + SVA analysis + - Based off of the DSA paper + the first iteration I believe as newer one have had the SVA sections reduced + + Note: This does not result in amazing results currently, may need a paper focused + on SVA or more research to improve it, it only really works with mallocs (for + type inference use case) +*) + +open Lang +open Containers +open Common +open Wrapped_intervals + +(* + TODO + Figure out what the SymBases should actually have in them, is it just for cute printing? +*) + +module SymBase = struct + type t = + (* Known *) + | Stack of string + | Heap of { name : string } + | GlobSym + | Constant + (* Unknown *) + | Par of { name : string; param : Var.t } + | Ret of { name : string; param : Var.t } + | Loaded + [@@deriving ord, eq] + + let show = function + | Stack name -> Printf.sprintf "Stack(%s)" name + | Heap { name } -> Printf.sprintf "Heap(%s)" name + | GlobSym -> "Global" + | Constant -> "Constant" + | Par { name; param } -> Printf.sprintf "Par(%s_%s)" name (Var.show param) + | Ret { name; param } -> Printf.sprintf "Ret(%s_%s)" name (Var.show param) + | Loaded -> Printf.sprintf "Loaded" + + let is_place_holder = function + | Stack _ | Heap _ | GlobSym | Constant -> false + | Ret _ | Par _ | Loaded -> true + + let to_int = Hashtbl.hash + let pretty a = Containers_pp.int 1 + let is_stack = function Stack _ -> true | _ -> false +end + +module IntervalDomain = struct + open WrappedIntervalsLattice + + type t = WrappedIntervalsLattice.t [@@deriving eq, ord] + + let name = "interval offsets domain " + let pretty = WrappedIntervalsLattice.pretty + let show = WrappedIntervalsLattice.show + let bottom = WrappedIntervalsLattice.bottom + let leq = WrappedIntervalsLattice.leq + let widening = WrappedIntervalsLattice.widening + let join = WrappedIntervalsLattice.join + let top = WrappedIntervalsLattice.Top + let neg = WrappedIntervalsLatticeOps.neg + let init a = interval a a +end + +module SymAddrSetLattice = struct + include Lattice_collections.LatticeMap (SymBase) (IntervalDomain) +end + +module SVAAbstraction = struct + include SymAddrSetLattice + open WrappedIntervalsValueAbstractionBasil + + let eval_const (op : Lang.Ops.AllOps.const) rt = + SymAddrSetLattice.singleton SymBase.Constant @@ eval_const op rt + + let eval_unop (op : Lang.Ops.AllOps.unary) (a, t) rt = + SymAddrSetLattice.mapi + (fun sb1 vs1 -> + match sb1 with + | SymBase.GlobSym | Constant -> eval_unop op (vs1, t) rt + | _ -> Top) + a + + let eval_binop (op : E.binary) (a, ta) (b, tb) rt = + SymAddrSetLattice.fold + (fun sb1 vs1 map -> + SymAddrSetLattice.fold + (fun sb2 vs2 map -> + match (sb1, sb2) with + (* WARN: not 100% sure about this case but makes sense in head we would prefer one over the other? *) + | (SymBase.GlobSym | Constant), (SymBase.GlobSym | Constant) -> + let sb = + if SymBase.equal sb1 GlobSym || SymBase.equal sb2 GlobSym then + SymBase.GlobSym + else Constant + in + SymAddrSetLattice.singleton sb + (eval_binop op (vs1, ta) (vs2, tb) rt) + | (SymBase.GlobSym | Constant), sb | sb, (SymBase.GlobSym | Constant) + -> + SymAddrSetLattice.update sb + (eval_binop op (vs1, ta) (vs2, tb) rt) + map + | _, _ -> + SymAddrSetLattice.update sb1 Top + @@ SymAddrSetLattice.update sb2 Top map) + b map) + a SymAddrSetLattice.bottom + + let eval_intrin (op : E.intrin) args rt = + let op a b = + match op with + | (`BVADD | `BVOR | `BVXOR | `BVAND) as op -> (eval_binop op a b rt, rt) + | `OR | `AND | `Cases | `MapUpdate -> (SymAddrSetLattice.top, rt) + | `BVConcat -> + ( SymAddrSetLattice.fold + (fun sb1 vs1 acc -> + SymAddrSetLattice.fold + (fun sb2 vs2 map -> + let return_size = + match (snd a, snd b) with + | Types.Bitvector a, Types.Bitvector b -> + Types.Bitvector (a + b) + | _ -> failwith "boom" + in + match (sb1, sb2) with + (* NOTE: OCaml compiler complains when these cases are merged *) + | (SymBase.GlobSym | Constant), sb + when not @@ SymBase.is_place_holder sb -> + SymAddrSetLattice.update sb + (WrappedIntervalsValueAbstractionBasil.eval_intrin op + [ (vs1, snd a); (vs2, snd b) ] + return_size) + map + | sb, (SymBase.GlobSym | Constant) + when not @@ SymBase.is_place_holder sb -> + SymAddrSetLattice.update sb + (WrappedIntervalsValueAbstractionBasil.eval_intrin op + [ (vs1, snd a); (vs2, snd b) ] + return_size) + map + | _, _ -> + SymAddrSetLattice.update sb1 Top + @@ SymAddrSetLattice.update sb2 Top map) + (fst b) acc) + (fst a) SymAddrSetLattice.bottom, + rt ) + in + match args with + | h :: b :: tl -> fst @@ List.fold_left op (op h b) tl + | _ -> failwith "Operators must have two operands" +end + +module SVAAbstractionBasil = struct + include SVAAbstraction + module E = Lang.Expr.BasilExpr +end + +module StateAbstraction = Intra_analysis.MapState (SVAAbstractionBasil) +module Eval = Intra_analysis.EvalStmt (SVAAbstractionBasil) + +module Domain = struct + include StateAbstraction + + let stack_pointer = Var.create ~scope:Local "R31_in" @@ Bitvector 64 + let link_register = Var.create ~scope:Local "R30_in" @@ Bitvector 64 + let frame_pointer = Var.create ~scope:Local "R29_in" @@ Bitvector 64 + + let call_preserve = + List.init 11 (fun i -> 19 + i) |> fun lst -> + 31 :: lst |> List.map (fun i -> "R" ^ string_of_int i) + + let implicit_form = [ stack_pointer; link_register; frame_pointer ] + + let init proc = + let name = ID.name @@ Procedure.id proc in + StringMap.filter (fun param _ -> + List.fold_left + (fun acc a -> + if String.starts_with param ~prefix:a then acc else false) + false call_preserve) + @@ Procedure.formal_in_params proc + |> StringMap.to_iter + |> Iter.map (fun (_, param) -> + let size = + match Var.typ param with + | Types.Boolean -> 1 + | Types.Integer -> 32 + | Types.Bitvector size -> size + | _ -> failwith "Illegal function parameter type" + in + ( param, + SymAddrSetLattice.singleton (Par { name; param }) + @@ IntervalDomain.init @@ Bitvec.zero ~size )) + |> Iter.cons + ( stack_pointer, + SymAddrSetLattice.singleton (SymBase.Stack name) + @@ IntervalDomain.init @@ Bitvec.zero ~size:64 ) + |> Iter.cons + ( link_register, + SymAddrSetLattice.singleton + (SymBase.Par { name; param = link_register }) + @@ IntervalDomain.init @@ Bitvec.zero ~size:64 ) + |> Iter.cons + ( frame_pointer, + SymAddrSetLattice.singleton + (SymBase.Par { name; param = frame_pointer }) + @@ IntervalDomain.init @@ Bitvec.zero ~size:64 ) + |> Iter.fold (fun m (v, d) -> update v d m) bottom + + let transfer_state read stmt = + let stmt = Eval.stmt_eval_fwd read stmt in + let updates = + match stmt with + | Stmt.Instr_Assign assignments -> List.to_iter assignments + | Stmt.Instr_Load { lhs; addr; rhs } -> ( + Iter.singleton + @@ + match addr with + | Scalar -> (lhs, rhs) + | Addr { size } -> + ( lhs, + SymAddrSetLattice.singleton Loaded + @@ IntervalDomain.init @@ Bitvec.zero ~size )) + | Stmt.Instr_Store { lhs; addr; rhs } -> ( + match addr with + | Scalar -> Iter.singleton (lhs, rhs) + | Addr { size } -> Iter.empty) + | Stmt.Instr_Call { lhs; procid } + when (String.equal "@malloc" @@ ID.name procid) + || (String.equal "@calloc" @@ ID.name procid) -> + let malloc = + Iter.filter (fun var -> + String.starts_with ~prefix:"R0" @@ Var.name var) + @@ StringMap.values lhs + in + let var = Iter.head_exn malloc in + let size = + match Var.typ var with + | Types.Bitvector size -> size + | _ -> failwith "Illegal malloc/calloc return type" + in + + Iter.singleton + ( var, + SymAddrSetLattice.singleton + (SymBase.Heap { name = ID.name procid }) + @@ IntervalDomain.init @@ Bitvec.zero ~size ) + | Stmt.Instr_Call { lhs; args; procid } -> + Iter.map (fun param -> + let size = + match Var.typ param with + | Types.Boolean -> 1 + | Types.Integer -> 32 + | Types.Bitvector size -> size + | _ -> failwith "Illegal function parameter type" + in + ( param, + SymAddrSetLattice.singleton + (Ret { name = ID.name procid; param }) + @@ IntervalDomain.init @@ Bitvec.zero ~size )) + @@ StringMap.values lhs + | Stmt.Instr_Assert _ | Stmt.Instr_Assume _ -> Iter.empty + (* TODO: (From Scala code) "possibly map every live variable to top" *) + | Stmt.Instr_IndirectCall _ -> Iter.empty + | Stmt.Instr_IntrinCall _ -> Iter.empty + in + updates + + let transfer dom stmt = + Iter.fold (fun a (k, v) -> update k v a) dom + @@ transfer_state (flip read dom) stmt +end + +module DFGAnalysis = Dataflow_graph.AnalysisFwd (Domain) + +let sva (prog : Program.t) = + let constant_within_global_address (interval : WrappedIntervalsLattice.t) + (prog : Program.t) : bool = + let open Option in + match + let* symbols = + match StringMap.find_opt ".symbols" prog.attrib with + | Some symbols -> Some symbols + | _ -> None + in + let* globs = + match Attrib.find_opt ".globals" (Some symbols) with + | Some Attrib.(`List globals) -> Some globals + | _ -> None + in + List.fold_left + (fun acc (global : Program.e Attrib.t) -> + (* I would like a better early continue then an if *) + if + Option.is_some acc + && Bool.equal (Option.value ~default:false acc) true + then Some true + else + let* address = + match Attrib.find_opt ".address" (Some global) with + | Some Attrib.(`Bitvector bv) -> Some bv + | _ -> None + in + let* size = + match Attrib.find_opt ".size" (Some global) with + | Some Attrib.(`Bitvector bv) -> Some bv + | _ -> None + in + let end_address = Bitvec.add address size in + let interval2 = + WrappedIntervalsLattice.interval address end_address + in + Some (WrappedIntervalsLattice.leq interval2 interval)) + None globs + with + | None -> false + | Some a -> a + in + let results = + IDMap.fold + (fun _ v acc -> DFGAnalysis.flow_insensitive v :: acc) + prog.procs [] + in + StateAbstraction.mapi (fun _ domain -> + SymAddrSetLattice.to_list domain + |> snd + |> List.map (fun (sym_base, value) -> + if + SymBase.equal Constant sym_base + && constant_within_global_address value prog + then (SymBase.GlobSym, value) + else (sym_base, value)) + |> SymAddrSetLattice.of_list_bot) + @@ List.hd results diff --git a/lib/passes.ml b/lib/passes.ml index db7aa06f..f75524b0 100644 --- a/lib/passes.ml +++ b/lib/passes.ml @@ -121,6 +121,18 @@ module PassManager = struct control flow graph and prints results"; } + let sva = + { + name = "sva"; + apply = + Prog + (fun p -> + let r = Analysis.Sva.sva p in + print_endline @@ Analysis.Sva.StateAbstraction.show r; + p); + doc = "Runs symbolic value analysis and prints stuff out after"; + } + let demo_dfg_gamma = { name = "demo-dfg-gamma-analysis"; @@ -237,6 +249,7 @@ module PassManager = struct read_uninit false; read_uninit true; sssa; + sva; full_ssa; type_check; split_memory_encoding; diff --git a/test/lang/test_value_soundness.ml b/test/lang/test_value_soundness.ml index 88d7e0aa..67064ca3 100644 --- a/test/lang/test_value_soundness.ml +++ b/test/lang/test_value_soundness.ml @@ -108,6 +108,8 @@ module TestTnumWintReducedDom = (Analysis.Tnum_wint_reduced_product .TnumWintReducedProductValueAbstractionBasil) +module TestSVADom = ValueAbstractionSoundness (Analysis.Sva.SVAAbstractionBasil) + let _ = Alcotest.run "value domain abstract eval soundness" [ From 69b90a961f6338dad649223dbd9e801035a382ec Mon Sep 17 00:00:00 2001 From: bpaul Date: Thu, 9 Apr 2026 14:33:07 +1000 Subject: [PATCH 2/8] flip test order because of hashing nonsense --- lib/transforms/may_read_uninit.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/lib/transforms/may_read_uninit.ml b/lib/transforms/may_read_uninit.ml index 4edb270d..62534cfc 100644 --- a/lib/transforms/may_read_uninit.ml +++ b/lib/transforms/may_read_uninit.ml @@ -148,10 +148,10 @@ let%expect_test "fold_block" = in [%expect {| - ($stack->RU, R31_in->RU, R0_in->RU, _->⊥) - ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, _->⊥) - ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, _->⊥) - ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, _->⊥) - ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, load46_1->W, _->⊥) - ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, load46_1->W, R0_10->W, _->⊥) + (R31_in->RU, $stack->RU, R0_in->RU, _->⊥) + (R31_in->RU, $stack->RU, R0_in->RU, load45_1->W, _->⊥) + (R31_in->RU, $stack->RU, R0_in->RU, load45_1->W, R1_4->W, _->⊥) + (R31_in->RU, $stack->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, _->⊥) + (R31_in->RU, $stack->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, load46_1->W, _->⊥) + (R31_in->RU, $stack->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, load46_1->W, R0_10->W, _->⊥) |}] From 36648b8ecc84ba8f13cdcdeec2c433b2e59771e3 Mon Sep 17 00:00:00 2001 From: bpaul Date: Thu, 9 Apr 2026 16:20:19 +1000 Subject: [PATCH 3/8] funny option monad --- lib/analysis/sva.ml | 71 ++++++++++++++++++++------------------------- lib/passes.ml | 10 +++---- 2 files changed, 37 insertions(+), 44 deletions(-) diff --git a/lib/analysis/sva.ml b/lib/analysis/sva.ml index 16fcec2f..332102d3 100644 --- a/lib/analysis/sva.ml +++ b/lib/analysis/sva.ml @@ -282,50 +282,44 @@ let sva (prog : Program.t) = let constant_within_global_address (interval : WrappedIntervalsLattice.t) (prog : Program.t) : bool = let open Option in - match - let* symbols = - match StringMap.find_opt ".symbols" prog.attrib with - | Some symbols -> Some symbols - | _ -> None - in - let* globs = - match Attrib.find_opt ".globals" (Some symbols) with - | Some Attrib.(`List globals) -> Some globals - | _ -> None - in - List.fold_left - (fun acc (global : Program.e Attrib.t) -> - (* I would like a better early continue then an if *) - if - Option.is_some acc - && Bool.equal (Option.value ~default:false acc) true - then Some true - else - let* address = - match Attrib.find_opt ".address" (Some global) with - | Some Attrib.(`Bitvector bv) -> Some bv - | _ -> None - in - let* size = - match Attrib.find_opt ".size" (Some global) with - | Some Attrib.(`Bitvector bv) -> Some bv - | _ -> None - in - let end_address = Bitvec.add address size in - let interval2 = - WrappedIntervalsLattice.interval address end_address - in - Some (WrappedIntervalsLattice.leq interval2 interval)) - None globs - with - | None -> false - | Some a -> a + (let* symbols = + match StringMap.find_opt ".symbols" prog.attrib with + | Some symbols -> Some symbols + | _ -> None + in + let* globs = + match Attrib.find_opt ".globals" (Some symbols) with + | Some Attrib.(`List globals) -> Some globals + | _ -> None + in + Some + (List.exists + (fun (global : Program.e Attrib.t) -> + (let* address = + match Attrib.find_opt ".address" (Some global) with + | Some Attrib.(`Bitvector bv) -> Some bv + | _ -> None + in + let* size = + match Attrib.find_opt ".size" (Some global) with + | Some Attrib.(`Bitvector bv) -> Some bv + | _ -> None + in + let end_address = Bitvec.add address size in + let interval2 = + WrappedIntervalsLattice.interval address end_address + in + Some (WrappedIntervalsLattice.leq interval2 interval)) + |> Option.get_or ~default:false) + globs)) + |> Option.get_or ~default:false in let results = IDMap.fold (fun _ v acc -> DFGAnalysis.flow_insensitive v :: acc) prog.procs [] in + results |> List.map @@ StateAbstraction.mapi (fun _ domain -> SymAddrSetLattice.to_list domain |> snd @@ -336,4 +330,3 @@ let sva (prog : Program.t) = then (SymBase.GlobSym, value) else (sym_base, value)) |> SymAddrSetLattice.of_list_bot) - @@ List.hd results diff --git a/lib/passes.ml b/lib/passes.ml index f75524b0..97a7075a 100644 --- a/lib/passes.ml +++ b/lib/passes.ml @@ -128,7 +128,7 @@ module PassManager = struct Prog (fun p -> let r = Analysis.Sva.sva p in - print_endline @@ Analysis.Sva.StateAbstraction.show r; + List.iter (print_endline % Analysis.Sva.StateAbstraction.show) r; p); doc = "Runs symbolic value analysis and prints stuff out after"; } @@ -208,7 +208,7 @@ module PassManager = struct apply = Prog Transforms.Memory_specification.transform; doc = "Specifies programs for memory safety"; } - + let intra_function_summaries = { name = "intra-function-summaries"; @@ -296,9 +296,9 @@ module PassManager = struct doc = "Replaces captured global variables with explicit parameters"; }; { - name = "gamma-vars"; - apply = Prog Transforms.Gamma_vars.transform; - doc = "Replace gamma expressions with gamma variables"; + name = "gamma-vars"; + apply = Prog Transforms.Gamma_vars.transform; + doc = "Replace gamma expressions with gamma variables"; }; { name = "linear-const"; From ae7eb546c0c7548e5f0c13a6191be35bf2885b1c Mon Sep 17 00:00:00 2001 From: JTrenerry <105094182+JTrenerry@users.noreply.github.com> Date: Thu, 9 Apr 2026 16:32:47 +1000 Subject: [PATCH 4/8] fixes changes --- lib/analysis/sva.ml | 21 ++++----------------- 1 file changed, 4 insertions(+), 17 deletions(-) diff --git a/lib/analysis/sva.ml b/lib/analysis/sva.ml index 332102d3..de5ace4b 100644 --- a/lib/analysis/sva.ml +++ b/lib/analysis/sva.ml @@ -45,7 +45,7 @@ module SymBase = struct | Ret _ | Par _ | Loaded -> true let to_int = Hashtbl.hash - let pretty a = Containers_pp.int 1 + let pretty a = Containers_pp.text @@ show a let is_stack = function Stack _ -> true | _ -> false end @@ -130,14 +130,7 @@ module SVAAbstraction = struct match (sb1, sb2) with (* NOTE: OCaml compiler complains when these cases are merged *) | (SymBase.GlobSym | Constant), sb - when not @@ SymBase.is_place_holder sb -> - SymAddrSetLattice.update sb - (WrappedIntervalsValueAbstractionBasil.eval_intrin op - [ (vs1, snd a); (vs2, snd b) ] - return_size) - map - | sb, (SymBase.GlobSym | Constant) - when not @@ SymBase.is_place_holder sb -> + | sb, (SymBase.GlobSym | Constant) -> SymAddrSetLattice.update sb (WrappedIntervalsValueAbstractionBasil.eval_intrin op [ (vs1, snd a); (vs2, snd b) ] @@ -170,26 +163,21 @@ module Domain = struct let link_register = Var.create ~scope:Local "R30_in" @@ Bitvector 64 let frame_pointer = Var.create ~scope:Local "R29_in" @@ Bitvector 64 + (* These registers are preserved over calls and are not real params, so we can ignore later *) let call_preserve = List.init 11 (fun i -> 19 + i) |> fun lst -> 31 :: lst |> List.map (fun i -> "R" ^ string_of_int i) - let implicit_form = [ stack_pointer; link_register; frame_pointer ] - let init proc = let name = ID.name @@ Procedure.id proc in StringMap.filter (fun param _ -> - List.fold_left - (fun acc a -> - if String.starts_with param ~prefix:a then acc else false) - false call_preserve) + List.exists (fun a -> String.starts_with param ~prefix:a) call_preserve) @@ Procedure.formal_in_params proc |> StringMap.to_iter |> Iter.map (fun (_, param) -> let size = match Var.typ param with | Types.Boolean -> 1 - | Types.Integer -> 32 | Types.Bitvector size -> size | _ -> failwith "Illegal function parameter type" in @@ -255,7 +243,6 @@ module Domain = struct let size = match Var.typ param with | Types.Boolean -> 1 - | Types.Integer -> 32 | Types.Bitvector size -> size | _ -> failwith "Illegal function parameter type" in From 87b9482a5015acca93967fad8f9e5806299f244e Mon Sep 17 00:00:00 2001 From: bpaul Date: Thu, 9 Apr 2026 16:38:50 +1000 Subject: [PATCH 5/8] Don't throw on invalid params --- lib/analysis/sva.ml | 41 ++++++++++++++++++++++------------------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/lib/analysis/sva.ml b/lib/analysis/sva.ml index de5ace4b..889e7fe5 100644 --- a/lib/analysis/sva.ml +++ b/lib/analysis/sva.ml @@ -169,21 +169,23 @@ module Domain = struct 31 :: lst |> List.map (fun i -> "R" ^ string_of_int i) let init proc = + let open Option in let name = ID.name @@ Procedure.id proc in StringMap.filter (fun param _ -> List.exists (fun a -> String.starts_with param ~prefix:a) call_preserve) @@ Procedure.formal_in_params proc |> StringMap.to_iter - |> Iter.map (fun (_, param) -> - let size = + |> Iter.filter_map (fun (_, param) -> + let* size = match Var.typ param with - | Types.Boolean -> 1 - | Types.Bitvector size -> size - | _ -> failwith "Illegal function parameter type" + | Types.Boolean -> Some 1 + | Types.Bitvector size -> Some size + | _ -> None in - ( param, - SymAddrSetLattice.singleton (Par { name; param }) - @@ IntervalDomain.init @@ Bitvec.zero ~size )) + Some + ( param, + SymAddrSetLattice.singleton (Par { name; param }) + @@ IntervalDomain.init @@ Bitvec.zero ~size )) |> Iter.cons ( stack_pointer, SymAddrSetLattice.singleton (SymBase.Stack name) @@ -306,14 +308,15 @@ let sva (prog : Program.t) = (fun _ v acc -> DFGAnalysis.flow_insensitive v :: acc) prog.procs [] in - results |> List.map @@ - StateAbstraction.mapi (fun _ domain -> - SymAddrSetLattice.to_list domain - |> snd - |> List.map (fun (sym_base, value) -> - if - SymBase.equal Constant sym_base - && constant_within_global_address value prog - then (SymBase.GlobSym, value) - else (sym_base, value)) - |> SymAddrSetLattice.of_list_bot) + results + |> List.map + @@ StateAbstraction.mapi (fun _ domain -> + SymAddrSetLattice.to_list domain + |> snd + |> List.map (fun (sym_base, value) -> + if + SymBase.equal Constant sym_base + && constant_within_global_address value prog + then (SymBase.GlobSym, value) + else (sym_base, value)) + |> SymAddrSetLattice.of_list_bot) From d3286146bc762a6c130170a3e970e11ede3ce53d Mon Sep 17 00:00:00 2001 From: JTrenerry <105094182+JTrenerry@users.noreply.github.com> Date: Mon, 13 Apr 2026 09:21:36 +1000 Subject: [PATCH 6/8] Bitvec.one needs size, since it is an address it should be 64 --- lib/analysis/sva.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/lib/analysis/sva.ml b/lib/analysis/sva.ml index 889e7fe5..5ee756d1 100644 --- a/lib/analysis/sva.ml +++ b/lib/analysis/sva.ml @@ -294,7 +294,9 @@ let sva (prog : Program.t) = | Some Attrib.(`Bitvector bv) -> Some bv | _ -> None in - let end_address = Bitvec.add address size in + let end_address = + Bitvec.sub (Bitvec.one ~size:64) @@ Bitvec.add address size + in let interval2 = WrappedIntervalsLattice.interval address end_address in From 2021c6478c3bda19ab748d592fe78fb048fe9c10 Mon Sep 17 00:00:00 2001 From: JTrenerry <105094182+JTrenerry@users.noreply.github.com> Date: Tue, 14 Apr 2026 14:32:50 +1000 Subject: [PATCH 7/8] fix sva --- lib/analysis/sva.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/lib/analysis/sva.ml b/lib/analysis/sva.ml index 5ee756d1..590a90d1 100644 --- a/lib/analysis/sva.ml +++ b/lib/analysis/sva.ml @@ -85,7 +85,7 @@ module SVAAbstraction = struct | _ -> Top) a - let eval_binop (op : E.binary) (a, ta) (b, tb) rt = + let eval_binary op (a, ta) (b, tb) rt = SymAddrSetLattice.fold (fun sb1 vs1 map -> SymAddrSetLattice.fold @@ -99,11 +99,11 @@ module SVAAbstraction = struct else Constant in SymAddrSetLattice.singleton sb - (eval_binop op (vs1, ta) (vs2, tb) rt) + (eval_binary op (vs1, ta) (vs2, tb) rt) | (SymBase.GlobSym | Constant), sb | sb, (SymBase.GlobSym | Constant) -> SymAddrSetLattice.update sb - (eval_binop op (vs1, ta) (vs2, tb) rt) + (eval_binary op (vs1, ta) (vs2, tb) rt) map | _, _ -> SymAddrSetLattice.update sb1 Top @@ -111,10 +111,14 @@ module SVAAbstraction = struct b map) a SymAddrSetLattice.bottom + let eval_binop op a b rt = + match op with #Lang.Ops.AllOps.binary as op -> eval_binary op a b rt + let eval_intrin (op : E.intrin) args rt = let op a b = match op with - | (`BVADD | `BVOR | `BVXOR | `BVAND) as op -> (eval_binop op a b rt, rt) + | (`BVADD | `BVOR | `BVXOR | `BVAND | `BVMUL) as op -> + (eval_binary op a b rt, rt) | `OR | `AND | `Cases | `MapUpdate -> (SymAddrSetLattice.top, rt) | `BVConcat -> ( SymAddrSetLattice.fold From 4b9be31dc9cf2cbb1a87f50d771728410d7f81c6 Mon Sep 17 00:00:00 2001 From: JTrenerry <105094182+JTrenerry@users.noreply.github.com> Date: Tue, 14 Apr 2026 15:10:44 +1000 Subject: [PATCH 8/8] THE BEST TEST OF ALL TIME --- test/cram/dune | 1 + test/cram/malloc_free.t | 148 ++++++++++++++++++++-------------------- test/cram/sva.sexp | 2 + test/cram/sva.t | 3 + 4 files changed, 80 insertions(+), 74 deletions(-) create mode 100644 test/cram/sva.sexp create mode 100644 test/cram/sva.t diff --git a/test/cram/dune b/test/cram/dune index 001f4e7e..566b52eb 100644 --- a/test/cram/dune +++ b/test/cram/dune @@ -26,6 +26,7 @@ inter_dead.il typefail.sexp typepass.sexp + sva.sexp basicssa.sexp roundtrip.sexp gammavars.sexp diff --git a/test/cram/malloc_free.t b/test/cram/malloc_free.t index 02022580..6ad7fdb4 100644 --- a/test/cram/malloc_free.t +++ b/test/cram/malloc_free.t @@ -13,10 +13,10 @@ var $mem_encoding: MemEncoding; function f$magic(a: [bv64]bv8, b: [bv64]bv8) returns ([bv64]bv8) { a } - function {:bvbuiltin "bvadd"} {:extern } bvadd_bv64(bv64, bv64) returns (bv64); - function {:bvbuiltin "bvand"} {:extern } bvand_bv64(bv64, bv64) returns (bv64); - function {:bvbuiltin "bvule"} {:extern } bvule_bv64_bv64_bool(bv64, bv64) returns (bool); - function {:bvbuiltin "bvult"} {:extern } bvult_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:extern } {:bvbuiltin "bvadd"} bvadd_bv64(bv64, bv64) returns (bv64); + function {:extern } {:bvbuiltin "bvand"} bvand_bv64(bv64, bv64) returns (bv64); + function {:extern } {:bvbuiltin "bvule"} bvule_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:extern } {:bvbuiltin "bvult"} bvult_bv64_bv64_bool(bv64, bv64) returns (bool); function {:extern } load64_le(#memory: [bv64]bv8, #index: bv64) returns (bv64) { (((((((#memory[bvadd_bv64(#index, 7bv64)] ++ @@ -34,38 +34,38 @@ ++ #memory[bvadd_bv64(#index, 0bv64)]): bv64 } - function {:extern } {:inline } me_addr_alloc(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { + function {:inline } {:extern } me_addr_alloc(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { addr } - function {:extern } {:inline } me_addr_is_heap(mem_encoding: MemEncoding, addr: bv64) returns (bool) { + function {:inline } {:extern } me_addr_is_heap(mem_encoding: MemEncoding, addr: bv64) returns (bool) { mem_encoding->addr_is_heap[addr] } - function {:extern } {:inline } me_addr_offset(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { + function {:inline } {:extern } me_addr_offset(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { bvand_bv64(addr, 4294967295bv64) } - function {:extern } {:inline } me_alloc_base(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { + function {:inline } {:extern } me_alloc_base(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { bvand_bv64(alloc, 18446744069414584320bv64) } - function {:extern } {:inline } me_alloc_live(mem_encoding: MemEncoding, alloc: bv64) returns (bv2) { + function {:inline } {:extern } me_alloc_live(mem_encoding: MemEncoding, alloc: bv64) returns (bv2) { mem_encoding->alloc_live[alloc] } - function {:extern } {:inline } me_alloc_live_update(mem_encoding: MemEncoding, alloc: bv64, live: bv2) returns (MemEncoding) { + function {:inline } {:extern } me_alloc_live_update(mem_encoding: MemEncoding, alloc: bv64, live: bv2) returns (MemEncoding) { mem_encoding->(alloc_live := mem_encoding->alloc_live[alloc := live]) } - function {:extern } {:inline } me_alloc_size(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { + function {:inline } {:extern } me_alloc_size(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { mem_encoding->alloc_size[alloc] } - function {:extern } {:inline } me_alloc_size_update(mem_encoding: MemEncoding, alloc: bv64, size: bv64) returns (MemEncoding) { + function {:inline } {:extern } me_alloc_size_update(mem_encoding: MemEncoding, alloc: bv64, size: bv64) returns (MemEncoding) { mem_encoding->(alloc_size := mem_encoding->alloc_size[alloc := size]) } - function {:extern } {:inline } me_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (MemEncoding) { + function {:inline } {:extern } me_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (MemEncoding) { me_alloc_size_update( me_alloc_live_update(mem_encoding, me_addr_alloc(mem_encoding, addr), 1bv2), me_addr_alloc(mem_encoding, addr), size ) } - function {:extern } {:inline } me_can_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { + function {:inline } {:extern } me_can_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { ((((me_addr_is_heap(mem_encoding, addr)&&(me_alloc_base(mem_encoding, addr) == addr))&&(me_alloc_live( mem_encoding, me_addr_alloc(mem_encoding, addr) @@ -74,7 +74,7 @@ size )) } - function {:extern } {:inline } me_init_encoding(mem_encoding: MemEncoding) returns (bool) { + function {:inline } {:extern } me_init_encoding(mem_encoding: MemEncoding) returns (bool) { (((forall i: bv64 :: {me_addr_is_heap(mem_encoding, i)} @@ -86,7 +86,7 @@ {me_alloc_live(mem_encoding, i)} ((!(me_addr_is_heap(mem_encoding, i))) ==> (me_alloc_live(mem_encoding, i) == 2bv2)))) } - function {:extern } {:inline } me_valid_access(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { + function {:inline } {:extern } me_valid_access(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { (me_addr_is_heap(mem_encoding, addr) ==> ((me_alloc_live( mem_encoding, me_alloc_base(mem_encoding, me_addr_alloc(mem_encoding, addr)) @@ -99,7 +99,7 @@ ))) } datatype MemEncoding {MemEncoding(alloc_live: [bv64]bv2, alloc_size: [bv64]bv64, addr_is_heap: [bv64]bool)} - function {:define } {:extern } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) { + function {:extern } {:define } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) { #memory[#index := #value[8:0]][bvadd_bv64(#index, 1bv64) := #value[16:8]][bvadd_bv64( #index, 2bv64 @@ -111,10 +111,28 @@ 6bv64 ) := #value[56:48]][bvadd_bv64(#index, 7bv64) := #value[64:56]] } - function {:define } {:extern } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) { + function {:extern } {:define } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) { #memory[#index := #value[8:0]] } + procedure p$free(); + modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; + ensures ($mem_encoding == me_alloc_live_update( + old($mem_encoding), + me_addr_alloc(old($mem_encoding), $R0), + 2bv2 + )); + requires me_addr_is_heap($mem_encoding, $R0); + requires (0bv64 == me_addr_offset($mem_encoding, $R0)); + requires (me_alloc_live($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == 1bv2); + + procedure p$malloc(); + modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; + ensures me_can_allocate(old($mem_encoding), $R0, old($R0)); + ensures (me_addr_offset($mem_encoding, $R0) == 0bv64); + ensures (me_alloc_base($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == $R0); + ensures ($mem_encoding == me_allocate(old($mem_encoding), $R0, old($R0))); + procedure p$main(); modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; requires me_init_encoding($mem_encoding); @@ -190,24 +208,6 @@ assert true; return; } - - procedure p$malloc(); - modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; - ensures me_can_allocate(old($mem_encoding), $R0, old($R0)); - ensures (me_addr_offset($mem_encoding, $R0) == 0bv64); - ensures (me_alloc_base($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == $R0); - ensures ($mem_encoding == me_allocate(old($mem_encoding), $R0, old($R0))); - - procedure p$free(); - modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; - ensures ($mem_encoding == me_alloc_live_update( - old($mem_encoding), - me_addr_alloc(old($mem_encoding), $R0), - 2bv2 - )); - requires me_addr_is_heap($mem_encoding, $R0); - requires (0bv64 == me_addr_offset($mem_encoding, $R0)); - requires (me_alloc_live($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == 1bv2); $ boogie ./good.bpl @@ -226,10 +226,10 @@ var $mem_encoding: MemEncoding; function f$magic(a: [bv64]bv8, b: [bv64]bv8) returns ([bv64]bv8) { a } - function {:bvbuiltin "bvadd"} {:extern } bvadd_bv64(bv64, bv64) returns (bv64); - function {:bvbuiltin "bvand"} {:extern } bvand_bv64(bv64, bv64) returns (bv64); - function {:bvbuiltin "bvule"} {:extern } bvule_bv64_bv64_bool(bv64, bv64) returns (bool); - function {:bvbuiltin "bvult"} {:extern } bvult_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:extern } {:bvbuiltin "bvadd"} bvadd_bv64(bv64, bv64) returns (bv64); + function {:extern } {:bvbuiltin "bvand"} bvand_bv64(bv64, bv64) returns (bv64); + function {:extern } {:bvbuiltin "bvule"} bvule_bv64_bv64_bool(bv64, bv64) returns (bool); + function {:extern } {:bvbuiltin "bvult"} bvult_bv64_bv64_bool(bv64, bv64) returns (bool); function {:extern } load64_le(#memory: [bv64]bv8, #index: bv64) returns (bv64) { (((((((#memory[bvadd_bv64(#index, 7bv64)] ++ @@ -247,38 +247,38 @@ ++ #memory[bvadd_bv64(#index, 0bv64)]): bv64 } - function {:extern } {:inline } me_addr_alloc(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { + function {:inline } {:extern } me_addr_alloc(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { addr } - function {:extern } {:inline } me_addr_is_heap(mem_encoding: MemEncoding, addr: bv64) returns (bool) { + function {:inline } {:extern } me_addr_is_heap(mem_encoding: MemEncoding, addr: bv64) returns (bool) { mem_encoding->addr_is_heap[addr] } - function {:extern } {:inline } me_addr_offset(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { + function {:inline } {:extern } me_addr_offset(mem_encoding: MemEncoding, addr: bv64) returns (bv64) { bvand_bv64(addr, 4294967295bv64) } - function {:extern } {:inline } me_alloc_base(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { + function {:inline } {:extern } me_alloc_base(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { bvand_bv64(alloc, 18446744069414584320bv64) } - function {:extern } {:inline } me_alloc_live(mem_encoding: MemEncoding, alloc: bv64) returns (bv2) { + function {:inline } {:extern } me_alloc_live(mem_encoding: MemEncoding, alloc: bv64) returns (bv2) { mem_encoding->alloc_live[alloc] } - function {:extern } {:inline } me_alloc_live_update(mem_encoding: MemEncoding, alloc: bv64, live: bv2) returns (MemEncoding) { + function {:inline } {:extern } me_alloc_live_update(mem_encoding: MemEncoding, alloc: bv64, live: bv2) returns (MemEncoding) { mem_encoding->(alloc_live := mem_encoding->alloc_live[alloc := live]) } - function {:extern } {:inline } me_alloc_size(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { + function {:inline } {:extern } me_alloc_size(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) { mem_encoding->alloc_size[alloc] } - function {:extern } {:inline } me_alloc_size_update(mem_encoding: MemEncoding, alloc: bv64, size: bv64) returns (MemEncoding) { + function {:inline } {:extern } me_alloc_size_update(mem_encoding: MemEncoding, alloc: bv64, size: bv64) returns (MemEncoding) { mem_encoding->(alloc_size := mem_encoding->alloc_size[alloc := size]) } - function {:extern } {:inline } me_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (MemEncoding) { + function {:inline } {:extern } me_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (MemEncoding) { me_alloc_size_update( me_alloc_live_update(mem_encoding, me_addr_alloc(mem_encoding, addr), 1bv2), me_addr_alloc(mem_encoding, addr), size ) } - function {:extern } {:inline } me_can_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { + function {:inline } {:extern } me_can_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { ((((me_addr_is_heap(mem_encoding, addr)&&(me_alloc_base(mem_encoding, addr) == addr))&&(me_alloc_live( mem_encoding, me_addr_alloc(mem_encoding, addr) @@ -287,7 +287,7 @@ size )) } - function {:extern } {:inline } me_init_encoding(mem_encoding: MemEncoding) returns (bool) { + function {:inline } {:extern } me_init_encoding(mem_encoding: MemEncoding) returns (bool) { (((forall i: bv64 :: {me_addr_is_heap(mem_encoding, i)} @@ -299,7 +299,7 @@ {me_alloc_live(mem_encoding, i)} ((!(me_addr_is_heap(mem_encoding, i))) ==> (me_alloc_live(mem_encoding, i) == 2bv2)))) } - function {:extern } {:inline } me_valid_access(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { + function {:inline } {:extern } me_valid_access(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) { (me_addr_is_heap(mem_encoding, addr) ==> ((me_alloc_live( mem_encoding, me_alloc_base(mem_encoding, me_addr_alloc(mem_encoding, addr)) @@ -312,7 +312,7 @@ ))) } datatype MemEncoding {MemEncoding(alloc_live: [bv64]bv2, alloc_size: [bv64]bv64, addr_is_heap: [bv64]bool)} - function {:define } {:extern } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) { + function {:extern } {:define } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) { #memory[#index := #value[8:0]][bvadd_bv64(#index, 1bv64) := #value[16:8]][bvadd_bv64( #index, 2bv64 @@ -324,10 +324,28 @@ 6bv64 ) := #value[56:48]][bvadd_bv64(#index, 7bv64) := #value[64:56]] } - function {:define } {:extern } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) { + function {:extern } {:define } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) { #memory[#index := #value[8:0]] } + procedure p$free(); + modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; + ensures ($mem_encoding == me_alloc_live_update( + old($mem_encoding), + me_addr_alloc(old($mem_encoding), $R0), + 2bv2 + )); + requires me_addr_is_heap($mem_encoding, $R0); + requires (0bv64 == me_addr_offset($mem_encoding, $R0)); + requires (me_alloc_live($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == 1bv2); + + procedure p$malloc(); + modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; + ensures me_can_allocate(old($mem_encoding), $R0, old($R0)); + ensures (me_addr_offset($mem_encoding, $R0) == 0bv64); + ensures (me_alloc_base($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == $R0); + ensures ($mem_encoding == me_allocate(old($mem_encoding), $R0, old($R0))); + procedure p$main(); modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; requires me_init_encoding($mem_encoding); @@ -403,28 +421,10 @@ assert true; return; } - - procedure p$malloc(); - modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; - ensures me_can_allocate(old($mem_encoding), $R0, old($R0)); - ensures (me_addr_offset($mem_encoding, $R0) == 0bv64); - ensures (me_alloc_base($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == $R0); - ensures ($mem_encoding == me_allocate(old($mem_encoding), $R0, old($R0))); - - procedure p$free(); - modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31; - ensures ($mem_encoding == me_alloc_live_update( - old($mem_encoding), - me_addr_alloc(old($mem_encoding), $R0), - 2bv2 - )); - requires me_addr_is_heap($mem_encoding, $R0); - requires (0bv64 == me_addr_offset($mem_encoding, $R0)); - requires (me_alloc_live($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == 1bv2); $ boogie ./bad.bpl - ./bad.bpl(158,5): Error: this assertion could not be proved + ./bad.bpl(176,5): Error: this assertion could not be proved Execution trace: - ./bad.bpl(128,3): b#main_entry + ./bad.bpl(146,3): b#main_entry Boogie program verifier finished with 0 verified, 1 error diff --git a/test/cram/sva.sexp b/test/cram/sva.sexp new file mode 100644 index 00000000..5c749b79 --- /dev/null +++ b/test/cram/sva.sexp @@ -0,0 +1,2 @@ +(load-il "../../examples/irreducible_loop_1.il") +(run-transforms "sva") diff --git a/test/cram/sva.t b/test/cram/sva.t new file mode 100644 index 00000000..df3cea14 --- /dev/null +++ b/test/cram/sva.t @@ -0,0 +1,3 @@ + $ bincaml script ./sva.sexp + (R31_in->(Stack(@puts_1584)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@puts_1584_{id=1 ; data=R30_in:bv64})->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@puts_1584_{id=2 ; data=R29_in:bv64})->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), _->⊥) + (R31_in->(Stack(@main_1876)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@main_1876_{id=1 ; data=R30_in:bv64})->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@main_1876_{id=2 ; data=R29_in:bv64})->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), $CF->(Loaded->⊤, _->⊥), $NF->(Loaded->⊤, _->⊥), $R0->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), $R1->(Loaded->⊤, _->⊥), $R29->(Loaded->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), $R30->(Loaded->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), $VF->(Loaded->⊤, _->⊥), $ZF->(Loaded->⊤, _->⊥), load18->(Loaded->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), #5->(Loaded->⊤, _->⊥), load19->(Loaded->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), load21->(Loaded->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load22->(Loaded->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load20->(Loaded->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), #6->(Loaded->⊤, _->⊥), _->⊥)