|
|
@ -18,27 +18,6 @@ include IdMap
|
|
|
|
let pp fmt astate =
|
|
|
|
let pp fmt astate =
|
|
|
|
IdMap.pp ~pp_value:AccessPath.Raw.pp fmt astate
|
|
|
|
IdMap.pp ~pp_value:AccessPath.Raw.pp fmt astate
|
|
|
|
|
|
|
|
|
|
|
|
let (<=) ~lhs ~rhs =
|
|
|
|
|
|
|
|
if phys_equal lhs rhs
|
|
|
|
|
|
|
|
then true
|
|
|
|
|
|
|
|
else
|
|
|
|
|
|
|
|
try
|
|
|
|
|
|
|
|
IdMap.for_all
|
|
|
|
|
|
|
|
(fun id lhs_ap ->
|
|
|
|
|
|
|
|
let rhs_ap = IdMap.find id rhs in
|
|
|
|
|
|
|
|
let eq = AccessPath.Raw.equal lhs_ap rhs_ap in
|
|
|
|
|
|
|
|
if not eq && Config.debug_exceptions
|
|
|
|
|
|
|
|
then
|
|
|
|
|
|
|
|
failwithf "Id %a maps to both %a and %a@."
|
|
|
|
|
|
|
|
Var.pp id
|
|
|
|
|
|
|
|
AccessPath.Raw.pp lhs_ap
|
|
|
|
|
|
|
|
AccessPath.Raw.pp rhs_ap;
|
|
|
|
|
|
|
|
eq)
|
|
|
|
|
|
|
|
lhs
|
|
|
|
|
|
|
|
with Not_found -> false
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(* in principle, could do a join here if the access paths have the same root. but they should
|
|
|
|
|
|
|
|
always be equal if we are using the map correctly *)
|
|
|
|
|
|
|
|
let check_invariant ap1 ap2 = function
|
|
|
|
let check_invariant ap1 ap2 = function
|
|
|
|
| Var.ProgramVar pvar when Pvar.is_frontend_tmp pvar ->
|
|
|
|
| Var.ProgramVar pvar when Pvar.is_frontend_tmp pvar ->
|
|
|
|
(* Sawja reuses temporary variables which sometimes breaks this invariant *)
|
|
|
|
(* Sawja reuses temporary variables which sometimes breaks this invariant *)
|
|
|
@ -52,6 +31,18 @@ let check_invariant ap1 ap2 = function
|
|
|
|
AccessPath.Raw.pp ap1
|
|
|
|
AccessPath.Raw.pp ap1
|
|
|
|
AccessPath.Raw.pp ap2
|
|
|
|
AccessPath.Raw.pp ap2
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let (<=) ~lhs ~rhs =
|
|
|
|
|
|
|
|
if phys_equal lhs rhs
|
|
|
|
|
|
|
|
then true
|
|
|
|
|
|
|
|
else
|
|
|
|
|
|
|
|
IdMap.for_all
|
|
|
|
|
|
|
|
(fun id lhs_ap ->
|
|
|
|
|
|
|
|
let rhs_has = IdMap.mem id rhs in
|
|
|
|
|
|
|
|
if rhs_has && Config.debug_exceptions
|
|
|
|
|
|
|
|
then check_invariant lhs_ap (IdMap.find id rhs) id;
|
|
|
|
|
|
|
|
rhs_has)
|
|
|
|
|
|
|
|
lhs
|
|
|
|
|
|
|
|
|
|
|
|
let join astate1 astate2 =
|
|
|
|
let join astate1 astate2 =
|
|
|
|
if phys_equal astate1 astate2
|
|
|
|
if phys_equal astate1 astate2
|
|
|
|
then astate1
|
|
|
|
then astate1
|
|
|
|