Skip to content

Commit

Permalink
Remove FSpecVars??
Browse files Browse the repository at this point in the history
  • Loading branch information
@N1ark
N1ark committed Sep 14, 2024
1 parent 5f77004 commit 02c2593
Show file tree
Hide file tree
Showing 7 changed files with 72 additions and 115 deletions.
30 changes: 12 additions & 18 deletions Gillian-C/lib/MonadicSMemory.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -903,21 +903,19 @@ let get_fixes err =
let new_var_e1 = Expr.LVar new_var1 in
let new_var2 = LVar.alloc () in
let new_var_e2 = Expr.LVar new_var2 in
let set = SS.add new_var2 (SS.singleton new_var1) in
let value = Expr.EList [ new_var_e1; new_var_e2 ] in
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
[
( [
single ~loc ~ofs ~chunk ~sval:value ~perm;
Asrt.Types
[ (new_var_e1, Type.ObjectType); (new_var_e2, Type.IntType) ];
],
set );
([ single ~loc ~ofs ~chunk ~sval:null_ptr ~perm ], SS.empty);
[
single ~loc ~ofs ~chunk ~sval:value ~perm;
Asrt.Types
[ (new_var_e1, Type.ObjectType); (new_var_e2, Type.IntType) ];
];
[ single ~loc ~ofs ~chunk ~sval:null_ptr ~perm ];
]
| _ ->
let type_str, type_gil =
Expand All @@ -928,23 +926,19 @@ let get_fixes err =
| _ -> (int_type, Type.IntType)
in
let new_var = LVar.alloc () in
let set = SS.singleton new_var in
let new_var_e = Expr.LVar new_var in
let value = Expr.EList [ Expr.string type_str; new_var_e ] in
[
( [
single ~loc ~ofs ~chunk ~sval:value ~perm;
Asrt.Types [ (new_var_e, type_gil) ];
],
set );
[
single ~loc ~ofs ~chunk ~sval:value ~perm;
Asrt.Types [ (new_var_e, type_gil) ];
];
]
in
(* Additional fix for store operation to handle case of unitialized memory *)
let fixes =
if is_store then
( [ hole ~loc ~low:ofs ~high:(offset_by_chunk ofs chunk) ~perm ],
SS.empty )
:: fixes
[ hole ~loc ~low:ofs ~high:(offset_by_chunk ofs chunk) ~perm ] :: fixes
else fixes
in
fixes
Expand All @@ -961,7 +955,7 @@ let get_fixes err =
| InvalidLocation loc ->
let new_loc = ALoc.alloc () in
let new_expr = Expr.ALoc new_loc in
[ ([ Asrt.Pure (Eq (new_expr, loc)) ], SS.empty) ]
[ [ Asrt.Pure (Eq (new_expr, loc)) ] ]
| SHeapTreeErr
{
at_locations;
Expand Down
83 changes: 33 additions & 50 deletions Gillian-JS/lib/Semantics/JSILSMemory.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -597,7 +597,7 @@ module M = struct
let prop_abduce_none_in_js = [ "@call" ]
let prop_abduce_both_in_js = [ "hasOwnProperty" ]

type fix_result = Asrt.t list * Containers.SS.t
type fix_result = Asrt.t list

let complete_fix_js (i_fix : i_fix_t) : fix_result list =
match i_fix with
Expand All @@ -607,11 +607,10 @@ module M = struct
however it only seemed to add the binding without creating any state, so did it really
"do" anything? Bi-abduction is broken for Gillian-JS anyways. *)
let al = ALoc.alloc () in
[ ([ Asrt.Pure (Eq (ALoc al, v)) ], Containers.SS.empty) ]
[ [ Asrt.Pure (Eq (ALoc al, v)) ] ]
| FCell (l, p) -> (
let none_fix () =
( [ Asrt.GA (JSILNames.aCell, [ l; p ], [ Lit Nono ]) ],
Containers.SS.empty )
[ Asrt.GA (JSILNames.aCell, [ l; p ], [ Lit Nono ]) ]
in

let some_fix () =
Expand All @@ -632,13 +631,12 @@ module M = struct
Lit (Bool true);
]
in
( [
Asrt.GA (JSILNames.aCell, [ l; p ], [ descriptor ]);
Asrt.Pure asrt_empty;
Asrt.Pure asrt_none;
Asrt.Pure asrt_list;
],
Containers.SS.singleton vvar )
[
Asrt.GA (JSILNames.aCell, [ l; p ], [ descriptor ]);
Asrt.Pure asrt_empty;
Asrt.Pure asrt_none;
Asrt.Pure asrt_list;
]
in

