From 843dcf7f776ddc6f28ac3368aa26af87ed52d11a Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Tue, 30 Sep 2025 22:25:49 +0100 Subject: [PATCH 01/29] cleanup tiny thing in bi_state Signed-off-by: Sacha Ayoun --- GillianCore/engine/BiAbduction/BiState.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/GillianCore/engine/BiAbduction/BiState.ml b/GillianCore/engine/BiAbduction/BiState.ml index d6d3b24f7..61ee5f6b5 100644 --- a/GillianCore/engine/BiAbduction/BiState.ml +++ b/GillianCore/engine/BiAbduction/BiState.ml @@ -103,13 +103,11 @@ module Make (State : SState.S) = struct { procs; state = State.copy state; af_state = State.copy af_state } let simplify - ?(save = false) - ?(kill_new_lvars : bool option) + ?save + ?kill_new_lvars ?matching:_ ({ procs; state; af_state } : t) : SVal.SESubst.t * t list = - let kill_new_lvars = Option.value ~default:true kill_new_lvars in - let subst, states = State.simplify ~save ~kill_new_lvars state in - + let subst, states = State.simplify ?save ?kill_new_lvars state in let states = List.concat_map (fun state -> From 4817343a4a9279c06f92b3643f53cacb367f59a2 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Tue, 30 Sep 2025 22:26:19 +0100 Subject: [PATCH 02/29] yojson for core predicates Signed-off-by: Sacha Ayoun --- transformers/lib/prebuilt/c_states/BlockTree.ml | 2 +- transformers/lib/states/Freeable.ml | 2 +- transformers/lib/states/MList.ml | 2 +- transformers/lib/states/MyMonadicSMemory.ml | 2 +- transformers/lib/states/PMap.ml | 4 ++-- transformers/lib/states/Product.ml | 2 +- transformers/lib/states/Sum.ml | 2 +- 7 files changed, 8 insertions(+), 8 deletions(-) diff --git a/transformers/lib/prebuilt/c_states/BlockTree.ml b/transformers/lib/prebuilt/c_states/BlockTree.ml index 531dbc915..747d06d9e 100644 --- a/transformers/lib/prebuilt/c_states/BlockTree.ml +++ b/transformers/lib/prebuilt/c_states/BlockTree.ml @@ -1145,7 +1145,7 @@ module M = struct [@@deriving show, yojson] type action = ac - type pred = ga + type pred = ga [@@deriving yojson] let action_to_str = str_ac let action_from_str s = try Some (ac_from_str s) with _ -> None diff --git a/transformers/lib/states/Freeable.ml b/transformers/lib/states/Freeable.ml index f6027b427..3ba0964f8 100644 --- a/transformers/lib/states/Freeable.ml +++ b/transformers/lib/states/Freeable.ml @@ -38,7 +38,7 @@ module Make (S : MyMonadicSMemory.S) : (fun (a, arg, ret) -> (SubAction a, arg, ret)) (S.list_actions ()) - type pred = FreedPred | SubPred of S.pred + type pred = FreedPred | SubPred of S.pred [@@deriving yojson] let pred_from_str = function | "freed" -> Some FreedPred diff --git a/transformers/lib/states/MList.ml b/transformers/lib/states/MList.ml index d585ec235..67d5bf75c 100644 --- a/transformers/lib/states/MList.ml +++ b/transformers/lib/states/MList.ml @@ -37,7 +37,7 @@ module Make (S : MyMonadicSMemory.S) : (fun (a, args, ret) -> (SubAction a, "offset" :: args, ret)) (S.list_actions ()) - type pred = Length | SubPred of S.pred + type pred = Length | SubPred of S.pred [@@deriving yojson] let pred_from_str = function | "length" -> Some Length diff --git a/transformers/lib/states/MyMonadicSMemory.ml b/transformers/lib/states/MyMonadicSMemory.ml index a4e48b0fb..93cd08adc 100644 --- a/transformers/lib/states/MyMonadicSMemory.ml +++ b/transformers/lib/states/MyMonadicSMemory.ml @@ -14,7 +14,7 @@ module type S = sig (* Type of predicates and actions *) type action - type pred + type pred [@@deriving yojson] val action_from_str : string -> action option val action_to_str : action -> string diff --git a/transformers/lib/states/PMap.ml b/transformers/lib/states/PMap.ml index 4a450a46e..ebe5d2277 100644 --- a/transformers/lib/states/PMap.ml +++ b/transformers/lib/states/PMap.ml @@ -156,7 +156,7 @@ struct (fun (a, args, ret) -> (SubAction a, "index" :: args, ret)) (S.list_actions ()) - type pred = DomainSet | SubPred of S.pred + type pred = DomainSet | SubPred of S.pred [@@deriving yojson] let pred_from_str = function | "domainset" -> Some DomainSet @@ -444,7 +444,7 @@ struct (fun (a, args, ret) -> (SubAction a, "index" :: args, ret)) (S.list_actions ()) - type pred = S.pred + type pred = S.pred [@@deriving yojson] let pred_from_str = S.pred_from_str let pred_to_str = S.pred_to_str diff --git a/transformers/lib/states/Product.ml b/transformers/lib/states/Product.ml index eca0bf7a0..a3d063c55 100644 --- a/transformers/lib/states/Product.ml +++ b/transformers/lib/states/Product.ml @@ -27,7 +27,7 @@ module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) : List.map (fun (a, args, ret) -> (A1 a, args, ret)) (S1.list_actions ()) @ List.map (fun (a, args, ret) -> (A2 a, args, ret)) (S2.list_actions ()) - type pred = P1 of S1.pred | P2 of S2.pred + type pred = P1 of S1.pred | P2 of S2.pred [@@deriving yojson] let pred_from_str s = match IDer.get_ided s with diff --git a/transformers/lib/states/Sum.ml b/transformers/lib/states/Sum.ml index c0ce11120..42674a0b8 100644 --- a/transformers/lib/states/Sum.ml +++ b/transformers/lib/states/Sum.ml @@ -27,7 +27,7 @@ module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) : List.map (fun (a, args, ret) -> (A1 a, args, ret)) (S1.list_actions ()) @ List.map (fun (a, args, ret) -> (A2 a, args, ret)) (S2.list_actions ()) - type pred = P1 of S1.pred | P2 of S2.pred + type pred = P1 of S1.pred | P2 of S2.pred [@@deriving yojson] let pred_from_str s = match IDer.get_ided s with From a3b883c5040d9ced2f208949a80b413a3bcd1953 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Tue, 30 Sep 2025 23:37:15 +0100 Subject: [PATCH 03/29] add assume_type to delayed Signed-off-by: Sacha Ayoun --- GillianCore/monadic/delayed.ml | 9 +++++++++ GillianCore/monadic/delayed.mli | 1 + 2 files changed, 10 insertions(+) diff --git a/GillianCore/monadic/delayed.ml b/GillianCore/monadic/delayed.ml index deae9e9a4..c1b77bb41 100644 --- a/GillianCore/monadic/delayed.ml +++ b/GillianCore/monadic/delayed.ml @@ -95,6 +95,15 @@ let delayed_eval2 f x y ~curr_pc = let reduce = delayed_eval FOSolver.reduce_expr let resolve_loc = delayed_eval FOSolver.resolve_loc_name +let assume_types e_tys ~curr_pc = + let new_tys = Engine.Typing.reverse_type_lexpr false curr_pc.Pc.gamma e_tys in + match new_tys with + | None -> [] (* type inconsistency, vanish *) + | Some new_tys -> + let new_tys = Engine.Type_env.to_list new_tys in + let new_pc = Pc.extend_types curr_pc new_tys in + [ Branch.make ~pc:new_pc ~value:() ] + let entails = let entails ~pc lhs rhs = let temp_pc = Pc.extend pc lhs in diff --git a/GillianCore/monadic/delayed.mli b/GillianCore/monadic/delayed.mli index dc0413bf4..b8c87eca6 100644 --- a/GillianCore/monadic/delayed.mli +++ b/GillianCore/monadic/delayed.mli @@ -20,6 +20,7 @@ val if_sure : Expr.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t val branch_entailment : (Expr.t * (unit -> 'a t)) list -> 'a t val leak_pc_copy : unit -> Engine.Gpc.t t val branch_on : Expr.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t +val assume_types : (Expr.t * Type.t) list -> unit t module Syntax : sig val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t From b69ad034edea041f6a6f683d048d9b8e3187fd87 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 1 Oct 2025 00:25:49 +0100 Subject: [PATCH 04/29] yeet myasrt Signed-off-by: Sacha Ayoun --- transformers/lib/prebuilt/C.ml | 3 +- .../lib/prebuilt/c_states/BlockTree.ml | 36 ++++++------------- transformers/lib/prebuilt/c_states/CGEnv.ml | 2 +- .../lib/prebuilt/c_states/LActions.ml | 2 +- transformers/lib/states/ActionAdder.ml | 7 ++-- transformers/lib/states/Agreement.ml | 5 ++- transformers/lib/states/Exclusive.ml | 4 +-- transformers/lib/states/Fix.ml | 31 ++++++++++++++++ transformers/lib/states/Freeable.ml | 6 ++-- transformers/lib/states/MList.ml | 14 +++----- transformers/lib/states/MyAsrt.ml | 20 ----------- transformers/lib/states/MyMonadicSMemory.ml | 15 ++++---- transformers/lib/states/PMap.ml | 20 ++++------- transformers/lib/states/Product.ml | 4 +-- transformers/lib/states/Sum.ml | 6 ++-- 15 files changed, 75 insertions(+), 100 deletions(-) create mode 100644 transformers/lib/states/Fix.ml delete mode 100644 transformers/lib/states/MyAsrt.ml diff --git a/transformers/lib/prebuilt/C.ml b/transformers/lib/prebuilt/C.ml index dd84b9d6b..839458a10 100644 --- a/transformers/lib/prebuilt/C.ml +++ b/transformers/lib/prebuilt/C.ml @@ -89,8 +89,7 @@ module ExtendMemory (S : C_PMapType) = struct | _ -> false let map_fixes mapper = - States.MyUtils.deep_map - (States.MyAsrt.map_cp (fun (p, i, o) -> (mapper p, i, o))) + States.MyUtils.deep_map (fun (p, i, o) -> (mapper p, i, o)) let get_fixes = function | BaseError e -> S.get_fixes e |> map_fixes S.pred_to_str diff --git a/transformers/lib/prebuilt/c_states/BlockTree.ml b/transformers/lib/prebuilt/c_states/BlockTree.ml index 747d06d9e..fb588660a 100644 --- a/transformers/lib/prebuilt/c_states/BlockTree.ml +++ b/transformers/lib/prebuilt/c_states/BlockTree.ml @@ -5,7 +5,6 @@ module DR = Delayed_result module DO = Delayed_option module SS = Gillian.Utils.Containers.SS module CoreP = Constr.Core -module MyAsrt = States.MyAsrt (* Import from Cgil lib: *) module CConstants = Cgil_lib.CConstants @@ -1596,7 +1595,7 @@ module M = struct ] ) -> let perm = ValueTranslation.permission_of_string perm_string in let chunk = ValueTranslation.chunk_of_string chunk_string in - let* sval = SVal.of_gil_expr_exn sval_e in + let* sval = SVal.of_gil_expr_vanish sval_e in prod_single s ofs chunk sval perm |> filter_errors | ( Array, [ @@ -1688,34 +1687,22 @@ module M = struct in let null_ptr = Expr.EList [ null_typ; Expr.int 0 ] in [ + [ (Single, [ ofs; chunk_as_expr ], [ value; freeable_perm ]) ]; [ - MyAsrt.CorePred - (Single, [ ofs; chunk_as_expr ], [ value; freeable_perm ]); - MyAsrt.Types - [ (new_var1, Type.ObjectType); (new_var2, Type.IntType) ]; - ]; - [ - MyAsrt.CorePred - (Single, [ ofs; chunk_as_expr ], [ null_ptr; freeable_perm ]); + (Single, [ ofs; chunk_as_expr ], [ null_ptr; freeable_perm ]); ]; ] | _ -> - let type_str, type_gil = + let type_str = match chunk with - | Chunk.Mfloat32 -> (single_type, Type.NumberType) - | Chunk.Mfloat64 -> (float_type, Type.NumberType) - | Chunk.Mint64 -> (long_type, Type.IntType) - | _ -> (int_type, Type.IntType) + | Chunk.Mfloat32 -> single_type + | Chunk.Mfloat64 -> float_type + | Chunk.Mint64 -> long_type + | _ -> int_type in let new_var = Expr.LVar (LVar.alloc ()) in let value = Expr.EList [ Expr.string type_str; new_var ] in - [ - [ - MyAsrt.CorePred - (Single, [ ofs; chunk_as_expr ], [ value; freeable_perm ]); - MyAsrt.Types [ (new_var, type_gil) ]; - ]; - ] + [ [ (Single, [ ofs; chunk_as_expr ], [ value; freeable_perm ]) ] ] in (* Additional fix for store operation to handle case of unitialized memory *) if is_store then @@ -1726,10 +1713,7 @@ module M = struct in let uninit = [ - [ - MyAsrt.CorePred - (Hole, [ ofs; offset_by_chunk ofs chunk ], [ freeable_perm ]); - ]; + [ (Hole, [ ofs; offset_by_chunk ofs chunk ], [ freeable_perm ]) ]; ] in uninit @ fixes diff --git a/transformers/lib/prebuilt/c_states/CGEnv.ml b/transformers/lib/prebuilt/c_states/CGEnv.ml index 44d533503..ba877c8cd 100644 --- a/transformers/lib/prebuilt/c_states/CGEnv.ml +++ b/transformers/lib/prebuilt/c_states/CGEnv.ml @@ -10,7 +10,7 @@ module M : States.MyMonadicSMemory.S with type t = Global_env.t = struct type t = Global_env.t [@@deriving yojson] type err_t = unit [@@deriving show, yojson] type action = GetDef - type pred = unit + type pred = unit [@@deriving show, yojson] let pp = Global_env.pp diff --git a/transformers/lib/prebuilt/c_states/LActions.ml b/transformers/lib/prebuilt/c_states/LActions.ml index 1cb77ed5e..7ebaf374e 100644 --- a/transformers/lib/prebuilt/c_states/LActions.ml +++ b/transformers/lib/prebuilt/c_states/LActions.ml @@ -1,5 +1,5 @@ type ac = DropPerm | GetCurPerm | WeakValidPointer | Store | Load -type ga = Single | Array | Hole | Zeros | Bounds +type ga = Single | Array | Hole | Zeros | Bounds [@@deriving yojson] let str_ac = function | DropPerm -> "dropperm" diff --git a/transformers/lib/states/ActionAdder.ml b/transformers/lib/states/ActionAdder.ml index 912356738..8de5730bc 100644 --- a/transformers/lib/states/ActionAdder.ml +++ b/transformers/lib/states/ActionAdder.ml @@ -14,7 +14,7 @@ module type ActionAddition = sig action -> t -> Expr.t list -> (t * Expr.t list, err_t) result Delayed.t val can_fix : err_t -> bool - val get_fixes : err_t -> string MyAsrt.t list list + val get_fixes : err_t -> string Fix.t list val get_recovery_tactic : err_t -> Expr.t Gillian.General.Recovery_tactic.t end @@ -65,9 +65,8 @@ struct | BaseErr e -> S.get_fixes e | AddedErr e -> A.get_fixes e - |> MyUtils.deep_map - @@ MyAsrt.map_cp (fun (p, i, o) -> - (S.pred_from_str p |> Option.get, i, o)) + |> MyUtils.deep_map @@ fun (p, i, o) -> + (S.pred_from_str p |> Option.get, i, o) let get_recovery_tactic = function | BaseErr e -> S.get_recovery_tactic e diff --git a/transformers/lib/states/Agreement.ml b/transformers/lib/states/Agreement.ml index 68233b48b..3ca2c7281 100644 --- a/transformers/lib/states/Agreement.ml +++ b/transformers/lib/states/Agreement.ml @@ -8,7 +8,7 @@ module Recovery_tactic = Gillian.General.Recovery_tactic type t = Expr.t option [@@deriving yojson] type err_t = MissingState [@@deriving show, yojson] type action = Load -type pred = Ag +type pred = Ag [@@deriving yojson] let pp = Fmt.(option ~none:(any "None") Expr.pp) @@ -103,5 +103,4 @@ let can_fix = function | MissingState -> true let get_fixes = function - | MissingState -> - [ [ MyAsrt.CorePred (Ag, [], [ LVar (Generators.fresh_svar ()) ]) ] ] + | MissingState -> [ [ (Ag, [], [ Expr.LVar (Generators.fresh_svar ()) ]) ] ] diff --git a/transformers/lib/states/Exclusive.ml b/transformers/lib/states/Exclusive.ml index 8bd28fff2..3cbbced1e 100644 --- a/transformers/lib/states/Exclusive.ml +++ b/transformers/lib/states/Exclusive.ml @@ -8,7 +8,7 @@ module Recovery_tactic = Gillian.General.Recovery_tactic type t = Expr.t option [@@deriving show, yojson] type err_t = MissingState [@@deriving show, yojson] type action = Load | Store -type pred = Ex +type pred = Ex [@@deriving yojson] let pp = Fmt.(option ~none:(any "None") Expr.pp) @@ -95,4 +95,4 @@ let get_recovery_tactic _ = Recovery_tactic.none let can_fix MissingState = true let get_fixes MissingState = - [ [ MyAsrt.CorePred (Ex, [], [ LVar (Generators.fresh_svar ()) ]) ] ] + [ [ (Ex, [], [ Expr.LVar (Generators.fresh_svar ()) ]) ] ] diff --git a/transformers/lib/states/Fix.ml b/transformers/lib/states/Fix.ml new file mode 100644 index 000000000..94dc1c23a --- /dev/null +++ b/transformers/lib/states/Fix.ml @@ -0,0 +1,31 @@ +open Gillian.Gil_syntax + +type 'cp atom = 'cp * Expr.t list * Expr.t list [@@deriving yojson, show] +type 'cp t = 'cp atom list [@@deriving yojson, show] + +let lvars (fix : 'cp t) = + let open Gillian.Utils.Containers in + List.fold_left + (fun acc (_, ins, outs) -> + let acc = + List.fold_left (fun acc e -> SS.union acc (Expr.lvars e)) acc ins + in + List.fold_left (fun acc e -> SS.union acc (Expr.lvars e)) acc outs) + SS.empty fix + +let alocs (fix : 'cp t) = + let open Gillian.Utils.Containers in + List.fold_left + (fun acc (_, ins, outs) -> + let acc = + List.fold_left (fun acc e -> SS.union acc (Expr.alocs e)) acc ins + in + List.fold_left (fun acc e -> SS.union acc (Expr.alocs e)) acc outs) + SS.empty fix + +let subst (subst : Gillian.Symbolic.Subst.t) (fix : 'a t) : 'a t = + let le_subst = Gillian.Symbolic.Subst.subst_in_expr subst ~partial:true in + let subst_atom (cp, ins, outs) = + (cp, List.map le_subst ins, List.map le_subst outs) + in + List.map subst_atom fix diff --git a/transformers/lib/states/Freeable.ml b/transformers/lib/states/Freeable.ml index 3ba0964f8..4ebcb153b 100644 --- a/transformers/lib/states/Freeable.ml +++ b/transformers/lib/states/Freeable.ml @@ -177,11 +177,11 @@ module Make (S : MyMonadicSMemory.S) : let get_fixes = function | SubError e -> - S.get_fixes e |> MyUtils.deep_map (MyAsrt.map_cp lift_corepred) + S.get_fixes e |> MyUtils.deep_map lift_corepred (* Fix can either be inner fix, or if empty the memory is freed! But Gillian C/WISL doesn't implement this so we comment it out to have comparable performance *) - (* @ [ [ MyAsrt.CorePred (FreedPred, [], []) ] ]*) - | MissingFreed -> [ [ MyAsrt.CorePred (FreedPred, [], []) ] ] + (* @ [ [ (FreedPred, [], []) ] ]*) + | MissingFreed -> [ [ (FreedPred, [], []) ] ] | _ -> failwith "Invalid fix call" end diff --git a/transformers/lib/states/MList.ml b/transformers/lib/states/MList.ml index 67d5bf75c..b8041d100 100644 --- a/transformers/lib/states/MList.ml +++ b/transformers/lib/states/MList.ml @@ -112,7 +112,9 @@ module Make (S : MyMonadicSMemory.S) : | Length, [ n' ] -> ( match n with | Some _ -> Delayed.vanish () - | None -> Delayed.return (b, Some n')) + | None -> + let+ () = Delayed.assume_types [ (n', Type.IntType) ] in + (b, Some n')) | Length, _ -> failwith "Invalid arguments for length produce" let compose s1 s2 = @@ -228,15 +230,9 @@ module Make (S : MyMonadicSMemory.S) : | OutOfBounds _ -> false let get_fixes = function - | SubError (idx, e) -> - S.get_fixes e |> MyUtils.deep_map (MyAsrt.map_cp (lift_corepred idx)) + | SubError (idx, e) -> S.get_fixes e |> MyUtils.deep_map (lift_corepred idx) | MissingLength -> let lvar = Expr.LVar (LVar.alloc ()) in - [ - [ - MyAsrt.CorePred (Length, [], [ lvar ]); - MyAsrt.Types [ (lvar, Type.IntType) ]; - ]; - ] + [ [ (Length, [], [ lvar ]) ] ] | _ -> failwith "Called get_fixes on unfixable error" end diff --git a/transformers/lib/states/MyAsrt.ml b/transformers/lib/states/MyAsrt.ml deleted file mode 100644 index 5524979ee..000000000 --- a/transformers/lib/states/MyAsrt.ml +++ /dev/null @@ -1,20 +0,0 @@ -open Gil_syntax - -(* Similar to Gil_syntax.Asrt.t, but made to be simpler and nicer to use: - - typed core predicate names - - removed wands + predicates as using them from within a state model seems complicated+uneeded *) -type 'cp t = - | Emp (** Empty heap *) - | Pure of Expr.t (** Pure formula *) - | Types of (Expr.t * Type.t) list (** Typing assertion *) - | CorePred of 'cp * Expr.t list * Expr.t list (** Core predicate *) - -let map_cp - (f : 'cp1 * Expr.t list * Expr.t list -> 'cp2 * Expr.t list * Expr.t list) : - 'cp1 t -> 'cp2 t = function - | Emp -> Emp - | Pure f -> Pure f - | Types tys -> Types tys - | CorePred (cp, i, o) -> - let cp', i', o' = f (cp, i, o) in - CorePred (cp', i', o') diff --git a/transformers/lib/states/MyMonadicSMemory.ml b/transformers/lib/states/MyMonadicSMemory.ml index 93cd08adc..acd3bba27 100644 --- a/transformers/lib/states/MyMonadicSMemory.ml +++ b/transformers/lib/states/MyMonadicSMemory.ml @@ -66,7 +66,7 @@ module type S = sig (** Get the fixes for an error, as a list of fixes -- a fix is a list of core predicates to produce onto the state. *) - val get_fixes : err_t -> pred MyAsrt.t list list + val get_fixes : err_t -> pred Fix.t list (** The recovery tactic to attempt to resolve an error, by eg. unfolding predicates *) @@ -174,14 +174,11 @@ struct let mapping (p, ins, outs) = Asrt.CorePred (pred_to_str p, ins, outs) in List.map mapping core_preds @ formulas - let get_fixes e = - get_fixes e - |> MyUtils.deep_map @@ function - | MyAsrt.Emp -> Asrt.Emp - | MyAsrt.Pure f -> Asrt.Pure f - | MyAsrt.Types ts -> Asrt.Types ts - | MyAsrt.CorePred (p, ins, outs) -> - Asrt.CorePred (pred_to_str p, ins, outs) + let get_fixes (e : err_t) = + let fixes = get_fixes e in + MyUtils.deep_map + (fun (p, ins, outs) -> Asrt.CorePred (pred_to_str p, ins, outs)) + fixes (* Override methods to keep implementations light *) let clear _ = empty () diff --git a/transformers/lib/states/PMap.ml b/transformers/lib/states/PMap.ml index ebe5d2277..80a7100ed 100644 --- a/transformers/lib/states/PMap.ml +++ b/transformers/lib/states/PMap.ml @@ -287,6 +287,7 @@ struct match s with | _, Some _ -> Delayed.vanish () | h, None -> + let* () = Delayed.assume_types [ (d', Type.SetType) ] in (* This would be the correct implementation, but the handling of sets is bad so it creates all sorts of issues (eg. in matching plans)... let dom = ExpMap.bindings h |> List.map fst in @@ -389,18 +390,11 @@ struct | NotAllocated _ -> false let get_fixes = function - | SubError (idx, idx', e) -> - S.get_fixes e - |> MyUtils.deep_map @@ MyAsrt.map_cp @@ lift_corepred idx' - |> List.map @@ List.cons @@ MyAsrt.Pure Expr.Infix.(idx == idx') + | SubError (_idx, idx', e) -> + S.get_fixes e |> MyUtils.deep_map @@ lift_corepred idx' | MissingDomainSet -> let lvar = Expr.LVar (LVar.alloc ()) in - [ - [ - MyAsrt.CorePred (DomainSet, [], [ lvar ]); - MyAsrt.Types [ (lvar, Type.SetType) ]; - ]; - ] + [ [ (DomainSet, [], [ lvar ]) ] ] | _ -> failwith "Called get_fixes on unfixable error" end @@ -552,10 +546,8 @@ struct | InvalidIndexValue _ -> false let get_fixes = function - | SubError (idx, idx', e) -> - S.get_fixes e - |> MyUtils.deep_map @@ MyAsrt.map_cp @@ lift_corepred idx' - |> List.map @@ List.cons @@ MyAsrt.Pure Expr.Infix.(idx == idx') + | SubError (_idx, idx', e) -> + S.get_fixes e |> MyUtils.deep_map @@ lift_corepred idx' | _ -> failwith "Called get_fixes on unfixable error" end diff --git a/transformers/lib/states/Product.ml b/transformers/lib/states/Product.ml index a3d063c55..38d286101 100644 --- a/transformers/lib/states/Product.ml +++ b/transformers/lib/states/Product.ml @@ -133,6 +133,6 @@ module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) : | E2 e -> S2.can_fix e let get_fixes = function - | E1 e -> S1.get_fixes e |> MyUtils.deep_map (MyAsrt.map_cp lift_corepred_1) - | E2 e -> S2.get_fixes e |> MyUtils.deep_map (MyAsrt.map_cp lift_corepred_2) + | E1 e -> S1.get_fixes e |> MyUtils.deep_map lift_corepred_1 + | E2 e -> S2.get_fixes e |> MyUtils.deep_map lift_corepred_2 end diff --git a/transformers/lib/states/Sum.ml b/transformers/lib/states/Sum.ml index 42674a0b8..d7a249837 100644 --- a/transformers/lib/states/Sum.ml +++ b/transformers/lib/states/Sum.ml @@ -192,9 +192,7 @@ module Make (IDs : IDs) (S1 : MyMonadicSMemory.S) (S2 : MyMonadicSMemory.S) : let get_fixes e = match e with - | E1 e1 -> - S1.get_fixes e1 |> MyUtils.deep_map (MyAsrt.map_cp lift_corepred_1) - | E2 e2 -> - S2.get_fixes e2 |> MyUtils.deep_map (MyAsrt.map_cp lift_corepred_2) + | E1 e1 -> S1.get_fixes e1 |> MyUtils.deep_map lift_corepred_1 + | E2 e2 -> S2.get_fixes e2 |> MyUtils.deep_map lift_corepred_2 | _ -> failwith "get_fixes: invalid error" end From df6a85b02922739cc2262a375f5f680b05807a01 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Wed, 1 Oct 2025 00:27:09 +0100 Subject: [PATCH 05/29] =?UTF-8?q?add=20bi-abductive=20state=20model=20?= =?UTF-8?q?=F0=9F=8E=89?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Sacha Ayoun --- transformers/lib/states/bi_abd.ml | 120 ++++++++++++++++++++++++++++++ 1 file changed, 120 insertions(+) create mode 100644 transformers/lib/states/bi_abd.ml diff --git a/transformers/lib/states/bi_abd.ml b/transformers/lib/states/bi_abd.ml new file mode 100644 index 000000000..f21566ab3 --- /dev/null +++ b/transformers/lib/states/bi_abd.ml @@ -0,0 +1,120 @@ +open Gillian.Monadic +module DR = Delayed_result + +type ('a, 'pred) bi_state = { state : 'a; anti_frame : 'pred Fix.t } +[@@deriving show, yojson] + +module Make (Mem : MyMonadicSMemory.S) : + MyMonadicSMemory.S with type t = (Mem.t, Mem.pred) bi_state = struct + type pred = Mem.pred [@@deriving yojson] + + let pred_from_str = Mem.pred_from_str + let pred_to_str = Mem.pred_to_str + let pp_pred = Fmt.of_to_string pred_to_str + let list_preds = Mem.list_preds + + type t = (Mem.t, pred) bi_state [@@deriving show, yojson] + type err_t = Mem.err_t [@@deriving show, yojson] + type action = Mem.action + + let action_from_str = Mem.action_from_str + let action_to_str = Mem.action_to_str + let list_actions = Mem.list_actions + let empty () : t = { state = Mem.empty (); anti_frame = [] } + + let with_bi_abduction ~f state args = + let open Delayed.Syntax in + let rec aux ~fuel state = + (* If fuel is exhausted we give up *) + let* () = if fuel <= 0 then Delayed.vanish () else Delayed.return () in + let* r = f state.state args in + match r with + | Ok (state', v) -> DR.ok ({ state with state = state' }, v) + | Error e when not (Mem.can_fix e) -> + (* can_fix is true when the error is a `miss` *) + DR.error e + | Error err -> + (* This is the missing error case *) + (* We take each fix one by one *) + let* cp_list = + Mem.get_fixes err |> List.map Delayed.return |> Delayed.branches + in + let* state' = + List.fold_left + (fun state (pred, ins, outs) -> + let* state = state in + Mem.produce pred state (ins @ outs)) + (Delayed.return state.state) + cp_list + in + let anti_frame = cp_list @ state.anti_frame in + (* We produce that fix in our current state *) + let new_state = { state = state'; anti_frame } in + aux ~fuel:(fuel - 1) new_state + in + (* We try to fix twice *) + aux ~fuel:2 state + + let execute_action action = with_bi_abduction ~f:(Mem.execute_action action) + + let produce pred { state; anti_frame } args = + let open Delayed.Syntax in + let+ state = Mem.produce pred state args in + { state; anti_frame } + + let consume pred state args = + with_bi_abduction ~f:(Mem.consume pred) state args + + let is_empty s = Mem.is_empty s.state + + (* Variables *) + + let lvars s = + let open Gillian.Utils.Containers in + Mem.lvars s.state |> SS.union (Fix.lvars s.anti_frame) + + let alocs s = + let open Gillian.Utils.Containers in + Mem.alocs s.state |> SS.union (Fix.alocs s.anti_frame) + + let substitution_in_place subst s = + let open Monadic.Delayed.Syntax in + let+ state = Mem.substitution_in_place subst s.state in + let anti_frame = Fix.subst subst s.anti_frame in + { state; anti_frame } + + (* Error handling *) + + let get_recovery_tactic = Mem.get_recovery_tactic + let can_fix e = Mem.can_fix e + + let get_fixes _ = + failwith + "Bi_abd state should not be used as an input to the bi-abduction state \ + module. That one is legacy." + + (* Assertions *) + + let assertions_others _ = + failwith + "Should not be transforming bi-abd state to assertions, only its first \ + component" + + let assertions _ = + failwith + "Should not be transforming bi-abd state to assertions, only its first \ + component" + + (* The rest of the functions remain unimplemented as Bi_abd makes no sense being an input to other transformers. *) + + let instantiate _ = + failwith "Bi_abd state should not be used as an input state" + + let is_exclusively_owned _ = + failwith "Bi_abd state should not be used as an input state" + + let is_concrete _ = + failwith "Bi_abd state should not be used as an input state" + + let compose _ _ = failwith "Bi_abd state should not be used as an input state" +end From 9de2bfabc564094742339179f3029d6a12157bc8 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Tue, 7 Oct 2025 10:17:18 +0100 Subject: [PATCH 06/29] move make_callgraph to Prog.ml Signed-off-by: Sacha Ayoun --- GillianCore/GIL_Syntax/Gil_syntax.mli | 2 ++ GillianCore/GIL_Syntax/Prog.ml | 24 +++++++++++++++++++++++ GillianCore/command_line/act_console.ml | 26 +------------------------ 3 files changed, 27 insertions(+), 25 deletions(-) diff --git a/GillianCore/GIL_Syntax/Gil_syntax.mli b/GillianCore/GIL_Syntax/Gil_syntax.mli index 33fccd51c..47bb5dacd 100644 --- a/GillianCore/GIL_Syntax/Gil_syntax.mli +++ b/GillianCore/GIL_Syntax/Gil_syntax.mli @@ -1154,6 +1154,8 @@ module Prog : sig (** Print indexed *) val pp_indexed : Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, int) t -> unit + + val make_callgraph : ('a, 'b) t -> Call_graph.t end (** @canonical Gillian.Gil_syntax.Visitors *) diff --git a/GillianCore/GIL_Syntax/Prog.ml b/GillianCore/GIL_Syntax/Prog.ml index f0bd3b943..bf7d85882 100644 --- a/GillianCore/GIL_Syntax/Prog.ml +++ b/GillianCore/GIL_Syntax/Prog.ml @@ -253,3 +253,27 @@ let add_macro (prog : ('a, 'b) t) (macro : Macro.t) : ('a, 'b) t = let add_bispec (prog : ('a, 'b) t) (bi_spec : BiSpec.t) : ('a, 'b) t = Hashtbl.add prog.bi_specs bi_spec.bispec_name bi_spec; prog + +let make_callgraph (prog : ('a, 'b) t) = + let fcalls = + Hashtbl.fold + (fun _ proc acc -> + Proc.(proc.proc_name, proc.proc_aliases, proc.proc_calls) :: acc) + prog.procs [] + in + let call_graph = Call_graph.make () in + let fnames = Hashtbl.create (List.length fcalls * 2) in + fcalls + |> List.iter (fun (sym, aliases, _) -> + Call_graph.add_proc call_graph sym; + Hashtbl.add fnames sym sym; + aliases |> List.iter (fun alias -> Hashtbl.add fnames alias sym)); + fcalls + |> List.iter (fun (caller, _, callees) -> + callees + |> List.iter (fun callee -> + match Hashtbl.find_opt fnames callee with + | Some callee -> + Call_graph.add_proc_call call_graph caller callee + | None -> ())); + call_graph diff --git a/GillianCore/command_line/act_console.ml b/GillianCore/command_line/act_console.ml index 19f60d6f4..a6704fbc9 100644 --- a/GillianCore/command_line/act_console.ml +++ b/GillianCore/command_line/act_console.ml @@ -64,30 +64,6 @@ struct let out_path = Filename.concat dirname (fname ^ "_bi.gil") in Io_utils.save_file_pp out_path (Prog.pp_labeled ~pp_annot) e_prog - let make_callgraph (prog : ('a, 'b) Prog.t) = - let fcalls = - Hashtbl.fold - (fun _ proc acc -> - Proc.(proc.proc_name, proc.proc_aliases, proc.proc_calls) :: acc) - prog.procs [] - in - let call_graph = Call_graph.make () in - let fnames = Hashtbl.create (List.length fcalls * 2) in - fcalls - |> List.iter (fun (sym, aliases, _) -> - Call_graph.add_proc call_graph sym; - Hashtbl.add fnames sym sym; - aliases |> List.iter (fun alias -> Hashtbl.add fnames alias sym)); - fcalls - |> List.iter (fun (caller, _, callees) -> - callees - |> List.iter (fun callee -> - match Hashtbl.find_opt fnames callee with - | Some callee -> - Call_graph.add_proc_call call_graph caller callee - | None -> ())); - call_graph - let process_files files already_compiled @@ -109,7 +85,7 @@ struct let+ prog = Gil_parsing.eprog_to_prog ~other_imports:PC.other_imports e_prog in - let call_graph = make_callgraph prog in + let call_graph = Prog.make_callgraph prog in let () = L.normal (fun m -> m "@\n*** Stage 2: DONE transforming the program.@\n") in From 18776ebd5a5fb4eab30612649dcd07dd46ed1f58 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 8 Nov 2025 13:42:21 +0000 Subject: [PATCH 07/29] BiState carries around a set of proc names but is never used??? Signed-off-by: Sacha Ayoun --- GillianCore/engine/BiAbduction/BiState.ml | 52 +++++++++------------- GillianCore/engine/BiAbduction/BiState.mli | 2 +- 2 files changed, 22 insertions(+), 32 deletions(-) diff --git a/GillianCore/engine/BiAbduction/BiState.ml b/GillianCore/engine/BiAbduction/BiState.ml index 61ee5f6b5..39400ac10 100644 --- a/GillianCore/engine/BiAbduction/BiState.ml +++ b/GillianCore/engine/BiAbduction/BiState.ml @@ -2,7 +2,7 @@ open Containers open Literal module L = Logging -type 'a _t = { procs : SS.t; state : 'a; af_state : 'a } [@@deriving yojson] +type 'a _t = { state : 'a; af_state : 'a } [@@deriving yojson] module Make (State : SState.S) = struct type heap_t = State.heap_t @@ -19,9 +19,8 @@ module Make (State : SState.S) = struct type action_ret = (t * Expr.t list, err_t) result list - let make ~(procs : SS.t) ~(state : State.t) ~(init_data : State.init_data) : t - = - { procs; state; af_state = State.init init_data } + let make ~(state : State.t) ~(init_data : State.init_data) : t = + { state; af_state = State.init init_data } let lift_error st : State.err_t -> err_t = function | StateErr.EMem e -> StateErr.EMem (st, e) @@ -54,8 +53,7 @@ module Make (State : SState.S) = struct let state' = State.set_store state store in { bi_state with state = state' } - let assume ?(unfold = false) ({ procs; state; af_state } : t) (v : Expr.t) : - t list = + let assume ?(unfold = false) ({ state; af_state } : t) (v : Expr.t) : t list = let new_states = State.assume ~unfold state v in match new_states with | [] -> [] @@ -63,11 +61,10 @@ module Make (State : SState.S) = struct (* Slight optim, we don't copy the anti_frame if we have only one state. *) let rest = List.map - (fun state' -> - { procs; state = state'; af_state = State.copy af_state }) + (fun state' -> { state = state'; af_state = State.copy af_state }) rest in - { procs; state = first_state; af_state } :: rest + { state = first_state; af_state } :: rest let assume_a ?(matching = false) @@ -99,14 +96,11 @@ module Make (State : SState.S) = struct let get_type ({ state; _ } : t) (v : Expr.t) : Type.t option = State.get_type state v - let copy ({ procs; state; af_state } : t) : t = - { procs; state = State.copy state; af_state = State.copy af_state } + let copy ({ state; af_state } : t) : t = + { state = State.copy state; af_state = State.copy af_state } - let simplify - ?save - ?kill_new_lvars - ?matching:_ - ({ procs; state; af_state } : t) : SVal.SESubst.t * t list = + let simplify ?save ?kill_new_lvars ?matching:_ ({ state; af_state } : t) : + SVal.SESubst.t * t list = let subst, states = State.simplify ?save ?kill_new_lvars state in let states = List.concat_map @@ -118,7 +112,7 @@ module Make (State : SState.S) = struct | LVar x -> if SS.mem x svars then None else Some x_v | _ -> Some x_v); List.map - (fun af_state -> { procs; state; af_state }) + (fun af_state -> { state; af_state }) (State.substitution_in_place af_subst af_state)) states in @@ -128,10 +122,9 @@ module Make (State : SState.S) = struct let simplify_val ({ state; _ } : t) (v : Expr.t) : Expr.t = State.simplify_val state v - let pp fmt { procs; state; af_state } = - Fmt.pf fmt "PROCS:@\n@[%a@]@\nMAIN STATE:@\n%a@\nANTI FRAME:@\n%a@\n" - Fmt.(iter ~sep:comma SS.iter string) - procs State.pp state State.pp af_state + let pp fmt { state; af_state } = + Fmt.pf fmt "MAIN STATE:@\n%a@\nANTI FRAME:@\n%a@\n" State.pp state State.pp + af_state (* TODO: By-need formatter *) let pp_by_need _ _ _ fmt state = pp fmt state @@ -217,7 +210,6 @@ module Make (State : SState.S) = struct type post_res = (Flag.t * Asrt.t list) option let match_ - (_ : SS.t) (state : State.t) (af_state : State.t) (subst : SVal.SESubst.t) @@ -348,7 +340,7 @@ module Make (State : SState.S) = struct Fmt.(list ~sep:comma Expr.pp) args SVal.SESubst.pp subst_i)); - let { procs; state; af_state } = bi_state in + let { state; af_state } = bi_state in let old_store = State.get_store state in @@ -367,7 +359,7 @@ module Make (State : SState.S) = struct BI-ABDUCTION:@\n\ %a@]@\n" spec.data.spec_name MP.pp spec.mp)); - let ret_states = match_ procs state' af_state subst spec.mp in + let ret_states = match_ state' af_state subst spec.mp in L.( verbose (fun m -> m "Concluding matching With %d results" (List.length ret_states))); @@ -407,7 +399,7 @@ module Make (State : SState.S) = struct let final_state' : State.t = update_store final_state' (Some x) v_ret in (* FIXME: NOT WORKING DUE TO SIMPLIFICATION TYPE CHANGING *) let _ = State.simplify ~matching:true final_state' in - let bi_state : t = { procs; state = final_state'; af_state = af_state' } in + let bi_state : t = { state = final_state'; af_state = af_state' } in L.( verbose (fun m -> @@ -469,14 +461,14 @@ module Make (State : SState.S) = struct let rec execute_action (action : string) - ({ procs; state; af_state } : t) + ({ state; af_state } : t) (args : Expr.t list) : action_ret = let open Syntaxes.List in let* ret = State.execute_action action state args in match ret with - | Ok (state', outs) -> [ Ok ({ procs; state = state'; af_state }, outs) ] + | Ok (state', outs) -> [ Ok ({ state = state'; af_state }, outs) ] | Error err when not (State.can_fix err) -> - [ Error (lift_error { procs; state; af_state } err) ] + [ Error (lift_error { state; af_state } err) ] | Error err -> ( match State.get_fixes err with | [] -> [] (* No fix, we stop *) @@ -486,9 +478,7 @@ module Make (State : SState.S) = struct let af_state' = State.copy af_state in let* state' = fix_list_apply state' fix in let* af_state' = fix_list_apply af_state' fix in - execute_action action - { procs; state = state'; af_state = af_state' } - args) + execute_action action { state = state'; af_state = af_state' } args) let get_equal_values { state; _ } = State.get_equal_values state let get_heap { state; _ } = State.get_heap state diff --git a/GillianCore/engine/BiAbduction/BiState.mli b/GillianCore/engine/BiAbduction/BiState.mli index cc8c081d7..12871b115 100644 --- a/GillianCore/engine/BiAbduction/BiState.mli +++ b/GillianCore/engine/BiAbduction/BiState.mli @@ -10,6 +10,6 @@ module Make (BaseState : PState.S) : sig and type init_data = BaseState.init_data and type m_err_t = BaseState.t _t * BaseState.m_err_t - val make : procs:SS.t -> state:BaseState.t -> init_data:init_data -> t + val make : state:BaseState.t -> init_data:init_data -> t val get_components : t -> BaseState.t * BaseState.t end From 1c2dba3ec65ab49c422002e78d3362372167e771 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 8 Nov 2025 13:51:19 +0000 Subject: [PATCH 08/29] expose more stuff Signed-off-by: Sacha Ayoun --- GillianCore/engine/symbolic_semantics/Symbolic.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/GillianCore/engine/symbolic_semantics/Symbolic.ml b/GillianCore/engine/symbolic_semantics/Symbolic.ml index cd5f3a749..0492488f1 100644 --- a/GillianCore/engine/symbolic_semantics/Symbolic.ml +++ b/GillianCore/engine/symbolic_semantics/Symbolic.ml @@ -6,6 +6,8 @@ module Values = struct (** @inline *) include SVal.M + + module Subst = SVal.SESubst end (** @canonical Gillian.Symbolic.Subst *) @@ -56,3 +58,9 @@ module Dummy_memory = SMemory.Dummy (** @canonical Gillian.Symbolic.Legacy_s_memory *) module Legacy_s_memory = Legacy_s_memory + +(** @canonical Gillian.Symbolic.Store *) +module Store = SStore + +module SState = SState +module PState = PState From 35fb9c83879ecf8f8491137e9df8c167980661c1 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 8 Nov 2025 15:36:08 +0000 Subject: [PATCH 09/29] more type re-org Signed-off-by: Sacha Ayoun --- GillianCore/engine/Abstraction/PState.ml | 13 ++++++++++--- GillianCore/engine/Abstraction/PState.mli | 13 ++++++++++--- GillianCore/engine/Abstraction/Verifier.ml | 9 +++------ GillianCore/engine/Abstraction/Verifier.mli | 10 +++------- GillianCore/lib/gillian.ml | 3 +++ 5 files changed, 29 insertions(+), 19 deletions(-) diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml index 22dce031d..cb2e5522c 100644 --- a/GillianCore/engine/Abstraction/PState.ml +++ b/GillianCore/engine/Abstraction/PState.ml @@ -1,12 +1,19 @@ (** Interface for GIL Predicate States. They are considered to be mutable. *) module type S = sig - include SState.S - type state_t - type abs_t = string * vt list + type abs_t = string * SVal.M.t list module SMatcher : Matcher.S with type state_t = state_t + type t = SMatcher.t = { + state : state_t; + preds : Preds.t; + wands : Wands.t; + pred_defs : MP.preds_tbl_t; + } + + include SState.S with type t := t + val make_p : preds:MP.preds_tbl_t -> init_data:init_data -> diff --git a/GillianCore/engine/Abstraction/PState.mli b/GillianCore/engine/Abstraction/PState.mli index 9d9e3e35f..fe289d862 100644 --- a/GillianCore/engine/Abstraction/PState.mli +++ b/GillianCore/engine/Abstraction/PState.mli @@ -1,12 +1,19 @@ (** Interface for GIL General States. They are considered to be mutable. *) module type S = sig - include SState.S - type state_t - type abs_t = string * vt list + type abs_t = string * SVal.M.t list module SMatcher : Matcher.S with type state_t = state_t + type t = SMatcher.t = { + state : state_t; + preds : Preds.t; + wands : Wands.t; + pred_defs : MP.preds_tbl_t; + } + + include SState.S with type t := t + val make_p : preds:MP.preds_tbl_t -> init_data:init_data -> diff --git a/GillianCore/engine/Abstraction/Verifier.ml b/GillianCore/engine/Abstraction/Verifier.ml index aa403e468..44cfc6fa1 100644 --- a/GillianCore/engine/Abstraction/Verifier.ml +++ b/GillianCore/engine/Abstraction/Verifier.ml @@ -4,15 +4,12 @@ module DL = Debugger_log module type S = sig type heap_t - type state type m_err type annot - module SPState : - PState.S - with type t = state - and type heap_t = heap_t - and type m_err_t = m_err + module SPState : PState.S with type heap_t = heap_t and type m_err_t = m_err + + type state = SPState.t module SState : SState.S with type t = SPState.state_t and type heap_t = heap_t diff --git a/GillianCore/engine/Abstraction/Verifier.mli b/GillianCore/engine/Abstraction/Verifier.mli index b16073d02..06375d53c 100644 --- a/GillianCore/engine/Abstraction/Verifier.mli +++ b/GillianCore/engine/Abstraction/Verifier.mli @@ -1,14 +1,11 @@ module type S = sig type heap_t - type state type m_err type annot - module SPState : - PState.S - with type t = state - and type heap_t = heap_t - and type m_err_t = m_err + module SPState : PState.S with type heap_t = heap_t and type m_err_t = m_err + + type state = SPState.t module SState : SState.S with type t = SPState.state_t and type heap_t = heap_t @@ -71,7 +68,6 @@ module Make S with type heap_t = SPState.heap_t and type m_err = SPState.m_err_t - and type state = SPState.t and module SPState = SPState and module SState = SState and type annot = PC.Annot.t diff --git a/GillianCore/lib/gillian.ml b/GillianCore/lib/gillian.ml index 57eec9e66..42ab1b176 100644 --- a/GillianCore/lib/gillian.ml +++ b/GillianCore/lib/gillian.ml @@ -57,8 +57,11 @@ end module Abstraction = struct module MP = Engine.MP module Verifier = Engine.Verifier + module Normaliser = Engine.Normaliser end +module Abductor = Engine.Abductor + (* module Test262 = Test262_main *) (** Modules for logging (to the file log and the report database) *) From a5a44c0608e54ad8fd04af90e3120c4d76a050b9 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 8 Nov 2025 16:15:46 +0000 Subject: [PATCH 10/29] exposing even more constructors Signed-off-by: Sacha Ayoun --- GillianCore/engine/Abstraction/PState.ml | 26 +++++++++++++++++++ GillianCore/engine/Abstraction/PState.mli | 11 ++++++++ .../engine/symbolic_semantics/SState.ml | 16 ++++++++++++ .../engine/symbolic_semantics/SState.mli | 8 ++++++ 4 files changed, 61 insertions(+) diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml index cb2e5522c..8dce37f09 100644 --- a/GillianCore/engine/Abstraction/PState.ml +++ b/GillianCore/engine/Abstraction/PState.ml @@ -24,6 +24,17 @@ module type S = sig unit -> t + val make_p_from_heap : + pred_defs:MP.preds_tbl_t -> + store:store_t -> + heap:heap_t -> + spec_vars:SS.t -> + wands:Wands.t -> + preds:Preds.t -> + pfs:PFS.t -> + gamma:Type_env.t -> + t + val init_with_pred_table : MP.preds_tbl_t -> init_data -> t (** Get preds of given symbolic state *) @@ -122,6 +133,21 @@ module Make (State : SState.S) : let state = State.make_s ~init_data ~store ~pfs ~gamma ~spec_vars in { state; preds = Preds.init []; wands = Wands.init []; pred_defs = preds } + let make_s_from_heap ~heap:_ ~store:_ ~pfs:_ ~gamma:_ ~spec_vars:_ = + failwith "Calling make_s_from_heap on SState" + + let make_p_from_heap + ~pred_defs + ~store + ~heap + ~spec_vars + ~wands + ~preds + ~pfs + ~gamma = + let sstate = State.make_s_from_heap ~store ~heap ~spec_vars ~pfs ~gamma in + { state = sstate; preds; wands; pred_defs } + let make_s ~init_data:_ ~store:_ ~pfs:_ ~gamma:_ ~spec_vars:_ : t = failwith "Calling make_s on a PState" diff --git a/GillianCore/engine/Abstraction/PState.mli b/GillianCore/engine/Abstraction/PState.mli index fe289d862..69a6a2b0a 100644 --- a/GillianCore/engine/Abstraction/PState.mli +++ b/GillianCore/engine/Abstraction/PState.mli @@ -24,6 +24,17 @@ module type S = sig unit -> t + val make_p_from_heap : + pred_defs:MP.preds_tbl_t -> + store:store_t -> + heap:heap_t -> + spec_vars:SS.t -> + wands:Wands.t -> + preds:Preds.t -> + pfs:PFS.t -> + gamma:Type_env.t -> + t + val init_with_pred_table : MP.preds_tbl_t -> init_data -> t (** Get preds of given symbolic state *) diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml index f06375b06..e4c69ad75 100644 --- a/GillianCore/engine/symbolic_semantics/SState.ml +++ b/GillianCore/engine/symbolic_semantics/SState.ml @@ -18,6 +18,14 @@ module type S = sig spec_vars:SS.t -> t + val make_s_from_heap : + heap:heap_t -> + store:store_t -> + pfs:PFS.t -> + gamma:Type_env.t -> + spec_vars:SS.t -> + t + val init : init_data -> t val get_init_data : t -> init_data val clear_resource : t -> t @@ -56,6 +64,14 @@ module Make (SMemory : SMemory.S) : type err_t = (m_err_t, vt) StateErr.t [@@deriving yojson, show] type action_ret = (t * vt list, err_t) result list + let make_s_from_heap + ~(heap : heap_t) + ~(store : store_t) + ~(pfs : PFS.t) + ~(gamma : Type_env.t) + ~(spec_vars : SS.t) : t = + { heap; store; pfs; gamma; spec_vars } + exception Internal_State_Error of err_t list * t module ES = Expr.Set diff --git a/GillianCore/engine/symbolic_semantics/SState.mli b/GillianCore/engine/symbolic_semantics/SState.mli index bbfbc6e82..0b7b1fa8d 100644 --- a/GillianCore/engine/symbolic_semantics/SState.mli +++ b/GillianCore/engine/symbolic_semantics/SState.mli @@ -13,6 +13,14 @@ module type S = sig spec_vars:SS.t -> t + val make_s_from_heap : + heap:heap_t -> + store:store_t -> + pfs:PFS.t -> + gamma:Type_env.t -> + spec_vars:SS.t -> + t + val init : init_data -> t val get_init_data : t -> init_data val clear_resource : t -> t From bcc2ca0969309f3403c9a7b270a2b54df518e4e4 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 8 Nov 2025 16:22:07 +0000 Subject: [PATCH 11/29] MORE FUNCTIONS Signed-off-by: Sacha Ayoun --- GillianCore/engine/Abstraction/PState.ml | 3 +++ GillianCore/engine/Abstraction/PState.mli | 2 ++ 2 files changed, 5 insertions(+) diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml index 8dce37f09..338698bcc 100644 --- a/GillianCore/engine/Abstraction/PState.ml +++ b/GillianCore/engine/Abstraction/PState.ml @@ -40,6 +40,8 @@ module type S = sig (** Get preds of given symbolic state *) val get_preds : t -> Preds.t + val get_wands : t -> Wands.t + (** Set preds of given symbolic state *) val set_preds : t -> Preds.t -> t @@ -179,6 +181,7 @@ module Make (State : SState.S) : let get_preds (astate : t) : Preds.t = astate.preds let set_preds (astate : t) (preds : Preds.t) : t = { astate with preds } let set_wands astate wands = { astate with wands } + let get_wands (astate : t) : Wands.t = astate.wands let assume ?(unfold = false) (astate : t) (v : Expr.t) : t list = let open Syntaxes.List in diff --git a/GillianCore/engine/Abstraction/PState.mli b/GillianCore/engine/Abstraction/PState.mli index 69a6a2b0a..16c7f04ef 100644 --- a/GillianCore/engine/Abstraction/PState.mli +++ b/GillianCore/engine/Abstraction/PState.mli @@ -43,6 +43,8 @@ module type S = sig (** Set preds of given symbolic state *) val set_preds : t -> Preds.t -> t + val get_wands : t -> Wands.t + (** Set wands of given symbolic state *) val set_wands : t -> Wands.t -> t From 47ae9a011eb889148e7026aad1f00257d14083f4 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 8 Nov 2025 16:38:01 +0000 Subject: [PATCH 12/29] urgh Signed-off-by: Sacha Ayoun --- GillianCore/engine/Abstraction/PState.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml index 338698bcc..b97a40623 100644 --- a/GillianCore/engine/Abstraction/PState.ml +++ b/GillianCore/engine/Abstraction/PState.ml @@ -40,11 +40,11 @@ module type S = sig (** Get preds of given symbolic state *) val get_preds : t -> Preds.t - val get_wands : t -> Wands.t - (** Set preds of given symbolic state *) val set_preds : t -> Preds.t -> t + val get_wands : t -> Wands.t + (** Set preds of given symbolic state *) val set_wands : t -> Wands.t -> t From bf378a2662b58944f7f66699977b74e9685aef79 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 8 Nov 2025 16:38:37 +0000 Subject: [PATCH 13/29] okkkk Signed-off-by: Sacha Ayoun --- GillianCore/engine/BiAbduction/Abductor.ml | 583 +++++++++++++++++++- transformers/lib/bi_abduction/abductor.ml | 105 ++++ transformers/lib/bi_abduction/dune | 4 + transformers/lib/dune | 2 - transformers/lib/states/MyMonadicSMemory.ml | 4 +- 5 files changed, 687 insertions(+), 11 deletions(-) create mode 100644 transformers/lib/bi_abduction/abductor.ml create mode 100644 transformers/lib/bi_abduction/dune delete mode 100644 transformers/lib/dune diff --git a/GillianCore/engine/BiAbduction/Abductor.ml b/GillianCore/engine/BiAbduction/Abductor.ml index 6c66424f2..dd6b9e093 100644 --- a/GillianCore/engine/BiAbduction/Abductor.ml +++ b/GillianCore/engine/BiAbduction/Abductor.ml @@ -13,7 +13,417 @@ module type S = sig unit end -module Make +module type SimplifiedSState = + State.S + with type vt = SVal.M.t + and type st = SVal.SESubst.t + and type store_t = SStore.t + +module type BiProcessingS = sig + type annot + type init_data + type state_t + + (** Similar to Normaliser.normalise_assertion but all failed normalisations + are discarded, and it produces something of the adapted state type *) + val normalise_assertion : + init_data:init_data -> + prog:'a MP.prog -> + pvars:SS.t -> + Asrt.t -> + state_t list + + val make_spec : + string -> string list -> state_t -> state_t -> Flag.t -> Spec.t option +end + +(* A bit of hack around as the legacy hardcoded BiState and the new, + simpler, BiAbd combinator approach expose different state types. + We try to aggregate the logic of creating specs and running tests in a single module. *) +module Make_raw + (PC : ParserAndCompiler.S) + (State : SimplifiedSState) + (BiProcess : + BiProcessingS + with type state_t = State.t + and type init_data = State.init_data) + (External : External.T(PC.Annot).S) = +struct + module L = Logging + module SSubst = SVal.SESubst + + module Interp = + G_interpreter.Make (SVal.M) (SVal.SESubst) (SStore) (State) (PC) (External) + (* module Normaliser = Normaliser.Make (SPState) *) + + type state_t = Interp.state_t + type result_t = Interp.result_t + type t = { name : string; params : string list; state : state_t } + type annot = PC.Annot.t + type init_data = PC.init_data + + let testify ~init_data ~(prog : annot MP.prog) (bi_spec : BiSpec.t) : t list = + let open Syntaxes.List in + L.verbose (fun m -> m "Bi-testifying: %s" bi_spec.bispec_name); + let params = SS.of_list bi_spec.bispec_params in + (* For each pre in the bispec *) + let* pre, _ = bi_spec.bispec_pres in + let+ state = + BiProcess.normalise_assertion ~init_data ~pvars:params ~prog pre + in + { name = bi_spec.bispec_name; params = bi_spec.bispec_params; state } + + let run_test + (ret_fun : result_t -> (Spec.t * Flag.t) option) + (prog : annot MP.prog) + (test : t) : (Spec.t * Flag.t) list = + let state = State.copy test.state in + let state = State.add_spec_vars state (State.get_lvars state) in + try + let opt_results = + Interp.evaluate_proc ret_fun prog test.name test.params state + in + let count = ref 0 in + let result = + List.filter_map + (function + | None -> + incr count; + None + | x -> x) + opt_results + in + if !count > 0 then + L.verbose (fun m -> + m "WARNING: %d vanished while creating the for %s!" !count test.name); + result + with Failure msg -> + L.print_to_all + (Printf.sprintf "ERROR in proc %s with message:\n%s\n" test.name msg); + [] + + let process_sym_exec_result + (prog : annot MP.prog) + (name : string) + (params : string list) + (state_i : state_t) + (result : result_t) : (Spec.t * Flag.t) option = + let open Syntaxes.Option in + let process_spec = BiProcess.make_spec in + let state_i = State.copy state_i in + let add_spec spec = + try MP.add_spec prog spec + with _ -> + L.fail + (Format.asprintf "When trying to build an MP for %s, I died!" name) + in + match result with + | RFail { error_state; _ } -> + (* let rec find_error_state (aux : Interp.err_t list) = + match aux with + | [] -> error_state + | e :: errs -> ( + match e with + | EState (EMem (s, _)) -> s + | _ -> find_error_state errs) + in + let error_state = find_error_state errors in *) + let+ spec = process_spec name params state_i error_state Flag.Bug in + add_spec spec; + (spec, Flag.Bug) + | RSucc { flag; final_state; _ } -> + let+ spec = process_spec name params state_i final_state flag in + add_spec spec; + (spec, flag) + + type proc_stats = { + gil_size : int; + mutable tests : int; + mutable succs : int; + mutable bugs : int; + mutable time : float; + } + + let pp_proc_stats fmt { gil_size; tests; succs; bugs; time } = + Fmt.pf fmt "%d, %d, %d, %d, %f" gil_size tests succs bugs time + + let run_tests (prog : annot MP.prog) (tests : t list) = + let num_tests = List.length tests in + Fmt.pr "Running tests on %d procs.\n@?" num_tests; + + let stats : (string * proc_stats) list ref = ref [] in + let get_stats name get_gil_size = + match List.assoc_opt name !stats with + | Some s -> s + | None -> + let gil_size = get_gil_size () in + let s = { gil_size; tests = 0; succs = 0; bugs = 0; time = 0.0 } in + stats := (name, s) :: !stats; + s + in + + let rec run_tests_aux tests succ_specs err_specs bug_specs i = + match tests with + | [] -> (succ_specs, err_specs, bug_specs) + | test :: rest -> + let rec part3 = function + | [] -> ([], [], []) + | (spec, flag) :: rest -> ( + let succ_specs, err_specs, bug_specs = part3 rest in + match flag with + | Flag.Normal -> (spec :: succ_specs, err_specs, bug_specs) + | Flag.Error -> (succ_specs, spec :: err_specs, bug_specs) + | Flag.Bug -> (succ_specs, err_specs, spec :: bug_specs)) + in + L.verbose (fun m -> m "Running bi-abduction on %s\n" test.name); + Fmt.pr "Testing %s... @?" test.name; + let start_time = Sys.time () in + let rets = + run_test + (process_sym_exec_result prog test.name test.params test.state) + prog test + in + let end_time = Sys.time () in + let stats = + get_stats test.name (fun () -> + match Hashtbl.find_opt prog.prog.procs test.name with + | None -> -1 + | Some prog -> Array.length prog.proc_body) + in + let cur_succ_specs, cur_err_specs, cur_bug_specs = part3 rets in + let new_succ_specs = succ_specs @ cur_succ_specs in + let new_err_specs = err_specs @ cur_err_specs in + let new_bug_specs = bug_specs @ cur_bug_specs in + + stats.tests <- stats.tests + 1; + stats.succs <- stats.succs + List.length cur_succ_specs; + stats.bugs <- stats.bugs + List.length cur_bug_specs; + stats.time <- stats.time +. (end_time -. start_time); + Fmt.pr "%dS %dB (%d/%d)\n@?" + (List.length cur_succ_specs) + (List.length cur_bug_specs) + i num_tests; + + run_tests_aux rest new_succ_specs new_err_specs new_bug_specs (i + 1) + in + let result = run_tests_aux tests [] [] [] 1 in + Fmt.pr "\nTest results:\nProc, GIL Commands, Tests, Succs, Bugs, Time\n"; + !stats + |> List.sort (fun (name1, _) (name2, _) -> String.compare name1 name2) + |> List.iter (fun (name, stats) -> + Fmt.pr "%s, %a\n" name pp_proc_stats stats); + Fmt.pr "@?"; + result + + let get_test_results + (prog : annot MP.prog) + (succ_specs : Spec.t list) + (error_specs : Spec.t list) + (bug_specs : Spec.t list) = + let sort_specs = + List.sort + (fun Spec.{ spec_name = name1; _ } Spec.{ spec_name = name2; _ } -> + String.compare name1 name2) + in + let bug_specs_txt = + Format.asprintf "@[BUG SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs bug_specs) + in + let error_specs_txt = + Format.asprintf "@[ERROR SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs error_specs) + in + let normal_specs_txt = + Format.asprintf "@[SUCCESSFUL SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs succ_specs) + in + + if !Config.specs_to_stdout then ( + L.print_to_all bug_specs_txt; + L.print_to_all error_specs_txt; + L.print_to_all normal_specs_txt) + else ( + L.normal (fun m -> m "%s" bug_specs_txt); + L.normal (fun m -> m "%s" error_specs_txt); + L.normal (fun m -> m "%s" normal_specs_txt)); + + (* This is a hack to not count auxiliary functions that are bi-abduced *) + let len_succ = List.length succ_specs in + let auxiliaries = + List.fold_left + (fun ac (spec : Spec.t) -> + ac || String.equal spec.spec_name "assumeType") + false succ_specs + in + let offset = if auxiliaries then 12 else 0 in + let len_succ = len_succ - offset in + let () = + L.print_to_all + (Printf.sprintf "SUCCESS SPECS: %d\nERROR SPECS: %d\nBUG SPECS: %d" + len_succ (List.length error_specs) (List.length bug_specs)) + in + let results = BiAbductionResults.make () in + let () = + List.iter + (fun (spec : Spec.t) -> + BiAbductionResults.set_spec results spec.spec_name spec) + (Prog.get_specs prog.prog) + in + results + + let str_concat = String.concat ", " + + let sort_tests_by_callgraph tests callgraph = + let rec aux acc rest_tests = function + | [] -> (acc, rest_tests) + | name :: rest -> + let selected_tests, rest_tests = + List.partition (fun t -> t.name = name) rest_tests + in + aux (acc @ selected_tests) rest_tests rest + in + let callgraph_order = Call_graph.get_sorted_names callgraph in + let sorted_tests, rest_tests = aux [] tests callgraph_order in + let rest_sorted_tests = + rest_tests |> List.sort (fun t1 t2 -> Stdlib.compare t1.name t2.name) + in + sorted_tests @ rest_sorted_tests + + let test_procs ~init_data ~call_graph (prog : annot MP.prog) = + L.verbose (fun m -> m "Starting bi-abductive testing in normal mode"); + let proc_names = Prog.get_noninternal_proc_names prog.prog in + L.verbose (fun m -> m "Proc names: %s" (str_concat proc_names)); + let bi_specs = List.map (Prog.get_bispec_exn prog.prog) proc_names in + + let tests = List.concat_map (testify ~init_data ~prog) bi_specs in + let test_names tests = str_concat (List.map (fun t -> t.name) tests) in + L.verbose (fun m -> m "I have tests for: %s" (test_names tests)); + let tests = sort_tests_by_callgraph tests call_graph in + L.verbose (fun m -> m "I have tests for: %s" (test_names tests)); + let succ_specs, err_specs, bug_specs = run_tests prog tests in + get_test_results prog succ_specs err_specs bug_specs + + let specs_equal (spec_a : Spec.t) (spec_b : Spec.t) = + (* FIXME: Perform a more robust comparsion based on matching *) + String.equal (Spec.hash_of_t spec_a) (Spec.hash_of_t spec_b) + + let test_procs_incrementally + (prog : annot MP.prog) + ~(init_data : State.init_data) + ~(prev_results : BiAbductionResults.t) + ~(reverse_graph : Call_graph.t) + ~(changed_procs : string list) + ~(to_test : string list) = + L.verbose (fun m -> m "Starting bi-abductive testing in incremental mode"); + let to_test_set = SS.of_list to_test in + let filter spec_name = not (SS.mem spec_name to_test_set) in + let prev_specs = BiAbductionResults.get_all_specs ~filter prev_results in + let prev_spec_names = + str_concat (List.map (fun (s : Spec.t) -> s.spec_name) prev_specs) + in + L.verbose (fun m -> m "I will use the stored specs of: %s" prev_spec_names); + List.iter (fun spec -> MP.add_spec prog spec) prev_specs; + + let rec test_procs_aux to_test checked succ_specs error_specs bug_specs = + (* FIXME: Keep tests in a heap/priority queue *) + match to_test with + | [] -> (succ_specs, error_specs, bug_specs) + | proc_name :: rest -> + let () = MP.remove_spec prog proc_name in + let tests = + testify ~init_data ~prog (Prog.get_bispec_exn prog.prog proc_name) + in + let cur_succ_specs, cur_err_specs, cur_bug_specs = + run_tests prog tests + in + let checked = SS.add proc_name checked in + let new_to_test = + if BiAbductionResults.contains_spec prev_results proc_name then + let prev_spec = + BiAbductionResults.get_spec_exn prev_results proc_name + in + let new_spec = (Hashtbl.find prog.specs proc_name).data in + if not (specs_equal prev_spec new_spec) then ( + L.verbose (fun m -> m "The spec of %s has changed" proc_name); + (* Must also check immediate callers *) + let callers = + ChangeTracker.get_callers prog.prog ~reverse_graph + ~excluded_procs:changed_procs ~proc_name + in + let callers = + List.filter (fun name -> not (SS.mem name checked)) callers + in + L.verbose (fun m -> + m "I will check its callers: %s" (str_concat callers)); + List.sort Stdlib.compare (rest @ callers)) + else ( + L.verbose (fun m -> m "The spec of %s is unchanged" proc_name); + rest) + else rest + in + let new_succ_specs = succ_specs @ cur_succ_specs in + let new_err_specs = error_specs @ cur_err_specs in + let new_bug_specs = bug_specs @ cur_bug_specs in + test_procs_aux new_to_test checked new_succ_specs new_err_specs + new_bug_specs + in + (* Keep list sorted to ensure tests are executed in the required order *) + let to_test = List.sort Stdlib.compare to_test in + L.verbose (fun m -> m "I will begin by checking: %s" (str_concat to_test)); + let succ_specs, error_specs, bug_specs = + test_procs_aux to_test SS.empty [] [] [] + in + get_test_results prog succ_specs error_specs bug_specs + + let test_prog + ~init_data + ?(call_graph = Call_graph.make ()) + (prog : annot MP.prog) + (incremental : bool) + (source_files : SourceFiles.t option) : unit = + let open ResultsDir in + let open ChangeTracker in + if incremental && prev_results_exist () then + (* Only test changed procedures *) + let cur_source_files = + match source_files with + | Some files -> files + | None -> failwith "Cannot use -a in incremental mode" + in + let prev_source_files, prev_call_graph, prev_results = + read_biabduction_results () + in + let proc_changes = + get_changes prog.prog ~prev_source_files ~prev_call_graph + ~cur_source_files + in + let to_test = proc_changes.changed_procs @ proc_changes.new_procs in + let to_prune = proc_changes.changed_procs @ proc_changes.deleted_procs in + let reverse_graph = Call_graph.to_reverse_graph prev_call_graph in + let cur_results = + test_procs_incrementally prog ~init_data ~prev_results ~reverse_graph + ~changed_procs:proc_changes.changed_procs ~to_test + in + let cur_call_graph = Interp.call_graph in + let () = Call_graph.prune_procs prev_call_graph to_prune in + let call_graph = Call_graph.merge prev_call_graph cur_call_graph in + let results = BiAbductionResults.merge prev_results cur_results in + let diff = Fmt.str "%a" ChangeTracker.pp_proc_changes proc_changes in + write_biabduction_results cur_source_files call_graph ~diff results + else + (* Test all procedures *) + let cur_source_files = + Option.value ~default:(SourceFiles.make ()) source_files + in + let dyn_call_graph = Interp.call_graph in + let results = test_procs ~init_data ~call_graph prog in + write_biabduction_results cur_source_files dyn_call_graph ~diff:"" results +end + +(* module Make (SPState : PState.S) (PC : ParserAndCompiler.S with type init_data = SPState.init_data) (External : External.T(PC.Annot).S) : @@ -54,7 +464,6 @@ module Make SSubst.init bindings' let make_spec - (_ : annot MP.prog) (name : string) (params : string list) (bi_state_i : bi_state_t) @@ -160,7 +569,6 @@ module Make let testify ~init_data ~(prog : annot MP.prog) (bi_spec : BiSpec.t) : t list = L.verbose (fun m -> m "Bi-testifying: %s" bi_spec.bispec_name); - let proc_names = Prog.get_proc_names prog.prog in let params = SS.of_list bi_spec.bispec_params in let normalise = Normaliser.normalise_assertion ~init_data ~pred_defs:prog.preds @@ -175,9 +583,7 @@ module Make { name = bi_spec.bispec_name; params = bi_spec.bispec_params; - state = - SBAState.make ~procs:(SS.of_list proc_names) ~state:ss_pre - ~init_data; + state = SBAState.make ~state:ss_pre ~init_data; }) l in @@ -219,7 +625,7 @@ module Make (state_i : bi_state_t) (result : result_t) : (Spec.t * Flag.t) option = let open Syntaxes.Option in - let process_spec = make_spec prog in + let process_spec = make_spec in let state_i = SBAState.copy state_i in let add_spec spec = try MP.add_spec prog spec @@ -536,6 +942,169 @@ module Make let dyn_call_graph = SBAInterpreter.call_graph in let results = test_procs ~init_data ~call_graph prog in write_biabduction_results cur_source_files dyn_call_graph ~diff:"" results +end *) + +module Make + (SPState : PState.S) + (PC : ParserAndCompiler.S with type init_data = SPState.init_data) + (External : External.T(PC.Annot).S) : + S with type annot = PC.Annot.t and type init_data = PC.init_data = struct + module Pre_constructions = struct + module Normaliser = Normaliser.Make (SPState) + module SBAState = BiState.Make (SPState) + module SSubst = SVal.SESubst + module L = Logging + + module BiProcess = struct + type state_t = SBAState.t + type init_data = SBAState.init_data + type annot = PC.Annot.t + + let normalise_assertion + ~(init_data : init_data) + ~(prog : 'a MP.prog) + ~(pvars : SS.t) + assertion = + let open Syntaxes.List in + let+ ss_pre, _ = + match + Normaliser.normalise_assertion ~pred_defs:prog.preds ~init_data + ~pvars assertion + with + | Ok l -> l + | Error _ -> [] + in + SBAState.make ~state:ss_pre ~init_data + + let make_id_subst (a : Asrt.t) : SSubst.t = + let lvars = Asrt.lvars a in + let alocs = Asrt.alocs a in + let lvar_bindings = + List.map (fun x -> (Expr.LVar x, Expr.LVar x)) (SS.elements lvars) + in + let aloc_bindings = + List.map (fun x -> (Expr.LVar x, Expr.ALoc x)) (SS.elements alocs) + in + let bindings = lvar_bindings @ aloc_bindings in + let bindings' = + List.map + (fun (x, e) -> + match SVal.M.from_expr e with + | Some v -> (x, v) + | _ -> raise (Failure "DEATH. make_id_subst")) + bindings + in + SSubst.init bindings' + + let make_spec + (name : string) + (params : string list) + (bi_state_i : state_t) + (bi_state_f : state_t) + (fl : Flag.t) : Spec.t option = + let open Syntaxes.List in + let sspecs = + (* let start_time = time() in *) + + (* HMMMMM *) + (* let _ = SBAState.simplify ~kill_new_lvars:true bi_state_f in *) + let state_i, _ = SBAState.get_components bi_state_i in + let state_f, state_af = SBAState.get_components bi_state_f in + let pvars = SS.of_list (Names.return_variable :: params) in + + L.verbose (fun m -> + m + "Going to create a spec for @[%s(%a)@]\n\ + @[AF:@\n\ + %a@]@\n\ + @[Final STATE:@\n\ + %a@]" + name + Fmt.(list ~sep:comma string) + params SPState.pp state_af SPState.pp state_f); + (* Drop all pvars except ret/err from the state *) + let () = + SStore.filter_map_inplace (SPState.get_store state_f) (fun x v -> + if x = Names.return_variable then Some v else None) + in + let* post = + let _, finals_simplified = + SPState.simplify ~kill_new_lvars:true state_f + in + let+ final_simplified = finals_simplified in + List.sort Asrt.compare + (SPState.to_assertions ~to_keep:pvars final_simplified) + in + + let+ pre = + let af_asrt = SPState.to_assertions state_af in + let af_subst = make_id_subst af_asrt in + let* af_produce_res = SPState.produce state_i af_subst af_asrt in + match af_produce_res with + | Ok state_i' -> + let _, simplifieds = + SPState.simplify ~kill_new_lvars:true state_i' + in + let+ simplified = simplifieds in + List.sort Asrt.compare + (SPState.to_assertions ~to_keep:pvars simplified) + | Error _ -> + L.verbose (fun m -> m "Failed to produce anti-frame"); + [] + in + let post_clocs = Asrt.clocs post in + let pre_clocs = Asrt.clocs pre in + let new_clocs = SS.diff post_clocs pre_clocs in + let subst = Hashtbl.create Config.medium_tbl_size in + List.iter + (fun cloc -> Hashtbl.replace subst cloc (Expr.ALoc (ALoc.alloc ()))) + (SS.elements new_clocs); + let subst_fun cloc = + match Hashtbl.find_opt subst cloc with + | Some e -> e + | None -> Lit (Loc cloc) + in + let new_post = Asrt.subst_clocs subst_fun post in + Spec. + { + ss_pre = (pre, None); + ss_posts = [ (new_post, None) ]; + ss_variant = None; + ss_flag = fl; + ss_to_verify = false; + ss_label = None; + } + in + match sspecs with + | [] -> None + | sspecs -> + let spec = + Spec. + { + spec_name = name; + spec_params = params; + spec_sspecs = sspecs; + spec_normalised = true; + spec_incomplete = true; + spec_to_verify = false; + spec_location = None; + } + in + L.verbose (fun m -> + m + "@[Created a spec for @[%s(%a)@] successfully. Here \ + is the spec:@\n\ + %a@]" + name + Fmt.(list ~sep:comma string) + params Spec.pp spec); + Some spec + end + end + + include + Make_raw (PC) (Pre_constructions.SBAState) (Pre_constructions.BiProcess) + (External) end module From_scratch diff --git a/transformers/lib/bi_abduction/abductor.ml b/transformers/lib/bi_abduction/abductor.ml new file mode 100644 index 000000000..cef3af5b2 --- /dev/null +++ b/transformers/lib/bi_abduction/abductor.ml @@ -0,0 +1,105 @@ +open Gillian +open Gillian.Symbolic +open Gillian.General +open Gillian.Gil_syntax +open Utils.Containers +module MP = Gillian.Abstraction.MP +module L = Gillian.Logging + +(** This functor expects to receive a symbolic memory that was *not* transformed + through the Bi_abd combinator. *) +module Make + (SMemory : States.MyMonadicSMemory.S) + (Init_data : States.MyMonadicSMemory.ID) + (PC : ParserAndCompiler.S with type init_data = Init_data.t) + (External : External.T(PC.Annot).S) = +struct + (* We first construct memory that performs bi-abduction *) + module BiMemory = States.Bi_abd.Make (SMemory) + + (* We lift to legacy memory signature *) + module BiMemoryMonadicLegacy = + States.MyMonadicSMemory.Make (BiMemory) (Init_data) + + module BiMemoryLegacy = Monadic.MonadicSMemory.Lift (BiMemoryMonadicLegacy) + + (* We lift it to Gillian states *) + module BiSState = SState.Make (BiMemoryLegacy) + module SPState = PState.Make (BiSState) + module NonBiMemory = States.MyMonadicSMemory.Make (SMemory) (Init_data) + module NonBiMemoryLegacy = Monadic.MonadicSMemory.Lift (NonBiMemory) + module NonBiSState = SState.Make (NonBiMemoryLegacy) + module NonBiSPState = PState.Make (NonBiSState) + + (* We define a helper to run functions under bi-abduction *) + + module Normaliser = Abstraction.Normaliser.Make (SPState) + + (* We can now use the standard Abductor loop + (which iterates over the functions of the program to generate specifications). + *) + + module BiProcess = struct + type annot = PC.Annot.t + type state_t = SPState.t + type init_data = Init_data.t + + let normalise_assertion ~init_data ~prog ~pvars assertion = + match + Normaliser.normalise_assertion ~init_data ~pred_defs:prog.MP.preds + ~pvars assertion + with + | Ok l -> List.map fst l + | Error _ -> [] + + let make_spec + name + params + (_initial_state : state_t) + (final_state : state_t) + fl = + let pvars = SS.of_list (Utils.Names.return_variable :: params) in + let States.Bi_abd.{ anti_frame = _; state } = + SPState.get_heap final_state + in + let final_state = + NonBiSPState.make_p_from_heap ~pred_defs:final_state.pred_defs + ~store:(SPState.get_store final_state) + ~heap:state + ~pfs:(SPState.get_pfs final_state) + ~gamma:(SPState.get_typ_env final_state) + ~spec_vars:(SPState.get_spec_vars final_state) + ~wands:(SPState.get_wands final_state) + ~preds:(SPState.get_preds final_state) + in + let post = NonBiSPState.to_assertions ~to_keep:pvars final_state in + let pre = [ Asrt.Emp ] in + let sspec = + Spec. + { + ss_pre = (pre, None); + ss_posts = [ (post, None) ]; + ss_variant = None; + ss_flag = fl; + ss_label = None; + ss_to_verify = false; + } + in + let spec = + Spec. + { + spec_name = name; + spec_params = params; + spec_sspecs = [ sspec ]; + spec_normalised = true; + spec_incomplete = true; + spec_to_verify = false; + spec_location = None; + } + in + Some spec + (* So first we need to extract a state that corresponds to the *) + end + + module Abductor = Abductor.Make_raw (PC) (SPState) (BiProcess) (External) +end diff --git a/transformers/lib/bi_abduction/dune b/transformers/lib/bi_abduction/dune new file mode 100644 index 000000000..0e23e1e5a --- /dev/null +++ b/transformers/lib/bi_abduction/dune @@ -0,0 +1,4 @@ +(library + (name transformers_abductor) + (public_name transformers.abductor) + (libraries gillian states)) diff --git a/transformers/lib/dune b/transformers/lib/dune deleted file mode 100644 index ed98c29bf..000000000 --- a/transformers/lib/dune +++ /dev/null @@ -1,2 +0,0 @@ -(library - (name transformers_lib)) diff --git a/transformers/lib/states/MyMonadicSMemory.ml b/transformers/lib/states/MyMonadicSMemory.ml index acd3bba27..9bb505783 100644 --- a/transformers/lib/states/MyMonadicSMemory.ml +++ b/transformers/lib/states/MyMonadicSMemory.ml @@ -129,8 +129,8 @@ end (** Functor to convert composable, typed state models into Gillian monadic state models *) -module Make (Mem : S) (ID : ID) : MonadicSMemory.S with type init_data = ID.t = -struct +module Make (Mem : S) (ID : ID) : + MonadicSMemory.S with type init_data = ID.t and type t = Mem.t = struct include Mem include Defaults From 80b3119ccff21fb6712f32d58a0ad6983be88723 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 8 Nov 2025 16:41:41 +0000 Subject: [PATCH 14/29] minor merge conflict Signed-off-by: Sacha Ayoun --- transformers/lib/states/Fractional.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/transformers/lib/states/Fractional.ml b/transformers/lib/states/Fractional.ml index db0a02aee..43800a2f6 100644 --- a/transformers/lib/states/Fractional.ml +++ b/transformers/lib/states/Fractional.ml @@ -13,7 +13,7 @@ type t = (Expr.t * Expr.t) option [@@deriving show, yojson] type err_t = MissingState | NotEnoughPermission [@@deriving show, yojson] type action = Load | Store -type pred = Frac +type pred = Frac [@@deriving yojson] let action_from_str = function | "load" -> Some Load From 89df3b34af12a09bed221edacc46e2fe08dedeaf Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 8 Nov 2025 17:05:20 +0000 Subject: [PATCH 15/29] IT COMPILES AND RUNS Signed-off-by: Sacha Ayoun --- GillianCore/command_line/command_line.ml | 1 + GillianCore/command_line/command_line.mli | 9 +++++++++ GillianCore/engine/BiAbduction/Abductor.ml | 2 +- transformers/bin/c_bi_abd.ml | 13 +++++++++++++ transformers/bin/dune | 5 +++-- transformers/lib/bi_abduction/abductor.ml | 21 ++++++++++++++++++--- transformers/lib/prebuilt/C.ml | 2 +- transformers/lib/states/MyMonadicSMemory.ml | 4 ++-- 8 files changed, 48 insertions(+), 9 deletions(-) create mode 100644 transformers/bin/c_bi_abd.ml diff --git a/GillianCore/command_line/command_line.ml b/GillianCore/command_line/command_line.ml index 268a5ac09..0603f12b9 100644 --- a/GillianCore/command_line/command_line.ml +++ b/GillianCore/command_line/command_line.ml @@ -1,5 +1,6 @@ open Cmdliner module ParserAndCompiler = ParserAndCompiler +module Act_console = Act_console module Make (ID : Init_data.S) diff --git a/GillianCore/command_line/command_line.mli b/GillianCore/command_line/command_line.mli index 45eccc43d..8e08a165a 100644 --- a/GillianCore/command_line/command_line.mli +++ b/GillianCore/command_line/command_line.mli @@ -2,6 +2,15 @@ module ParserAndCompiler = ParserAndCompiler +module Act_console : sig + module Make + (ID : Init_data.S) + (PC : ParserAndCompiler.S with type init_data = ID.t) + (Abductor : + Abductor.S with type init_data = ID.t and type annot = PC.Annot.t) + (Gil_parsing : Gil_parsing.S with type annot = PC.Annot.t) : Console.S +end + module Make (ID : Init_data.S) (CMemory : CMemory.S with type init_data = ID.t) diff --git a/GillianCore/engine/BiAbduction/Abductor.ml b/GillianCore/engine/BiAbduction/Abductor.ml index dd6b9e093..2b7c5a84d 100644 --- a/GillianCore/engine/BiAbduction/Abductor.ml +++ b/GillianCore/engine/BiAbduction/Abductor.ml @@ -42,7 +42,7 @@ end We try to aggregate the logic of creating specs and running tests in a single module. *) module Make_raw (PC : ParserAndCompiler.S) - (State : SimplifiedSState) + (State : SimplifiedSState with type init_data = PC.init_data) (BiProcess : BiProcessingS with type state_t = State.t diff --git a/transformers/bin/c_bi_abd.ml b/transformers/bin/c_bi_abd.ml new file mode 100644 index 000000000..ffb3df360 --- /dev/null +++ b/transformers/bin/c_bi_abd.ml @@ -0,0 +1,13 @@ +open Prebuilt.Lib.C_ALoc +module SMemory = MonadicSMemory + +module Bi_cli = + Transformers_abductor.Abductor.Cli (MyInitData) (SMemory) (ParserAndCompiler) + (ExternalSemantics) + +let act_cmd = + match Bi_cli.cmds with + | [ Normal cmd ] -> cmd + | _ -> failwith "Unexpected command structure in bi-abduction CLI" + +let () = exit (Cmdliner.Cmd.eval act_cmd) diff --git a/transformers/bin/dune b/transformers/bin/dune index bd74a711d..7034e7c47 100644 --- a/transformers/bin/dune +++ b/transformers/bin/dune @@ -13,6 +13,7 @@ t_wisl_s t_wislf t_wislf_a - t_wislf_s) + t_wislf_s + c_bi_abd) (package transformers) - (libraries prebuilt states gillian)) + (libraries prebuilt states gillian transformers_abductor)) diff --git a/transformers/lib/bi_abduction/abductor.ml b/transformers/lib/bi_abduction/abductor.ml index cef3af5b2..d60d88353 100644 --- a/transformers/lib/bi_abduction/abductor.ml +++ b/transformers/lib/bi_abduction/abductor.ml @@ -9,10 +9,11 @@ module L = Gillian.Logging (** This functor expects to receive a symbolic memory that was *not* transformed through the Bi_abd combinator. *) module Make - (SMemory : States.MyMonadicSMemory.S) (Init_data : States.MyMonadicSMemory.ID) + (SMemory : States.MyMonadicSMemory.S) (PC : ParserAndCompiler.S with type init_data = Init_data.t) - (External : External.T(PC.Annot).S) = + (External : External.T(PC.Annot).S) : + Abductor.S with type init_data = PC.init_data and type annot = PC.Annot.t = struct (* We first construct memory that performs bi-abduction *) module BiMemory = States.Bi_abd.Make (SMemory) @@ -101,5 +102,19 @@ struct (* So first we need to extract a state that corresponds to the *) end - module Abductor = Abductor.Make_raw (PC) (SPState) (BiProcess) (External) + include Abductor.Make_raw (PC) (SPState) (BiProcess) (External) +end + +module Cli + (Init_data : States.MyMonadicSMemory.ID) + (SMemory : States.MyMonadicSMemory.S) + (PC : ParserAndCompiler.S with type init_data = Init_data.t) + (External : External.T(PC.Annot).S) = +struct + module Gil_parsing = Gil_parsing.Make (PC.Annot) + module Abductor = Make (Init_data) (SMemory) (PC) (External) + + include + Gillian.Command_line.Act_console.Make (Init_data) (PC) (Abductor) + (Gil_parsing) end diff --git a/transformers/lib/prebuilt/C.ml b/transformers/lib/prebuilt/C.ml index 839458a10..2606b9309 100644 --- a/transformers/lib/prebuilt/C.ml +++ b/transformers/lib/prebuilt/C.ml @@ -149,7 +149,7 @@ module ExternalSemantics = module InitData = Cgil_lib.Global_env module MyInitData = struct - type t = InitData.t + type t = InitData.t [@@deriving yojson] let init = C_states.CGEnv.set_init_data end diff --git a/transformers/lib/states/MyMonadicSMemory.ml b/transformers/lib/states/MyMonadicSMemory.ml index 9bb505783..4745706b9 100644 --- a/transformers/lib/states/MyMonadicSMemory.ml +++ b/transformers/lib/states/MyMonadicSMemory.ml @@ -116,13 +116,13 @@ end callback, that is called whenever memory is initialised with some init data. *) module type ID = sig - type t + type t [@@deriving yojson] val init : t -> unit end module DummyID : ID with type t = unit = struct - type t = unit + type t = unit [@@deriving yojson] let init () = () end From 852e6765c5c84dc8e653f1c9f024dd3671524646 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 9 Nov 2025 11:38:25 +0000 Subject: [PATCH 16/29] simplify abductor interface, finish implementing Signed-off-by: Sacha Ayoun --- GillianCore/engine/BiAbduction/Abductor.ml | 212 ++++----------------- transformers/lib/bi_abduction/abductor.ml | 64 ++----- transformers/lib/states/Fix.ml | 4 + 3 files changed, 60 insertions(+), 220 deletions(-) diff --git a/GillianCore/engine/BiAbduction/Abductor.ml b/GillianCore/engine/BiAbduction/Abductor.ml index 2b7c5a84d..846553768 100644 --- a/GillianCore/engine/BiAbduction/Abductor.ml +++ b/GillianCore/engine/BiAbduction/Abductor.ml @@ -20,6 +20,8 @@ module type SimplifiedSState = and type store_t = SStore.t module type BiProcessingS = sig + module NonBiPState : PState.S + type annot type init_data type state_t @@ -33,8 +35,7 @@ module type BiProcessingS = sig Asrt.t -> state_t list - val make_spec : - string -> string list -> state_t -> state_t -> Flag.t -> Spec.t option + val bistate_to_pstate_and_af : state_t -> NonBiPState.t * Asrt.t end (* A bit of hack around as the legacy hardcoded BiState and the new, @@ -466,8 +467,8 @@ end let make_spec (name : string) (params : string list) - (bi_state_i : bi_state_t) - (bi_state_f : bi_state_t) + (bi_state_i : state_t) + (bi_state_f : state_t) (fl : Flag.t) : Spec.t option = let open Syntaxes.List in let sspecs = @@ -475,8 +476,8 @@ end (* HMMMMM *) (* let _ = SBAState.simplify ~kill_new_lvars:true bi_state_f in *) - let state_i, _ = SBAState.get_components bi_state_i in - let state_f, state_af = SBAState.get_components bi_state_f in + let state_i, _ = BiProcess.bistate_to_pstate_and_af bi_state_i in + let state_f, af_asrt = BiProcess.bistate_to_pstate_and_af bi_state_f in let pvars = SS.of_list (Names.return_variable :: params) in L.verbose (fun m -> @@ -488,33 +489,34 @@ end %a@]" name Fmt.(list ~sep:comma string) - params SPState.pp state_af SPState.pp state_f); + params Asrt.pp af_asrt BiProcess.NonBiPState.pp state_f); (* Drop all pvars except ret/err from the state *) let () = - SStore.filter_map_inplace (SPState.get_store state_f) (fun x v -> - if x = Names.return_variable then Some v else None) + SStore.filter_map_inplace (BiProcess.NonBiPState.get_store state_f) + (fun x v -> if x = Names.return_variable then Some v else None) in let* post = let _, finals_simplified = - SPState.simplify ~kill_new_lvars:true state_f + BiProcess.NonBiPState.simplify ~kill_new_lvars:true state_f in let+ final_simplified = finals_simplified in List.sort Asrt.compare - (SPState.to_assertions ~to_keep:pvars final_simplified) + (BiProcess.NonBiPState.to_assertions ~to_keep:pvars final_simplified) in let+ pre = - let af_asrt = SPState.to_assertions state_af in let af_subst = make_id_subst af_asrt in - let* af_produce_res = SPState.produce state_i af_subst af_asrt in + let* af_produce_res = + BiProcess.NonBiPState.produce state_i af_subst af_asrt + in match af_produce_res with | Ok state_i' -> let _, simplifieds = - SPState.simplify ~kill_new_lvars:true state_i' + BiProcess.NonBiPState.simplify ~kill_new_lvars:true state_i' in let+ simplified = simplifieds in List.sort Asrt.compare - (SPState.to_assertions ~to_keep:pvars simplified) + (BiProcess.NonBiPState.to_assertions ~to_keep:pvars simplified) | Error _ -> L.verbose (fun m -> m "Failed to produce anti-frame"); [] @@ -568,36 +570,25 @@ end Some spec let testify ~init_data ~(prog : annot MP.prog) (bi_spec : BiSpec.t) : t list = + let open Syntaxes.List in L.verbose (fun m -> m "Bi-testifying: %s" bi_spec.bispec_name); let params = SS.of_list bi_spec.bispec_params in - let normalise = - Normaliser.normalise_assertion ~init_data ~pred_defs:prog.preds - ~pvars:params - in - let make_test asrt = - match normalise asrt with - | Error _ -> [] - | Ok l -> - List.map - (fun (ss_pre, _) -> - { - name = bi_spec.bispec_name; - params = bi_spec.bispec_params; - state = SBAState.make ~state:ss_pre ~init_data; - }) - l + (* For each pre in the bispec *) + let* pre, _ = bi_spec.bispec_pres in + let+ state = + BiProcess.normalise_assertion ~init_data ~pvars:params ~prog pre in - List.concat_map (fun (pre, _) -> make_test pre) bi_spec.bispec_pres + { name = bi_spec.bispec_name; params = bi_spec.bispec_params; state } let run_test (ret_fun : result_t -> (Spec.t * Flag.t) option) (prog : annot MP.prog) (test : t) : (Spec.t * Flag.t) list = - let state = SBAState.copy test.state in - let state = SBAState.add_spec_vars state (SBAState.get_lvars state) in + let state = State.copy test.state in + let state = State.add_spec_vars state (State.get_lvars state) in try let opt_results = - SBAInterpreter.evaluate_proc ret_fun prog test.name test.params state + Interp.evaluate_proc ret_fun prog test.name test.params state in let count = ref 0 in let result = @@ -622,11 +613,11 @@ end (prog : annot MP.prog) (name : string) (params : string list) - (state_i : bi_state_t) + (state_i : state_t) (result : result_t) : (Spec.t * Flag.t) option = let open Syntaxes.Option in let process_spec = make_spec in - let state_i = SBAState.copy state_i in + let state_i = State.copy state_i in let add_spec spec = try MP.add_spec prog spec with _ -> @@ -634,13 +625,8 @@ end (Format.asprintf "When trying to build an MP for %s, I died!" name) in match result with - | RFail { error_state; errors; _ } -> - (* Because of fixes, the state may have changed since between the start of execution - and the failure: the anti-frame might have been modified before immediately erroring. - BiState thus returns, with every error, the state immeditaly before the error happens - with any applied fixes - this is the state that should be used to ensure fixes - don't get lost. *) - let rec find_error_state (aux : SBAInterpreter.err_t list) = + | RFail { error_state; _ } -> + (* let rec find_error_state (aux : Interp.err_t list) = match aux with | [] -> error_state | e :: errs -> ( @@ -648,7 +634,7 @@ end | EState (EMem (s, _)) -> s | _ -> find_error_state errs) in - let error_state = find_error_state errors in + let error_state = find_error_state errors in *) let+ spec = process_spec name params state_i error_state Flag.Bug in add_spec spec; (spec, Flag.Bug) @@ -833,7 +819,7 @@ end let test_procs_incrementally (prog : annot MP.prog) - ~(init_data : SPState.init_data) + ~(init_data : State.init_data) ~(prev_results : BiAbductionResults.t) ~(reverse_graph : Call_graph.t) ~(changed_procs : string list) @@ -928,7 +914,7 @@ end test_procs_incrementally prog ~init_data ~prev_results ~reverse_graph ~changed_procs:proc_changes.changed_procs ~to_test in - let cur_call_graph = SBAInterpreter.call_graph in + let cur_call_graph = Interp.call_graph in let () = Call_graph.prune_procs prev_call_graph to_prune in let call_graph = Call_graph.merge prev_call_graph cur_call_graph in let results = BiAbductionResults.merge prev_results cur_results in @@ -939,10 +925,10 @@ end let cur_source_files = Option.value ~default:(SourceFiles.make ()) source_files in - let dyn_call_graph = SBAInterpreter.call_graph in + let dyn_call_graph = Interp.call_graph in let results = test_procs ~init_data ~call_graph prog in write_biabduction_results cur_source_files dyn_call_graph ~diff:"" results -end *) +end module Make (SPState : PState.S) @@ -960,6 +946,8 @@ module Make type init_data = SBAState.init_data type annot = PC.Annot.t + module NonBiPState = SPState + let normalise_assertion ~(init_data : init_data) ~(prog : 'a MP.prog) @@ -976,129 +964,9 @@ module Make in SBAState.make ~state:ss_pre ~init_data - let make_id_subst (a : Asrt.t) : SSubst.t = - let lvars = Asrt.lvars a in - let alocs = Asrt.alocs a in - let lvar_bindings = - List.map (fun x -> (Expr.LVar x, Expr.LVar x)) (SS.elements lvars) - in - let aloc_bindings = - List.map (fun x -> (Expr.LVar x, Expr.ALoc x)) (SS.elements alocs) - in - let bindings = lvar_bindings @ aloc_bindings in - let bindings' = - List.map - (fun (x, e) -> - match SVal.M.from_expr e with - | Some v -> (x, v) - | _ -> raise (Failure "DEATH. make_id_subst")) - bindings - in - SSubst.init bindings' - - let make_spec - (name : string) - (params : string list) - (bi_state_i : state_t) - (bi_state_f : state_t) - (fl : Flag.t) : Spec.t option = - let open Syntaxes.List in - let sspecs = - (* let start_time = time() in *) - - (* HMMMMM *) - (* let _ = SBAState.simplify ~kill_new_lvars:true bi_state_f in *) - let state_i, _ = SBAState.get_components bi_state_i in - let state_f, state_af = SBAState.get_components bi_state_f in - let pvars = SS.of_list (Names.return_variable :: params) in - - L.verbose (fun m -> - m - "Going to create a spec for @[%s(%a)@]\n\ - @[AF:@\n\ - %a@]@\n\ - @[Final STATE:@\n\ - %a@]" - name - Fmt.(list ~sep:comma string) - params SPState.pp state_af SPState.pp state_f); - (* Drop all pvars except ret/err from the state *) - let () = - SStore.filter_map_inplace (SPState.get_store state_f) (fun x v -> - if x = Names.return_variable then Some v else None) - in - let* post = - let _, finals_simplified = - SPState.simplify ~kill_new_lvars:true state_f - in - let+ final_simplified = finals_simplified in - List.sort Asrt.compare - (SPState.to_assertions ~to_keep:pvars final_simplified) - in - - let+ pre = - let af_asrt = SPState.to_assertions state_af in - let af_subst = make_id_subst af_asrt in - let* af_produce_res = SPState.produce state_i af_subst af_asrt in - match af_produce_res with - | Ok state_i' -> - let _, simplifieds = - SPState.simplify ~kill_new_lvars:true state_i' - in - let+ simplified = simplifieds in - List.sort Asrt.compare - (SPState.to_assertions ~to_keep:pvars simplified) - | Error _ -> - L.verbose (fun m -> m "Failed to produce anti-frame"); - [] - in - let post_clocs = Asrt.clocs post in - let pre_clocs = Asrt.clocs pre in - let new_clocs = SS.diff post_clocs pre_clocs in - let subst = Hashtbl.create Config.medium_tbl_size in - List.iter - (fun cloc -> Hashtbl.replace subst cloc (Expr.ALoc (ALoc.alloc ()))) - (SS.elements new_clocs); - let subst_fun cloc = - match Hashtbl.find_opt subst cloc with - | Some e -> e - | None -> Lit (Loc cloc) - in - let new_post = Asrt.subst_clocs subst_fun post in - Spec. - { - ss_pre = (pre, None); - ss_posts = [ (new_post, None) ]; - ss_variant = None; - ss_flag = fl; - ss_to_verify = false; - ss_label = None; - } - in - match sspecs with - | [] -> None - | sspecs -> - let spec = - Spec. - { - spec_name = name; - spec_params = params; - spec_sspecs = sspecs; - spec_normalised = true; - spec_incomplete = true; - spec_to_verify = false; - spec_location = None; - } - in - L.verbose (fun m -> - m - "@[Created a spec for @[%s(%a)@] successfully. Here \ - is the spec:@\n\ - %a@]" - name - Fmt.(list ~sep:comma string) - params Spec.pp spec); - Some spec + let bistate_to_pstate_and_af bistate = + let post, af = SBAState.get_components bistate in + (post, NonBiPState.to_assertions af) end end diff --git a/transformers/lib/bi_abduction/abductor.ml b/transformers/lib/bi_abduction/abductor.ml index d60d88353..1a3407e61 100644 --- a/transformers/lib/bi_abduction/abductor.ml +++ b/transformers/lib/bi_abduction/abductor.ml @@ -1,10 +1,9 @@ open Gillian open Gillian.Symbolic open Gillian.General -open Gillian.Gil_syntax -open Utils.Containers module MP = Gillian.Abstraction.MP module L = Gillian.Logging +module SSubst = Symbolic.Subst (** This functor expects to receive a symbolic memory that was *not* transformed through the Bi_abd combinator. *) @@ -30,7 +29,6 @@ struct module NonBiMemory = States.MyMonadicSMemory.Make (SMemory) (Init_data) module NonBiMemoryLegacy = Monadic.MonadicSMemory.Lift (NonBiMemory) module NonBiSState = SState.Make (NonBiMemoryLegacy) - module NonBiSPState = PState.Make (NonBiSState) (* We define a helper to run functions under bi-abduction *) @@ -45,6 +43,8 @@ struct type state_t = SPState.t type init_data = Init_data.t + module NonBiPState = PState.Make (NonBiSState) + let normalise_assertion ~init_data ~prog ~pvars assertion = match Normaliser.normalise_assertion ~init_data ~pred_defs:prog.MP.preds @@ -53,53 +53,21 @@ struct | Ok l -> List.map fst l | Error _ -> [] - let make_spec - name - params - (_initial_state : state_t) - (final_state : state_t) - fl = - let pvars = SS.of_list (Utils.Names.return_variable :: params) in - let States.Bi_abd.{ anti_frame = _; state } = - SPState.get_heap final_state - in - let final_state = - NonBiSPState.make_p_from_heap ~pred_defs:final_state.pred_defs - ~store:(SPState.get_store final_state) - ~heap:state - ~pfs:(SPState.get_pfs final_state) - ~gamma:(SPState.get_typ_env final_state) - ~spec_vars:(SPState.get_spec_vars final_state) - ~wands:(SPState.get_wands final_state) - ~preds:(SPState.get_preds final_state) - in - let post = NonBiSPState.to_assertions ~to_keep:pvars final_state in - let pre = [ Asrt.Emp ] in - let sspec = - Spec. - { - ss_pre = (pre, None); - ss_posts = [ (post, None) ]; - ss_variant = None; - ss_flag = fl; - ss_label = None; - ss_to_verify = false; - } + let bistate_to_pstate_and_af (bi_state : state_t) = + let States.Bi_abd.{ anti_frame; state } = SPState.get_heap bi_state in + let current = + NonBiPState.make_p_from_heap ~pred_defs:bi_state.pred_defs + ~store:(SPState.get_store bi_state) + ~heap:state ~pfs:(SPState.get_pfs bi_state) + ~gamma:(SPState.get_typ_env bi_state) + ~spec_vars:(SPState.get_spec_vars bi_state) + ~wands:(SPState.get_wands bi_state) + ~preds:(SPState.get_preds bi_state) in - let spec = - Spec. - { - spec_name = name; - spec_params = params; - spec_sspecs = [ sspec ]; - spec_normalised = true; - spec_incomplete = true; - spec_to_verify = false; - spec_location = None; - } + let anti_frame = + States.Fix.to_asrt ~pred_to_str:SMemory.pred_to_str anti_frame in - Some spec - (* So first we need to extract a state that corresponds to the *) + (current, anti_frame) end include Abductor.Make_raw (PC) (SPState) (BiProcess) (External) diff --git a/transformers/lib/states/Fix.ml b/transformers/lib/states/Fix.ml index 94dc1c23a..54a25da8a 100644 --- a/transformers/lib/states/Fix.ml +++ b/transformers/lib/states/Fix.ml @@ -29,3 +29,7 @@ let subst (subst : Gillian.Symbolic.Subst.t) (fix : 'a t) : 'a t = (cp, List.map le_subst ins, List.map le_subst outs) in List.map subst_atom fix + +let to_asrt ~pred_to_str fix : Asrt.t = + ListLabels.map fix ~f:(fun (cp, ins, outs) -> + Asrt.CorePred (pred_to_str cp, ins, outs)) From ce6f967910beab0c3e070d94a68db32b1e4eec04 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 9 Nov 2025 11:39:08 +0000 Subject: [PATCH 17/29] remove all commented code Signed-off-by: Sacha Ayoun --- GillianCore/engine/BiAbduction/Abductor.ml | 381 --------------------- 1 file changed, 381 deletions(-) diff --git a/GillianCore/engine/BiAbduction/Abductor.ml b/GillianCore/engine/BiAbduction/Abductor.ml index 846553768..ed6e74cc0 100644 --- a/GillianCore/engine/BiAbduction/Abductor.ml +++ b/GillianCore/engine/BiAbduction/Abductor.ml @@ -63,387 +63,6 @@ struct type annot = PC.Annot.t type init_data = PC.init_data - let testify ~init_data ~(prog : annot MP.prog) (bi_spec : BiSpec.t) : t list = - let open Syntaxes.List in - L.verbose (fun m -> m "Bi-testifying: %s" bi_spec.bispec_name); - let params = SS.of_list bi_spec.bispec_params in - (* For each pre in the bispec *) - let* pre, _ = bi_spec.bispec_pres in - let+ state = - BiProcess.normalise_assertion ~init_data ~pvars:params ~prog pre - in - { name = bi_spec.bispec_name; params = bi_spec.bispec_params; state } - - let run_test - (ret_fun : result_t -> (Spec.t * Flag.t) option) - (prog : annot MP.prog) - (test : t) : (Spec.t * Flag.t) list = - let state = State.copy test.state in - let state = State.add_spec_vars state (State.get_lvars state) in - try - let opt_results = - Interp.evaluate_proc ret_fun prog test.name test.params state - in - let count = ref 0 in - let result = - List.filter_map - (function - | None -> - incr count; - None - | x -> x) - opt_results - in - if !count > 0 then - L.verbose (fun m -> - m "WARNING: %d vanished while creating the for %s!" !count test.name); - result - with Failure msg -> - L.print_to_all - (Printf.sprintf "ERROR in proc %s with message:\n%s\n" test.name msg); - [] - - let process_sym_exec_result - (prog : annot MP.prog) - (name : string) - (params : string list) - (state_i : state_t) - (result : result_t) : (Spec.t * Flag.t) option = - let open Syntaxes.Option in - let process_spec = BiProcess.make_spec in - let state_i = State.copy state_i in - let add_spec spec = - try MP.add_spec prog spec - with _ -> - L.fail - (Format.asprintf "When trying to build an MP for %s, I died!" name) - in - match result with - | RFail { error_state; _ } -> - (* let rec find_error_state (aux : Interp.err_t list) = - match aux with - | [] -> error_state - | e :: errs -> ( - match e with - | EState (EMem (s, _)) -> s - | _ -> find_error_state errs) - in - let error_state = find_error_state errors in *) - let+ spec = process_spec name params state_i error_state Flag.Bug in - add_spec spec; - (spec, Flag.Bug) - | RSucc { flag; final_state; _ } -> - let+ spec = process_spec name params state_i final_state flag in - add_spec spec; - (spec, flag) - - type proc_stats = { - gil_size : int; - mutable tests : int; - mutable succs : int; - mutable bugs : int; - mutable time : float; - } - - let pp_proc_stats fmt { gil_size; tests; succs; bugs; time } = - Fmt.pf fmt "%d, %d, %d, %d, %f" gil_size tests succs bugs time - - let run_tests (prog : annot MP.prog) (tests : t list) = - let num_tests = List.length tests in - Fmt.pr "Running tests on %d procs.\n@?" num_tests; - - let stats : (string * proc_stats) list ref = ref [] in - let get_stats name get_gil_size = - match List.assoc_opt name !stats with - | Some s -> s - | None -> - let gil_size = get_gil_size () in - let s = { gil_size; tests = 0; succs = 0; bugs = 0; time = 0.0 } in - stats := (name, s) :: !stats; - s - in - - let rec run_tests_aux tests succ_specs err_specs bug_specs i = - match tests with - | [] -> (succ_specs, err_specs, bug_specs) - | test :: rest -> - let rec part3 = function - | [] -> ([], [], []) - | (spec, flag) :: rest -> ( - let succ_specs, err_specs, bug_specs = part3 rest in - match flag with - | Flag.Normal -> (spec :: succ_specs, err_specs, bug_specs) - | Flag.Error -> (succ_specs, spec :: err_specs, bug_specs) - | Flag.Bug -> (succ_specs, err_specs, spec :: bug_specs)) - in - L.verbose (fun m -> m "Running bi-abduction on %s\n" test.name); - Fmt.pr "Testing %s... @?" test.name; - let start_time = Sys.time () in - let rets = - run_test - (process_sym_exec_result prog test.name test.params test.state) - prog test - in - let end_time = Sys.time () in - let stats = - get_stats test.name (fun () -> - match Hashtbl.find_opt prog.prog.procs test.name with - | None -> -1 - | Some prog -> Array.length prog.proc_body) - in - let cur_succ_specs, cur_err_specs, cur_bug_specs = part3 rets in - let new_succ_specs = succ_specs @ cur_succ_specs in - let new_err_specs = err_specs @ cur_err_specs in - let new_bug_specs = bug_specs @ cur_bug_specs in - - stats.tests <- stats.tests + 1; - stats.succs <- stats.succs + List.length cur_succ_specs; - stats.bugs <- stats.bugs + List.length cur_bug_specs; - stats.time <- stats.time +. (end_time -. start_time); - Fmt.pr "%dS %dB (%d/%d)\n@?" - (List.length cur_succ_specs) - (List.length cur_bug_specs) - i num_tests; - - run_tests_aux rest new_succ_specs new_err_specs new_bug_specs (i + 1) - in - let result = run_tests_aux tests [] [] [] 1 in - Fmt.pr "\nTest results:\nProc, GIL Commands, Tests, Succs, Bugs, Time\n"; - !stats - |> List.sort (fun (name1, _) (name2, _) -> String.compare name1 name2) - |> List.iter (fun (name, stats) -> - Fmt.pr "%s, %a\n" name pp_proc_stats stats); - Fmt.pr "@?"; - result - - let get_test_results - (prog : annot MP.prog) - (succ_specs : Spec.t list) - (error_specs : Spec.t list) - (bug_specs : Spec.t list) = - let sort_specs = - List.sort - (fun Spec.{ spec_name = name1; _ } Spec.{ spec_name = name2; _ } -> - String.compare name1 name2) - in - let bug_specs_txt = - Format.asprintf "@[BUG SPECS:@\n%a@]@\n" - Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) - (sort_specs bug_specs) - in - let error_specs_txt = - Format.asprintf "@[ERROR SPECS:@\n%a@]@\n" - Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) - (sort_specs error_specs) - in - let normal_specs_txt = - Format.asprintf "@[SUCCESSFUL SPECS:@\n%a@]@\n" - Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) - (sort_specs succ_specs) - in - - if !Config.specs_to_stdout then ( - L.print_to_all bug_specs_txt; - L.print_to_all error_specs_txt; - L.print_to_all normal_specs_txt) - else ( - L.normal (fun m -> m "%s" bug_specs_txt); - L.normal (fun m -> m "%s" error_specs_txt); - L.normal (fun m -> m "%s" normal_specs_txt)); - - (* This is a hack to not count auxiliary functions that are bi-abduced *) - let len_succ = List.length succ_specs in - let auxiliaries = - List.fold_left - (fun ac (spec : Spec.t) -> - ac || String.equal spec.spec_name "assumeType") - false succ_specs - in - let offset = if auxiliaries then 12 else 0 in - let len_succ = len_succ - offset in - let () = - L.print_to_all - (Printf.sprintf "SUCCESS SPECS: %d\nERROR SPECS: %d\nBUG SPECS: %d" - len_succ (List.length error_specs) (List.length bug_specs)) - in - let results = BiAbductionResults.make () in - let () = - List.iter - (fun (spec : Spec.t) -> - BiAbductionResults.set_spec results spec.spec_name spec) - (Prog.get_specs prog.prog) - in - results - - let str_concat = String.concat ", " - - let sort_tests_by_callgraph tests callgraph = - let rec aux acc rest_tests = function - | [] -> (acc, rest_tests) - | name :: rest -> - let selected_tests, rest_tests = - List.partition (fun t -> t.name = name) rest_tests - in - aux (acc @ selected_tests) rest_tests rest - in - let callgraph_order = Call_graph.get_sorted_names callgraph in - let sorted_tests, rest_tests = aux [] tests callgraph_order in - let rest_sorted_tests = - rest_tests |> List.sort (fun t1 t2 -> Stdlib.compare t1.name t2.name) - in - sorted_tests @ rest_sorted_tests - - let test_procs ~init_data ~call_graph (prog : annot MP.prog) = - L.verbose (fun m -> m "Starting bi-abductive testing in normal mode"); - let proc_names = Prog.get_noninternal_proc_names prog.prog in - L.verbose (fun m -> m "Proc names: %s" (str_concat proc_names)); - let bi_specs = List.map (Prog.get_bispec_exn prog.prog) proc_names in - - let tests = List.concat_map (testify ~init_data ~prog) bi_specs in - let test_names tests = str_concat (List.map (fun t -> t.name) tests) in - L.verbose (fun m -> m "I have tests for: %s" (test_names tests)); - let tests = sort_tests_by_callgraph tests call_graph in - L.verbose (fun m -> m "I have tests for: %s" (test_names tests)); - let succ_specs, err_specs, bug_specs = run_tests prog tests in - get_test_results prog succ_specs err_specs bug_specs - - let specs_equal (spec_a : Spec.t) (spec_b : Spec.t) = - (* FIXME: Perform a more robust comparsion based on matching *) - String.equal (Spec.hash_of_t spec_a) (Spec.hash_of_t spec_b) - - let test_procs_incrementally - (prog : annot MP.prog) - ~(init_data : State.init_data) - ~(prev_results : BiAbductionResults.t) - ~(reverse_graph : Call_graph.t) - ~(changed_procs : string list) - ~(to_test : string list) = - L.verbose (fun m -> m "Starting bi-abductive testing in incremental mode"); - let to_test_set = SS.of_list to_test in - let filter spec_name = not (SS.mem spec_name to_test_set) in - let prev_specs = BiAbductionResults.get_all_specs ~filter prev_results in - let prev_spec_names = - str_concat (List.map (fun (s : Spec.t) -> s.spec_name) prev_specs) - in - L.verbose (fun m -> m "I will use the stored specs of: %s" prev_spec_names); - List.iter (fun spec -> MP.add_spec prog spec) prev_specs; - - let rec test_procs_aux to_test checked succ_specs error_specs bug_specs = - (* FIXME: Keep tests in a heap/priority queue *) - match to_test with - | [] -> (succ_specs, error_specs, bug_specs) - | proc_name :: rest -> - let () = MP.remove_spec prog proc_name in - let tests = - testify ~init_data ~prog (Prog.get_bispec_exn prog.prog proc_name) - in - let cur_succ_specs, cur_err_specs, cur_bug_specs = - run_tests prog tests - in - let checked = SS.add proc_name checked in - let new_to_test = - if BiAbductionResults.contains_spec prev_results proc_name then - let prev_spec = - BiAbductionResults.get_spec_exn prev_results proc_name - in - let new_spec = (Hashtbl.find prog.specs proc_name).data in - if not (specs_equal prev_spec new_spec) then ( - L.verbose (fun m -> m "The spec of %s has changed" proc_name); - (* Must also check immediate callers *) - let callers = - ChangeTracker.get_callers prog.prog ~reverse_graph - ~excluded_procs:changed_procs ~proc_name - in - let callers = - List.filter (fun name -> not (SS.mem name checked)) callers - in - L.verbose (fun m -> - m "I will check its callers: %s" (str_concat callers)); - List.sort Stdlib.compare (rest @ callers)) - else ( - L.verbose (fun m -> m "The spec of %s is unchanged" proc_name); - rest) - else rest - in - let new_succ_specs = succ_specs @ cur_succ_specs in - let new_err_specs = error_specs @ cur_err_specs in - let new_bug_specs = bug_specs @ cur_bug_specs in - test_procs_aux new_to_test checked new_succ_specs new_err_specs - new_bug_specs - in - (* Keep list sorted to ensure tests are executed in the required order *) - let to_test = List.sort Stdlib.compare to_test in - L.verbose (fun m -> m "I will begin by checking: %s" (str_concat to_test)); - let succ_specs, error_specs, bug_specs = - test_procs_aux to_test SS.empty [] [] [] - in - get_test_results prog succ_specs error_specs bug_specs - - let test_prog - ~init_data - ?(call_graph = Call_graph.make ()) - (prog : annot MP.prog) - (incremental : bool) - (source_files : SourceFiles.t option) : unit = - let open ResultsDir in - let open ChangeTracker in - if incremental && prev_results_exist () then - (* Only test changed procedures *) - let cur_source_files = - match source_files with - | Some files -> files - | None -> failwith "Cannot use -a in incremental mode" - in - let prev_source_files, prev_call_graph, prev_results = - read_biabduction_results () - in - let proc_changes = - get_changes prog.prog ~prev_source_files ~prev_call_graph - ~cur_source_files - in - let to_test = proc_changes.changed_procs @ proc_changes.new_procs in - let to_prune = proc_changes.changed_procs @ proc_changes.deleted_procs in - let reverse_graph = Call_graph.to_reverse_graph prev_call_graph in - let cur_results = - test_procs_incrementally prog ~init_data ~prev_results ~reverse_graph - ~changed_procs:proc_changes.changed_procs ~to_test - in - let cur_call_graph = Interp.call_graph in - let () = Call_graph.prune_procs prev_call_graph to_prune in - let call_graph = Call_graph.merge prev_call_graph cur_call_graph in - let results = BiAbductionResults.merge prev_results cur_results in - let diff = Fmt.str "%a" ChangeTracker.pp_proc_changes proc_changes in - write_biabduction_results cur_source_files call_graph ~diff results - else - (* Test all procedures *) - let cur_source_files = - Option.value ~default:(SourceFiles.make ()) source_files - in - let dyn_call_graph = Interp.call_graph in - let results = test_procs ~init_data ~call_graph prog in - write_biabduction_results cur_source_files dyn_call_graph ~diff:"" results -end - -(* module Make - (SPState : PState.S) - (PC : ParserAndCompiler.S with type init_data = SPState.init_data) - (External : External.T(PC.Annot).S) : - S with type annot = PC.Annot.t and type init_data = PC.init_data = struct - module L = Logging - module SSubst = SVal.SESubst - module Normaliser = Normaliser.Make (SPState) - module SBAState = BiState.Make (SPState) - - module SBAInterpreter = - G_interpreter.Make (SVal.M) (SVal.SESubst) (SStore) (SBAState) (PC) - (External) - - type bi_state_t = SBAState.t - type result_t = SBAInterpreter.result_t - type t = { name : string; params : string list; state : bi_state_t } - type annot = PC.Annot.t - type init_data = PC.init_data - let make_id_subst (a : Asrt.t) : SSubst.t = let lvars = Asrt.lvars a in let alocs = Asrt.alocs a in From 1fa343640e20cc417e2a7b7647e3c5c7a1481dd0 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 9 Nov 2025 12:34:41 +0000 Subject: [PATCH 18/29] printing Signed-off-by: Sacha Ayoun --- GillianCore/engine/BiAbduction/Abductor.ml | 9 +++------ GillianCore/engine/general_semantics/eSubst.ml | 2 +- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/GillianCore/engine/BiAbduction/Abductor.ml b/GillianCore/engine/BiAbduction/Abductor.ml index ed6e74cc0..678c20bd7 100644 --- a/GillianCore/engine/BiAbduction/Abductor.ml +++ b/GillianCore/engine/BiAbduction/Abductor.ml @@ -70,7 +70,7 @@ struct List.map (fun x -> (Expr.LVar x, Expr.LVar x)) (SS.elements lvars) in let aloc_bindings = - List.map (fun x -> (Expr.LVar x, Expr.ALoc x)) (SS.elements alocs) + List.map (fun x -> (Expr.ALoc x, Expr.ALoc x)) (SS.elements alocs) in let bindings = lvar_bindings @ aloc_bindings in let bindings' = @@ -101,11 +101,8 @@ struct L.verbose (fun m -> m - "Going to create a spec for @[%s(%a)@]\n\ - @[AF:@\n\ - %a@]@\n\ - @[Final STATE:@\n\ - %a@]" + "Going to create a spec for @[%s(%a)@]@\n\ + @[@[AF:@ %a@] @[Final STATE: %a@]@]" name Fmt.(list ~sep:comma string) params Asrt.pp af_asrt BiProcess.NonBiPState.pp state_f); diff --git a/GillianCore/engine/general_semantics/eSubst.ml b/GillianCore/engine/general_semantics/eSubst.ml index 3c573f15d..add2aa033 100644 --- a/GillianCore/engine/general_semantics/eSubst.ml +++ b/GillianCore/engine/general_semantics/eSubst.ml @@ -287,7 +287,7 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct @return unit *) let full_pp fmt (subst : t) = let pp_pair fmt (e, e_val) = - Fmt.pf fmt "@[(%a: %a)@]" Expr.pp e Val.full_pp e_val + Fmt.pf fmt "@[(%a: %a)@]" Expr.full_pp e Val.full_pp e_val in Fmt.pf fmt "[ @[%a@] ]" (Fmt.hashtbl ~sep:Fmt.comma pp_pair) subst From 5bcb01c81070aa3f775549475133cc88566428cd Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 9 Nov 2025 14:05:35 +0000 Subject: [PATCH 19/29] BOOYAH Signed-off-by: Sacha Ayoun --- transformers/lib/bi_abduction/abductor.ml | 14 +++- .../lib/prebuilt/c_states/BlockTree.ml | 71 ++++++++++--------- transformers/lib/states/bi_abd.ml | 7 +- 3 files changed, 56 insertions(+), 36 deletions(-) diff --git a/transformers/lib/bi_abduction/abductor.ml b/transformers/lib/bi_abduction/abductor.ml index 1a3407e61..d79206bb0 100644 --- a/transformers/lib/bi_abduction/abductor.ml +++ b/transformers/lib/bi_abduction/abductor.ml @@ -1,6 +1,7 @@ open Gillian open Gillian.Symbolic open Gillian.General +open Gil_syntax module MP = Gillian.Abstraction.MP module L = Gillian.Logging module SSubst = Symbolic.Subst @@ -64,8 +65,19 @@ struct ~wands:(SPState.get_wands bi_state) ~preds:(SPState.get_preds bi_state) in + (* To avoid unfeasible matching plans, we bring up equalities that avoid variable disconnection. *) let anti_frame = - States.Fix.to_asrt ~pred_to_str:SMemory.pred_to_str anti_frame + let spatial = + States.Fix.to_asrt ~pred_to_str:SMemory.pred_to_str anti_frame + in + let equalities = + SPState.get_pfs bi_state |> Pure_context.to_list + |> List.filter (function + | Expr.BinOp (_, Equal, _) -> true + | _ -> false) + |> List.map (fun e -> Asrt.Pure e) + in + spatial @ equalities in (current, anti_frame) end diff --git a/transformers/lib/prebuilt/c_states/BlockTree.ml b/transformers/lib/prebuilt/c_states/BlockTree.ml index fb588660a..0a575b16b 100644 --- a/transformers/lib/prebuilt/c_states/BlockTree.ml +++ b/transformers/lib/prebuilt/c_states/BlockTree.ml @@ -485,20 +485,24 @@ module Node = struct DR.ok (SVArr.AllUndef, exact_perm) let encode ~(perm : Perm.t) ~(chunk : Chunk.t) (sval : SVal.t) = - let mem_val = + let open Delayed.Syntax in + let+ mem_val = match (sval, chunk) with | ( SVint _, (Mint8signed | Mint8unsigned | Mint16signed | Mint16unsigned | Mint32) ) | SVlong _, Mint64 | SVsingle _, Mfloat32 - | SVfloat _, Mfloat64 -> Single { chunk; value = sval } + | SVfloat _, Mfloat64 -> Delayed.return (Single { chunk; value = sval }) | SVlong _, Mptr when Compcert.Archi.ptr64 -> - Single { chunk; value = sval } + Delayed.return (Single { chunk; value = sval }) | SVint _, Mptr when not Compcert.Archi.ptr64 -> - Single { chunk; value = sval } - | Sptr _, c when Chunk.could_be_ptr c -> Single { chunk; value = sval } - | _ -> Single { chunk; value = SUndefined } + Delayed.return (Single { chunk; value = sval }) + | Sptr _, c when Chunk.could_be_ptr c -> + Delayed.return (Single { chunk; value = sval }) + | _ -> + if !Gillian.Utils.Config.under_approximation then Delayed.vanish () + else Delayed.return (Single { chunk; value = SUndefined }) in MemVal { exact_perm = Some perm; min_perm = perm; mem_val } @@ -639,17 +643,18 @@ module Tree = struct in Delayed.return { node = new_node; span; children = Some (left, right) } - let remove_node x = Ok (make ~node:(NotOwned Totally) ~span:x.span ()) + let remove_node x = DR.ok (make ~node:(NotOwned Totally) ~span:x.span ()) let sval_leaf ~low ~perm ~value ~chunk = - let node = Node.encode ~perm ~chunk value in + let open Delayed.Syntax in + let+ node = Node.encode ~perm ~chunk value in let span = Range.of_low_and_chunk low chunk in - make ~node ~span () + Ok (make ~node ~span ()) let sarr_leaf ~low ~perm ~size ~array ~chunk = let node = Node.encode_arr ~perm ~chunk array in let span = Range.of_low_chunk_and_size low chunk size in - make ~node ~span () + DR.ok (make ~node ~span ()) let undefined ?(perm = Perm.Freeable) span = make ~node:(Node.undefined ~perm) ~span () @@ -779,9 +784,8 @@ module Tree = struct Range.is_equal range t.span then ( log_string "Range does equal span, replacing."; - match replace_node t with - | Ok new_tree -> DR.ok (t, new_tree) - | Error err -> DR.error err) + let++ new_tree = replace_node t in + (t, new_tree)) else match t.children with | Some (left, right) -> @@ -792,7 +796,7 @@ module Tree = struct then let l, h = range in let upper_range = (mid, h) in - let dont_replace_node = Result.ok in + let dont_replace_node = DR.ok in if%sat (* High-range already good *) Range.is_equal upper_range right.span @@ -870,7 +874,7 @@ module Tree = struct let prod_node (t : t) range node : (t, err) DR.t = let open DR.Syntax in - let replace_node _ = Ok (make ~node ~span:range ()) in + let replace_node _ = DR.ok (make ~node ~span:range ()) in let rebuild_parent = of_children in let++ _, t = frame_range t ~replace_node ~rebuild_parent range in t @@ -896,7 +900,7 @@ module Tree = struct (perm : Perm.t) : (t, err) DR.t = let open DR.Syntax in let open Delayed.Syntax in - let replace_node _ = Ok (sarr_leaf ~low ~chunk ~array ~size ~perm) in + let replace_node _ = sarr_leaf ~low ~chunk ~array ~size ~perm in let rebuild_parent = of_children in let range = Range.of_low_chunk_and_size low chunk size in let** _, t = frame_range t ~replace_node ~rebuild_parent range in @@ -921,7 +925,7 @@ module Tree = struct (sval : SVal.t) (perm : Perm.t) : (t, err) DR.t = let open DR.Syntax in - let replace_node _ = Ok (sval_leaf ~low ~chunk ~value:sval ~perm) in + let replace_node _ = sval_leaf ~low ~chunk ~value:sval ~perm in let rebuild_parent = of_children in let range = Range.of_low_and_chunk low chunk in let++ _, t = frame_range t ~replace_node ~rebuild_parent range in @@ -934,17 +938,17 @@ module Tree = struct let replace_node node = match node.node with | Node.NotOwned Totally -> - Error (MissingResource (Fixable { is_store = false; low; chunk })) + DR.error (MissingResource (Fixable { is_store = false; low; chunk })) | Node.NotOwned Partially -> Logging.verbose (fun fmt -> fmt "SHeapTree Load Error: Memory Partially Not Owned (Currently \ Unsupported)"); - Error (MissingResource Unfixable) + DR.error (MissingResource Unfixable) | MemVal { min_perm; _ } -> - if min_perm >=% Readable then Ok node + if min_perm >=% Readable then DR.ok node else - Error + DR.error (InsufficientPermission { required = Readable; actual = min_perm }) in let rebuild_parent = with_children in @@ -960,18 +964,18 @@ module Tree = struct let replace_node node = match node.node with | NotOwned Totally -> - Error (MissingResource (Fixable { is_store = true; low; chunk })) + DR.error (MissingResource (Fixable { is_store = true; low; chunk })) | NotOwned Partially -> Logging.verbose (fun fmt -> fmt "SHeapTree Store Error: Memory Partially Not Owned (Currently \ Unsupported)"); - Error (MissingResource Unfixable) + DR.error (MissingResource Unfixable) | MemVal { min_perm; _ } -> if min_perm >=% Writable then - Ok (sval_leaf ~low ~chunk ~value:sval ~perm:min_perm) + sval_leaf ~low ~chunk ~value:sval ~perm:min_perm else - Error + DR.error (InsufficientPermission { required = Writable; actual = min_perm }) in let rebuild_parent = of_children in @@ -1020,16 +1024,16 @@ module Tree = struct let replace_node node = match node.node with | NotOwned Totally -> - Error (MissingResource Unfixable) (* No chunk available to fix *) + DR.error (MissingResource Unfixable) (* No chunk available to fix *) | NotOwned Partially -> Logging.verbose (fun fmt -> fmt "SHeapTree Drop Permission Error: Memory Partially Not Owned \ (Currently Unsupported)"); - Error (MissingResource Unfixable) - | MemVal { min_perm = Freeable; _ } -> Ok (rec_set_perm node) + DR.error (MissingResource Unfixable) + | MemVal { min_perm = Freeable; _ } -> DR.ok (rec_set_perm node) | MemVal { min_perm; _ } -> - Error + DR.error (InsufficientPermission { required = Freeable; actual = min_perm }) in let rebuild_parent = update_parent_perm in @@ -1403,8 +1407,7 @@ module M = struct | None -> DR.error (MissingResource Unfixable) | Some src_root -> let** framed, _ = - Tree.frame_range src_root - ~replace_node:(fun x -> Ok x) + Tree.frame_range src_root ~replace_node:DR.ok ~rebuild_parent:(fun t ~left:_ ~right:_ -> Delayed.return t) src_range in @@ -1421,8 +1424,8 @@ module M = struct Tree.frame_range dst_root ~replace_node:(fun current -> match current.node with - | NotOwned _ -> Error (MissingResource Unfixable) - | _ -> Ok (Tree.realign framed dst_ofs)) + | NotOwned _ -> DR.error (MissingResource Unfixable) + | _ -> DR.ok (Tree.realign framed dst_ofs)) ~rebuild_parent:Tree.of_children dst_range in DR.of_result (with_root dst_tree new_dst_root) @@ -1481,7 +1484,7 @@ module M = struct List.fold_left (fun acc (tree_node : Tree.t) -> let** acc = acc in - let replace_node _ = Ok tree_node in + let replace_node _ = DR.ok tree_node in let rebuild_parent = Tree.of_children in let++ _, tree = Tree.frame_range acc ~replace_node ~rebuild_parent diff --git a/transformers/lib/states/bi_abd.ml b/transformers/lib/states/bi_abd.ml index f21566ab3..df71a965f 100644 --- a/transformers/lib/states/bi_abd.ml +++ b/transformers/lib/states/bi_abd.ml @@ -37,7 +37,12 @@ module Make (Mem : MyMonadicSMemory.S) : (* This is the missing error case *) (* We take each fix one by one *) let* cp_list = - Mem.get_fixes err |> List.map Delayed.return |> Delayed.branches + let fixes = Mem.get_fixes err in + Logging.verbose (fun m -> + m "Attempting to fix %a with candidates: %a" Mem.pp_err_t err + (Fmt.Dump.list (Fix.pp (Fmt.of_to_string Mem.pred_to_str))) + fixes); + List.map Delayed.return fixes |> Delayed.branches in let* state' = List.fold_left From 1d898e976bd9f52da6292735ccf6bf3dbaad4184 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 9 Nov 2025 14:28:48 +0000 Subject: [PATCH 20/29] ok Signed-off-by: Sacha Ayoun --- GillianCore/engine/BiAbduction/BiState.ml | 21 ++++++++++--------- .../lib/prebuilt/c_states/BlockTree.ml | 8 +++---- 2 files changed, 15 insertions(+), 14 deletions(-) diff --git a/GillianCore/engine/BiAbduction/BiState.ml b/GillianCore/engine/BiAbduction/BiState.ml index 39400ac10..72febf4b0 100644 --- a/GillianCore/engine/BiAbduction/BiState.ml +++ b/GillianCore/engine/BiAbduction/BiState.ml @@ -469,16 +469,17 @@ module Make (State : SState.S) = struct | Ok (state', outs) -> [ Ok ({ state = state'; af_state }, outs) ] | Error err when not (State.can_fix err) -> [ Error (lift_error { state; af_state } err) ] - | Error err -> ( - match State.get_fixes err with - | [] -> [] (* No fix, we stop *) - | fixes -> - let* fix = fixes in - let state' = State.copy state in - let af_state' = State.copy af_state in - let* state' = fix_list_apply state' fix in - let* af_state' = fix_list_apply af_state' fix in - execute_action action { state = state'; af_state = af_state' } args) + | Error err -> + let fixes = State.get_fixes err in + Logging.verbose (fun m -> + m "Attempting to fix %a with candidates: %a" State.pp_err_t err + (Fmt.Dump.list Asrt.pp) fixes); + let* fix = fixes in + let state' = State.copy state in + let af_state' = State.copy af_state in + let* state' = fix_list_apply state' fix in + let* af_state' = fix_list_apply af_state' fix in + execute_action action { state = state'; af_state = af_state' } args let get_equal_values { state; _ } = State.get_equal_values state let get_heap { state; _ } = State.get_heap state diff --git a/transformers/lib/prebuilt/c_states/BlockTree.ml b/transformers/lib/prebuilt/c_states/BlockTree.ml index 0a575b16b..2f28795c9 100644 --- a/transformers/lib/prebuilt/c_states/BlockTree.ml +++ b/transformers/lib/prebuilt/c_states/BlockTree.ml @@ -1684,16 +1684,16 @@ module M = struct let new_var1 = Expr.LVar (LVar.alloc ()) in let new_var2 = Expr.LVar (LVar.alloc ()) in let value = Expr.EList [ new_var1; new_var2 ] in - let null_typ = + (* let null_typ = if Compcert.Archi.ptr64 then Expr.string long_type else Expr.string int_type in - let null_ptr = Expr.EList [ null_typ; Expr.int 0 ] in + let null_ptr = Expr.EList [ null_typ; Expr.int 0 ] in *) [ [ (Single, [ ofs; chunk_as_expr ], [ value; freeable_perm ]) ]; - [ + (* [ (Single, [ ofs; chunk_as_expr ], [ null_ptr; freeable_perm ]); - ]; + ]; *) ] | _ -> let type_str = From 5621fe7e87833c225cf05ace12206eac11dfb3ab Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 9 Nov 2025 14:35:54 +0000 Subject: [PATCH 21/29] aaaaa Signed-off-by: Sacha Ayoun --- transformers/lib/prebuilt/c_states/BlockTree.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/transformers/lib/prebuilt/c_states/BlockTree.ml b/transformers/lib/prebuilt/c_states/BlockTree.ml index 2f28795c9..10ac9b51b 100644 --- a/transformers/lib/prebuilt/c_states/BlockTree.ml +++ b/transformers/lib/prebuilt/c_states/BlockTree.ml @@ -1681,19 +1681,19 @@ module M = struct let fixes = match chunk with | Mptr -> - let new_var1 = Expr.LVar (LVar.alloc ()) in + let new_var1 = Expr.ALoc (ALoc.alloc ()) in let new_var2 = Expr.LVar (LVar.alloc ()) in let value = Expr.EList [ new_var1; new_var2 ] in - (* let null_typ = + let null_typ = if Compcert.Archi.ptr64 then Expr.string long_type else Expr.string int_type in - let null_ptr = Expr.EList [ null_typ; Expr.int 0 ] in *) + let null_ptr = Expr.EList [ null_typ; Expr.int 0 ] in [ [ (Single, [ ofs; chunk_as_expr ], [ value; freeable_perm ]) ]; - (* [ + [ (Single, [ ofs; chunk_as_expr ], [ null_ptr; freeable_perm ]); - ]; *) + ]; ] | _ -> let type_str = From c3d6ee0e0457fc5eb210390a11910b10909e6d9c Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 9 Nov 2025 15:06:44 +0000 Subject: [PATCH 22/29] failures to match in UX mode should be ignored Signed-off-by: Sacha Ayoun --- GillianCore/engine/Abstraction/Matcher.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml index 4036171c9..75e255a55 100644 --- a/GillianCore/engine/Abstraction/Matcher.ml +++ b/GillianCore/engine/Abstraction/Matcher.ml @@ -1508,8 +1508,6 @@ module Make (State : SState.S) : let successes, errors = Res_list.split res_list in match (!Config.under_approximation, successes, errors) with (* We start by handling the crash cases that should never happen *) - | true, _, _ :: _ -> - L.fail "ERROR: IMPOSSIBLE! MATCHING ERRORS IN UX MODE!!!!" | true, [], _ -> (* Vanished in UX *) match_mp' (rest_search_states, errs_so_far) @@ -1556,7 +1554,7 @@ module Make (State : SState.S) : | Ok res -> Ok res | Error errs -> match_mp' (rest_search_states, errs @ errs_so_far)) - | true, first :: rem, [] -> + | true, first :: rem, _ -> let rem = List.map (fun state -> From 23bed500ff34c58f6adf5614e60c390549c7d833 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 9 Nov 2025 15:06:55 +0000 Subject: [PATCH 23/29] don't crash if SMT is banana in UX Signed-off-by: Sacha Ayoun --- GillianCore/engine/FOLogic/FOSolver.ml | 6 +++++- GillianCore/smt/smt.ml | 23 +++++++++++++---------- GillianCore/smt/smt.mli | 1 + 3 files changed, 19 insertions(+), 11 deletions(-) diff --git a/GillianCore/engine/FOLogic/FOSolver.ml b/GillianCore/engine/FOLogic/FOSolver.ml index cc121d667..ac0df42e0 100644 --- a/GillianCore/engine/FOLogic/FOSolver.ml +++ b/GillianCore/engine/FOLogic/FOSolver.ml @@ -86,7 +86,11 @@ let check_satisfiability if Expr.Set.is_empty fs then true else if Expr.Set.mem Expr.false_ fs then false else - let result = Smt.is_sat fs (Type_env.as_hashtbl gamma) in + let result = + try Smt.is_sat fs (Type_env.as_hashtbl gamma) + with Smt.SMT_error _ | Smt.SMT_unknown -> + if !Config.under_approximation then false else raise Smt.SMT_unknown + in (* if time <> "" then Utils.Statistics.update_statistics ("FOS: CheckSat: " ^ time) (Sys.time () -. t); *) diff --git a/GillianCore/smt/smt.ml b/GillianCore/smt/smt.ml index 9a3e59623..9f408cfb0 100644 --- a/GillianCore/smt/smt.ml +++ b/GillianCore/smt/smt.ml @@ -6,6 +6,10 @@ open Syntaxes.Option (* open Ctx *) module L = Logging +exception SMT_error of string + +let exceptf fmt = Fmt.kstr (fun s -> raise (SMT_error s)) fmt + let z3_config = [ ("model", "true"); @@ -350,7 +354,7 @@ let encode_type (t : Type.t) = | ListType -> Type_operations.List.construct | TypeType -> Type_operations.Type.construct | SetType -> Type_operations.Set.construct - with _ -> Fmt.failwith "DEATH: encode_type with arg: %a" Type.pp t + with _ -> exceptf "DEATH: encode_type with arg: %a" Type.pp t module Encoding = struct type kind = @@ -449,7 +453,7 @@ module Encoding = struct | BooleanType -> Bool.construct | ListType -> List.construct | UndefinedType | NullType | EmptyType | NoneType | SetType -> - Fmt.failwith "Cannot simple-wrap value of type %s" + exceptf "Cannot simple-wrap value of type %s" (Gil_syntax.Type.str typ) in construct expr @@ -470,7 +474,7 @@ module Encoding = struct match kind with | Native SetType -> expr | Extended_wrapped -> Ext_lit_operations.Gil_set.access expr - | _ -> failwith "wrong encoding of set" + | _ -> exceptf "wrong encoding of set" let get_string = get_native ~accessor:Lit_operations.String.access end @@ -561,8 +565,7 @@ let rec encode_lit (lit : Literal.t) : Encoding.t = let args = List.map (fun lit -> simple_wrap (encode_lit lit)) lits in list args >- ListType | Constant _ -> raise (Exceptions.Unsupported "Z3 encoding: constants") - with Failure msg -> - Fmt.failwith "DEATH: encode_lit %a. %s" Literal.pp lit msg + with Failure msg -> exceptf "DEATH: encode_lit %a. %s" Literal.pp lit msg let encode_equality (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t = let open Encoding in @@ -578,7 +581,7 @@ let encode_equality (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t = else eq p1.expr p2.expr | Simple_wrapped, Simple_wrapped | Extended_wrapped, Extended_wrapped -> eq p1.expr p2.expr - | Native _, Native _ -> failwith "incompatible equality, type error!" + | Native _, Native _ -> exceptf "incompatible equality, type error!" | Simple_wrapped, Native _ | Native _, Simple_wrapped -> eq (simple_wrap p1) (simple_wrap p2) | Extended_wrapped, _ | _, Extended_wrapped -> @@ -652,7 +655,7 @@ let encode_binop (op : BinOp.t) (p1 : Encoding.t) (p2 : Encoding.t) : Encoding.t | M_atan2 | M_pow | StrCat -> - Fmt.failwith "SMT encoding: Costruct not supported yet - binop: %s" + exceptf "SMT encoding: Costruct not supported yet - binop: %s" (BinOp.str op) let encode_unop ~llen_lvars ~e (op : UnOp.t) le = @@ -747,7 +750,7 @@ let encode_quantified_expr match encode_expr ~gamma ~llen_lvars ~list_elem_vars assertion with | { kind = Native BooleanType; expr; consts; extra_asrts } -> (expr, consts, extra_asrts) - | _ -> failwith "the thing inside forall is not boolean!" + | _ -> exceptf "the thing inside forall is not boolean!" in let quantified_vars = quantified_vars @@ -788,7 +791,7 @@ let rec encode_logical_expression in make_const ~typ kind var | ALoc var -> native_const ObjectType var - | PVar _ -> failwith "HORROR: Program variable in pure formula" + | PVar _ -> exceptf "HORROR: Program variable in pure formula" | UnOp (op, le) -> encode_unop ~llen_lvars ~e:le op (f le) | BinOp (le1, op, le2) -> encode_binop op (f le1) (f le2) | NOp (SetUnion, les) -> @@ -1093,7 +1096,7 @@ let lift_model match x with | LVar x -> x | _ -> - failwith "INTERNAL ERROR: SMT lifting of a non-logical variable" + exceptf "INTERNAL ERROR: SMT lifting of a non-logical variable" in let v = lift_val x in let () = diff --git a/GillianCore/smt/smt.mli b/GillianCore/smt/smt.mli index 18cebadeb..7f3e092d7 100644 --- a/GillianCore/smt/smt.mli +++ b/GillianCore/smt/smt.mli @@ -1,6 +1,7 @@ open Gil_syntax exception SMT_unknown +exception SMT_error of string val exec_sat : Expr.Set.t -> (string, Type.t) Hashtbl.t -> Sexplib.Sexp.t option val is_sat : Expr.Set.t -> (string, Type.t) Hashtbl.t -> bool From d016230236db474a6cb58797331d3f9cf40bdd37 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 9 Nov 2025 15:07:18 +0000 Subject: [PATCH 24/29] don't crash with inconsistent loop ids if outside verif Signed-off-by: Sacha Ayoun --- .../general_semantics/general/g_interpreter.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml index f9bd1fc54..6bfce9727 100644 --- a/GillianCore/engine/general_semantics/general/g_interpreter.ml +++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml @@ -453,12 +453,13 @@ struct raise (Interpreter_error (List.map (fun x -> Exec_err.EState x) errs, s)) let check_loop_ids actual expected = - match actual = expected with - | false -> - Fmt.failwith - "Malformed loop structure: current loops: %a; expected loops: %a" - pp_str_list actual pp_str_list expected - | true -> () + if Exec_mode.is_verification_exec !Config.current_exec_mode then + match actual = expected with + | false -> + Fmt.failwith + "Malformed loop structure: current loops: %a; expected loops: %a" + pp_str_list actual pp_str_list expected + | true -> () let rec loop_ids_to_frame_on_at_the_end end_ids start_ids = if end_ids = start_ids then [] From bf6eb31059655b77589afe73188f943a6913d2c8 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 9 Nov 2025 15:07:28 +0000 Subject: [PATCH 25/29] more precise analysis failure message Signed-off-by: Sacha Ayoun --- GillianCore/utils/gillian_result.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/GillianCore/utils/gillian_result.ml b/GillianCore/utils/gillian_result.ml index 8ba05571b..8bed19859 100644 --- a/GillianCore/utils/gillian_result.ml +++ b/GillianCore/utils/gillian_result.ml @@ -53,7 +53,10 @@ module Error = struct msgs | true, AnalysisFailures es -> let len = List.length es in - Fmt.pf fmt "%d analysis failure%s!" len (if len > 1 then "s" else "") + Fmt.pf fmt "%d analysis failure%s!\n%a" len + (if len > 1 then "s" else "") + (Fmt.Dump.list Yojson.Safe.pp) + (List.map analysis_failure_to_yojson es) | false, CompilationError { msg; loc; _ } -> Fmt.pf fmt "Error during compilation, at%a.\n%s" Location.pp_full loc msg From 7a8d8811251e5e073dcdcdcf64b8162719b7aac0 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Tue, 11 Nov 2025 21:32:42 +0000 Subject: [PATCH 26/29] CGEnv is just agreement Signed-off-by: Sacha Ayoun --- transformers/lib/prebuilt/c_states/CGEnv.ml | 76 ++++++--------------- 1 file changed, 20 insertions(+), 56 deletions(-) diff --git a/transformers/lib/prebuilt/c_states/CGEnv.ml b/transformers/lib/prebuilt/c_states/CGEnv.ml index ba877c8cd..4a266af73 100644 --- a/transformers/lib/prebuilt/c_states/CGEnv.ml +++ b/transformers/lib/prebuilt/c_states/CGEnv.ml @@ -1,62 +1,26 @@ open Gil_syntax -open Gillian.Monadic -module DR = Delayed_result module Global_env = Cgil_lib.Global_env let init_data = ref Global_env.empty let set_init_data d = init_data := d -module M : States.MyMonadicSMemory.S with type t = Global_env.t = struct - type t = Global_env.t [@@deriving yojson] - type err_t = unit [@@deriving show, yojson] - type action = GetDef - type pred = unit [@@deriving show, yojson] - - let pp = Global_env.pp - - let action_from_str = function - | "getdef" -> Some GetDef - | _ -> None - - let action_to_str GetDef = "getdef" - let pred_from_str _ = None - let pred_to_str () = failwith "No pred in GEnv" - let empty () = !init_data - - (* Execute action *) - let execute_action GetDef s args = - match args with - | [ (Expr.Lit (Loc loc) | Expr.ALoc loc | Expr.LVar loc) ] -> ( - match Global_env.find_def_opt s loc with - | Some def -> - let v = Global_env.serialize_def def in - DR.ok (s, [ Expr.Lit (Loc loc); Expr.Lit v ]) - | None -> - (* If we can't find a function, in UX mode we give up, while in OX mode we - signal. *) - if !Gillian.Utils.Config.under_approximation then Delayed.vanish () - else - Fmt.failwith "execute_genvgetdef: couldn't find %s\nGENV:\n%a" loc - Global_env.pp s) - | _ -> failwith "Invalid arguments for GetDef" - - let consume () _ _ = failwith "Invalid C GEnv consume" - let produce () _ _ = failwith "Invalid C GEnv produce" - let compose _ _ = Delayed.vanish () (* TODO *) - let is_exclusively_owned _ _ = Delayed.return false - let is_empty _ = false - let is_concrete _ = false - let instantiate _ = (Global_env.empty, []) - - (* Core predicates: pred * ins * outs, converted to Asrt.CorePred *) - let assertions _ = [] - let assertions_others _ = [] - let can_fix () = false - let get_fixes () = [] - let lvars _ = Gillian.Utils.Containers.SS.empty - let alocs _ = Gillian.Utils.Containers.SS.empty - let substitution_in_place _ s = Delayed.return s - let get_recovery_tactic _ = Gillian.General.Recovery_tactic.none - let list_actions () = [ (GetDef, [], []) ] - let list_preds () = [] -end +module M : States.MyMonadicSMemory.S = + States.Mapper.Make + (struct + let action_substitutions = [ ("getdef", "load") ] + let pred_substitutions = [ ("def", "value") ] + end) + (struct + include States.PMap.Make (States.PMap.ALocImpl) (States.Agreement) + + let empty () : t = + let map = + Cgil_lib.String_map.fold + (fun k v acc -> + States.MyUtils.SMap.add k + (Some (Expr.Lit (Global_env.serialize_def v))) + acc) + !init_data States.MyUtils.SMap.empty + in + (map, None) + end) From 349804491a5529bb0018651c6bb65e4e91a154a4 Mon Sep 17 00:00:00 2001 From: N1ark Date: Thu, 13 Nov 2025 15:14:01 +0000 Subject: [PATCH 27/29] Add `--ignore` to biab --- GillianCore/command_line/act_console.ml | 8 +++- GillianCore/engine/BiAbduction/Abductor.ml | 50 ++++++++++++++-------- GillianCore/utils/config.ml | 1 + 3 files changed, 40 insertions(+), 19 deletions(-) diff --git a/GillianCore/command_line/act_console.ml b/GillianCore/command_line/act_console.ml index a6704fbc9..abf1c4f76 100644 --- a/GillianCore/command_line/act_console.ml +++ b/GillianCore/command_line/act_console.ml @@ -23,6 +23,10 @@ struct let doc = "Emit specs to stdout, useful for testing." in Arg.(value & flag & info [ "specs-to-stdout" ] ~doc) + let ignored_procs = + let doc = "Procs to ignore" in + Arg.(value & opt_all string [] & info [ "ignore" ] ~doc) + let parse_eprog file files already_compiled = if not already_compiled then let () = @@ -110,6 +114,7 @@ struct incremental bi_unroll_depth bi_no_spec_depth + ignored_specs () = let () = Config.current_exec_mode := BiAbduction in let () = PC.initialize BiAbduction in @@ -119,6 +124,7 @@ struct let () = Config.bi_no_spec_depth := bi_no_spec_depth in let () = Config.specs_to_stdout := specs_to_stdout in let () = Config.max_branching := bi_unroll_depth in + let () = Config.bi_ignore_procs := ignored_specs in let () = Config.under_approximation := true in let r = process_files files already_compiled outfile_opt should_emit_specs @@ -132,7 +138,7 @@ struct Term.( const act $ files $ already_compiled $ output_gil $ no_heap $ stats $ should_emit_specs $ specs_to_stdout $ incremental $ bi_unroll_depth - $ bi_no_spec_depth) + $ bi_no_spec_depth $ ignored_procs) let act_info = let doc = diff --git a/GillianCore/engine/BiAbduction/Abductor.ml b/GillianCore/engine/BiAbduction/Abductor.ml index 678c20bd7..f5cf384de 100644 --- a/GillianCore/engine/BiAbduction/Abductor.ml +++ b/GillianCore/engine/BiAbduction/Abductor.ml @@ -288,6 +288,9 @@ struct let rec run_tests_aux tests succ_specs err_specs bug_specs i = match tests with | [] -> (succ_specs, err_specs, bug_specs) + | test :: rest when List.mem test.name !Config.bi_ignore_procs -> + Fmt.pr "Skipping %s... (%d/%d)\n@?" test.name i num_tests; + run_tests_aux rest succ_specs err_specs bug_specs (i + 1) | test :: rest -> let rec part3 = function | [] -> ([], [], []) @@ -348,30 +351,41 @@ struct (fun Spec.{ spec_name = name1; _ } Spec.{ spec_name = name2; _ } -> String.compare name1 name2) in - let bug_specs_txt = - Format.asprintf "@[BUG SPECS:@\n%a@]@\n" - Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) - (sort_specs bug_specs) - in - let error_specs_txt = - Format.asprintf "@[ERROR SPECS:@\n%a@]@\n" - Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) - (sort_specs error_specs) - in - let normal_specs_txt = - Format.asprintf "@[SUCCESSFUL SPECS:@\n%a@]@\n" - Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) - (sort_specs succ_specs) - in + Fmt.pr "Ok 3 - %f@." (Sys.time ()); if !Config.specs_to_stdout then ( + let bug_specs_txt = + Format.asprintf "@[BUG SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs bug_specs) + in + let error_specs_txt = + Format.asprintf "@[ERROR SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs error_specs) + in + let normal_specs_txt = + Format.asprintf "@[SUCCESSFUL SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs succ_specs) + in L.print_to_all bug_specs_txt; L.print_to_all error_specs_txt; L.print_to_all normal_specs_txt) else ( - L.normal (fun m -> m "%s" bug_specs_txt); - L.normal (fun m -> m "%s" error_specs_txt); - L.normal (fun m -> m "%s" normal_specs_txt)); + L.normal (fun m -> + m "@[BUG SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs bug_specs)); + L.normal (fun m -> + m "@[SUCCESSFUL SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs succ_specs)); + L.normal (fun m -> + m "@[SUCCESSFUL SPECS:@\n%a@]@\n" + Fmt.(list ~sep:(any "@\n") (MP.pp_spec ~preds:prog.preds)) + (sort_specs succ_specs))); + (* This is a hack to not count auxiliary functions that are bi-abduced *) let len_succ = List.length succ_specs in diff --git a/GillianCore/utils/config.ml b/GillianCore/utils/config.ml index fb71dfd92..5070cae60 100644 --- a/GillianCore/utils/config.ml +++ b/GillianCore/utils/config.ml @@ -64,6 +64,7 @@ let bi_dflt = ref true let bi_unfold_depth = ref 1 let bi_unroll_depth = ref 1 let bi_no_spec_depth = ref 0 +let bi_ignore_procs : string list ref = ref [] let delay_entailment = ref true (* If true, will dump a folder containing all smt queries made to the solver *) From e7a254e50939f4d222244cc6d4dbe04d9d4ff1c7 Mon Sep 17 00:00:00 2001 From: N1ark Date: Thu, 13 Nov 2025 15:14:41 +0000 Subject: [PATCH 28/29] Fix CGEnv for bi-abduction --- transformers/lib/prebuilt/c_states/CGEnv.ml | 38 ++++++++++++++------- 1 file changed, 26 insertions(+), 12 deletions(-) diff --git a/transformers/lib/prebuilt/c_states/CGEnv.ml b/transformers/lib/prebuilt/c_states/CGEnv.ml index 4a266af73..309e05baa 100644 --- a/transformers/lib/prebuilt/c_states/CGEnv.ml +++ b/transformers/lib/prebuilt/c_states/CGEnv.ml @@ -1,26 +1,40 @@ +open Utils +open Gillian.Monadic open Gil_syntax module Global_env = Cgil_lib.Global_env let init_data = ref Global_env.empty let set_init_data d = init_data := d -module M : States.MyMonadicSMemory.S = - States.Mapper.Make +module EnvAg = struct + include Agreement + + let execute_action a ins s = + let open Delayed.Syntax in + let* res = execute_action a ins s in + match (a, res) with + | Load, Error e when can_fix e && !Gillian.Utils.Config.under_approximation + -> Delayed.vanish () + | _ -> Delayed.return res + + let get_fixes _ = [] + let assertions _ = [] +end + +module M : MyMonadicSMemory = + Mapper (struct let action_substitutions = [ ("getdef", "load") ] let pred_substitutions = [ ("def", "value") ] end) (struct - include States.PMap.Make (States.PMap.ALocImpl) (States.Agreement) + include OpenALocPMap (EnvAg) let empty () : t = - let map = - Cgil_lib.String_map.fold - (fun k v acc -> - States.MyUtils.SMap.add k - (Some (Expr.Lit (Global_env.serialize_def v))) - acc) - !init_data States.MyUtils.SMap.empty - in - (map, None) + Cgil_lib.String_map.fold + (fun k v acc -> + States.MyUtils.SMap.add k + (Some (Expr.Lit (Global_env.serialize_def v))) + acc) + !init_data States.MyUtils.SMap.empty end) From e16c0e16990af97b1f6b4fc58f148b1ca9211c0d Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Fri, 21 Nov 2025 10:41:10 +0000 Subject: [PATCH 29/29] minor Signed-off-by: Sacha Ayoun --- transformers/lib/states/bi_abd.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/transformers/lib/states/bi_abd.ml b/transformers/lib/states/bi_abd.ml index df71a965f..e13e54e2a 100644 --- a/transformers/lib/states/bi_abd.ml +++ b/transformers/lib/states/bi_abd.ml @@ -93,13 +93,13 @@ module Make (Mem : MyMonadicSMemory.S) : let get_recovery_tactic = Mem.get_recovery_tactic let can_fix e = Mem.can_fix e + (* The rest of the functions remain unimplemented as Bi_abd makes no sense being an input to other transformers. *) + let get_fixes _ = failwith "Bi_abd state should not be used as an input to the bi-abduction state \ module. That one is legacy." - (* Assertions *) - let assertions_others _ = failwith "Should not be transforming bi-abd state to assertions, only its first \ @@ -110,8 +110,6 @@ module Make (Mem : MyMonadicSMemory.S) : "Should not be transforming bi-abd state to assertions, only its first \ component" - (* The rest of the functions remain unimplemented as Bi_abd makes no sense being an input to other transformers. *) - let instantiate _ = failwith "Bi_abd state should not be used as an input state"