match p with
Expand All @@ -651,64 +649,53 @@ module M = struct
let al = ALoc.alloc () in
let mloc = Expr.ALoc al in
[
( [
Asrt.Pure (Eq (ALoc al, l));
Asrt.GA (JSILNames.aMetadata, [ l ], [ mloc ]);
Asrt.GA (JSILNames.aMetadata, [ mloc ], [ Lit Null ]);
Asrt.GA
( JSILNames.aCell,
[ mloc; Lit (String "@class") ],
[ Lit (String "Object") ] );
Asrt.GA
( JSILNames.aCell,
[ mloc; Lit (String "@extensible") ],
[ Lit (Bool true) ] );
Asrt.GA
( JSILNames.aCell,
[ mloc; Lit (String "@proto") ],
[ Lit (Loc JS2JSIL_Helpers.locObjPrototype) ] );
],
Containers.SS.empty );
[
Asrt.Pure (Eq (ALoc al, l));
Asrt.GA (JSILNames.aMetadata, [ l ], [ mloc ]);
Asrt.GA (JSILNames.aMetadata, [ mloc ], [ Lit Null ]);
Asrt.GA
( JSILNames.aCell,
[ mloc; Lit (String "@class") ],
[ Lit (String "Object") ] );
Asrt.GA
( JSILNames.aCell,
[ mloc; Lit (String "@extensible") ],
[ Lit (Bool true) ] );
Asrt.GA
( JSILNames.aCell,
[ mloc; Lit (String "@proto") ],
[ Lit (Loc JS2JSIL_Helpers.locObjPrototype) ] );
];
]
| FPure f -> [ ([ Asrt.Pure f ], Containers.SS.empty) ]
| FPure f -> [ [ Asrt.Pure f ] ]

(* Fix completion: simple *)
let complete_fix_jsil (i_fix : i_fix_t) : fix_result list =
match i_fix with
| FLoc v ->
(* Get a fresh location *)
let al = ALoc.alloc () in
[ ([ Asrt.Pure (Eq (ALoc al, v)) ], Containers.SS.empty) ]
[ [ Asrt.Pure (Eq (ALoc al, v)) ] ]
| FCell (l, p) ->
(* Fresh variable to denote the property value *)
let vvar = LVar.alloc () in
let v : vt = LVar vvar in
(* Value is not none - we always bi-abduce presence *)
let not_none : Formula.t = Not (Eq (v, Lit Nono)) in
[
( [ Asrt.GA (JSILNames.aCell, [ l; p ], [ v ]); Asrt.Pure not_none ],
Containers.SS.singleton vvar );
]
[ [ Asrt.GA (JSILNames.aCell, [ l; p ], [ v ]); Asrt.Pure not_none ] ]
| FMetadata l ->
(* Fresh variable to denote the property value *)
let vvar = LVar.alloc () in
let v : vt = LVar vvar in
let not_none : Formula.t = Not (Eq (v, Lit Nono)) in
[
( [ Asrt.GA (JSILNames.aMetadata, [ l ], [ v ]); Asrt.Pure not_none ],
Containers.SS.singleton vvar );
]
| FPure f -> [ ([ Asrt.Pure f ], Containers.SS.empty) ]
[ [ Asrt.GA (JSILNames.aMetadata, [ l ], [ v ]); Asrt.Pure not_none ] ]
| FPure f -> [ [ Asrt.Pure f ] ]

(* An error can have multiple fixes *)
let get_fixes (err : err_t) : fix_result list =
let pp_fix_result ft res =
let open Fmt in
let fixes, svars = res in
pf ft "@[<v 2>@[<h>[[ %a ]]@]@\n@[<h>spec vars: %a@]@]"
(list ~sep:comma Asrt.pp) fixes
(iter ~sep:comma Containers.SS.iter string)
svars
pf ft "@[<v 2>@[<h>[[ %a ]]@]@\n@]" (list ~sep:comma Asrt.pp) res
in
let _, fixes, _ = err in
L.verbose (fun m ->
Expand All @@ -727,11 +714,7 @@ module M = struct
let completed_ifixes = List_utils.list_product completed_ifixes in
let completed_ifixes : fix_result list =
List.map
(fun fixes ->
List.fold_right
(fun (fix, svars) (fix', svars') ->
(fix @ fix', Containers.SS.union svars svars'))
fixes ([], Containers.SS.empty))
(fun fixes -> List.fold_right List.append fixes [])
completed_ifixes
in

Expand Down
2 changes: 1 addition & 1 deletion GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ module type S = sig
val pp_err : Format.formatter -> err_t -> unit
val get_failing_constraint : err_t -> Formula.t
val can_fix : err_t -> bool
val get_fixes : err_t -> (Asrt.t list * Containers.SS.t) list
val get_fixes : err_t -> Asrt.t list list
val sure_is_nonempty : t -> bool
end

Expand Down
2 changes: 1 addition & 1 deletion GillianCore/engine/symbolic_semantics/SMemory.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ module type S = sig
val get_recovery_tactic : t -> err_t -> vt Recovery_tactic.t
val pp_err : Format.formatter -> err_t -> unit
val get_failing_constraint : err_t -> Formula.t
val get_fixes : err_t -> (Asrt.t list * Containers.SS.t) list
val get_fixes : err_t -> Asrt.t list list
val can_fix : err_t -> bool
val sure_is_nonempty : t -> bool

Expand Down
63 changes: 22 additions & 41 deletions GillianCore/engine/symbolic_semantics/SState.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ module Make (SMemory : SMemory.S) :

type variants_t = (string, Expr.t option) Hashtbl.t [@@deriving yojson]
type init_data = SMemory.init_data
type fix_t = Fix of Asrt.t | FSpecVars of SS.t
type fix_t = Asrt.t
type err_t = (m_err_t, vt) StateErr.t [@@deriving yojson, show]
type action_ret = (t * vt list, err_t) result list

Expand Down Expand Up @@ -677,12 +677,7 @@ module Make (SMemory : SMemory.S) :
let mem_constraints ({ heap; _ } : t) : Formula.t list =
SMemory.mem_constraints heap

let pp_fix fmt = function
| Fix mf -> Fmt.pf fmt "Fix(%a)" Asrt.pp mf
| FSpecVars vs ->
Fmt.pf fmt "FSVar(@[<h>%a@])"
(Fmt.iter ~sep:Fmt.comma SS.iter Fmt.string)
vs
let pp_fix = Asrt.pp

let get_recovery_tactic (state : t) (errs : err_t list) : vt Recovery_tactic.t
=
Expand Down Expand Up @@ -723,21 +718,19 @@ module Make (SMemory : SMemory.S) :

let normalise_fix (pfs : PFS.t) (gamma : Type_env.t) (fix : fix_t list) :
fix_t list option =
let gafixes, pfs', spec_vars, types, asrts =
let gafixes, pfs', types =
List.fold_right
(fun fix (mfix, pfs, spec_vars, types, asrts) ->
(fun fix (mfix, pfs, types) ->
match fix with
| Fix Emp | Fix (Pure True) -> (mfix, pfs, spec_vars, types, asrts)
| Fix (GA _ as ga) -> (ga :: mfix, pfs, spec_vars, types, asrts)
| Fix (Types ts) -> (mfix, pfs, spec_vars, ts @ types, asrts)
| Fix (Pure pf') -> (mfix, pf' :: pfs, spec_vars, types, asrts)
| Fix (Pred _) | Fix (Wand _) | Fix (Star _) ->
| Asrt.Emp | Pure True -> (mfix, pfs, types)
| GA _ as ga -> (ga :: mfix, pfs, types)
| Types ts -> (mfix, pfs, ts @ types)
| Pure pf' -> (mfix, pf' :: pfs, types)
| Pred _ | Wand _ | Star _ ->
raise
(Exceptions.Impossible
"Invalid fix type: Pred, Wand or Star found")
| FSpecVars spec_vars' ->
(mfix, pfs, SS.union spec_vars' spec_vars, types, asrts))
fix ([], [], SS.empty, [], [])
"Invalid fix type: Pred, Wand or Star found"))
fix ([], [], [])
in

(* Check SAT for some notion of checking SAT *)
Expand All @@ -749,13 +742,9 @@ module Make (SMemory : SMemory.S) :
None
| Some gamma'
when FOSolver.check_satisfiability (PFS.to_list pfs @ pfs') gamma' ->
let pfixes = List.map (fun pfix -> Fix (Pure pfix)) pfs' in
let mfixes = List.map (fun fix -> Fix fix) gafixes in
let ftys = if types = [] then [] else [ Fix (Types types) ] in
let sfixes =
if SS.is_empty spec_vars then [] else [ FSpecVars spec_vars ]
in
Some (ftys @ sfixes @ pfixes @ asrts @ mfixes)
let pfixes = List.map (fun pfix -> Asrt.Pure pfix) pfs' in
let ftys = if types = [] then [] else [ Asrt.Types types ] in
Some (ftys @ pfixes @ gafixes)
| Some _ ->
L.verbose (fun m -> m "Warning: invalid fix.");
None
Expand All @@ -769,14 +758,9 @@ module Make (SMemory : SMemory.S) :
let { pfs; gamma; _ } = state in
let one_step_fixes : fix_t list list =
match err with
| EMem err ->
List.map
(fun (fixes, spec_vars) ->
List.map (fun pf -> Fix pf) fixes
@ if spec_vars == SS.empty then [] else [ FSpecVars spec_vars ])
(SMemory.get_fixes err)
| EMem err -> SMemory.get_fixes err
| EPure f ->
let result = [ [ Fix (Pure f) ] ] in
let result = [ [ Asrt.Pure f ] ] in
L.verbose (fun m ->
m "@[<v 2>Memory: Fixes found:@\n%a@]"
(Fmt.list ~sep:(Fmt.any "@\n") pp_fixes)
Expand All @@ -786,7 +770,7 @@ module Make (SMemory : SMemory.S) :
let result =
(List.map
(List.map (function
| Asrt.Pure fix -> Fix (Pure fix)
| Asrt.Pure _ as fix -> fix
| _ ->
raise
(Exceptions.Impossible
Expand Down Expand Up @@ -837,30 +821,27 @@ module Make (SMemory : SMemory.S) :
let { heap; store; pfs; gamma; spec_vars } = this_state in
match fix with
(* Apply fix in memory - this may change the pfs and gamma *)
| Fix Emp -> [ this_state ]
| Fix (GA (name, ins, outs)) ->
| Asrt.Emp -> [ this_state ]
| GA (name, ins, outs) ->
L.verbose (fun m -> m "SState: before applying fixes %a" pp state);
let pc = Gpc.make ~matching:false ~pfs ~gamma () in
let+ Gbranch.{ value = heap; pc } =
SMemory.produce name heap pc (ins @ outs)
in
{ heap; store; pfs = pc.pfs; gamma = pc.gamma; spec_vars }
| Fix (Pure f) ->
| Pure f ->
PFS.extend pfs f;
[ this_state ]
| Fix (Types types) -> (
| Types types -> (
let gamma' = Typing.reverse_type_lexpr true gamma types in
match gamma' with
| None -> []
| Some gamma' ->
Type_env.extend gamma gamma';
[ this_state ])
| Fix (Star _) | Fix (Wand _) | Fix (Pred _) ->
| Star _ | Wand _ | Pred _ ->
raise
(Failure "DEATH: apply_fixes: Star, Wand, and Pred not implemented.")
| FSpecVars vars ->
let spec_vars = SS.union vars spec_vars in
[ { heap; store; pfs; gamma; spec_vars } ]
in

let result = List.fold_left apply_fix [ state ] fixes in
Expand Down
2 changes: 1 addition & 1 deletion GillianCore/monadic/MonadicSMemory.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ module type S = sig
val get_recovery_tactic : t -> err_t -> vt Recovery_tactic.t
val pp_err : Format.formatter -> err_t -> unit
val get_failing_constraint : err_t -> Formula.t
val get_fixes : err_t -> (Asrt.t list * Containers.SS.t) list
val get_fixes : err_t -> Asrt.t list list
val can_fix : err_t -> bool
val pp_by_need : Containers.SS.t -> Format.formatter -> t -> unit
val get_print_info : Containers.SS.t -> t -> Containers.SS.t * Containers.SS.t
Expand Down
5 changes: 2 additions & 3 deletions wisl/lib/semantics/wislSMemory.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -309,14 +309,13 @@ let get_fixes (err : err_t) =
| MissingResource (Cell, loc, Some ofs) ->
let new_var = LVar.alloc () in
let value = Expr.LVar new_var in
let set = SS.singleton new_var in
let loc = Expr.loc_from_loc_name loc in
let ga = WislLActions.str_ga WislLActions.Cell in
[ ([ Asrt.GA (ga, [ loc; ofs ], [ value ]) ], set) ]
[ [ Asrt.GA (ga, [ loc; ofs ], [ value ]) ] ]
| InvalidLocation loc ->
let new_loc = ALoc.alloc () in
let new_expr = Expr.ALoc new_loc in
[ ([ Asrt.Pure (Eq (new_expr, loc)) ], SS.empty) ]
[ [ Asrt.Pure (Eq (new_expr, loc)) ] ]
| _ -> []

let can_fix = function
Expand Down

0 comments on commit 02c2593

Please sign in to comment.