@ -1396,144 +1396,6 @@ let instr_sub_ids ~sub_id_binders f instr =
(* * apply [subst] to all id's in [instr], including binder id's *)
(* * apply [subst] to all id's in [instr], including binder id's *)
let instr_sub ( subst : subst ) instr = instr_sub_ids ~ sub_id_binders : true ( apply_sub subst ) instr
let instr_sub ( subst : subst ) instr = instr_sub_ids ~ sub_id_binders : true ( apply_sub subst ) instr
(* * compare expressions from different procedures without considering loc's, ident's, and pvar's.
the [ exp_map ] param gives a mapping of names used in the procedure of [ e1 ] to names used in the
procedure of [ e2 ] * )
let rec exp_compare_structural e1 e2 exp_map =
let compare_exps_with_map e1 e2 exp_map =
try
let e1_mapping = Exp . Map . find e1 exp_map in
( Exp . compare e1_mapping e2 , exp_map )
with Not_found ->
(* assume e1 and e2 equal, enforce by adding to [exp_map] *)
( 0 , Exp . Map . add e1 e2 exp_map )
in
match ( ( e1 : Exp . t ) , ( e2 : Exp . t ) ) with
| Var _ , Var _ ->
compare_exps_with_map e1 e2 exp_map
| UnOp ( o1 , e1 , to1 ) , UnOp ( o2 , e2 , to2 ) ->
let n = Unop . compare o1 o2 in
if n < > 0 then ( n , exp_map )
else
let n , exp_map = exp_compare_structural e1 e2 exp_map in
( ( if n < > 0 then n else [ % compare : Typ . t option ] to1 to2 ) , exp_map )
| BinOp ( o1 , e1 , f1 ) , BinOp ( o2 , e2 , f2 ) ->
let n = Binop . compare o1 o2 in
if n < > 0 then ( n , exp_map )
else
let n , exp_map = exp_compare_structural e1 e2 exp_map in
if n < > 0 then ( n , exp_map ) else exp_compare_structural f1 f2 exp_map
| Cast ( t1 , e1 ) , Cast ( t2 , e2 ) ->
let n , exp_map = exp_compare_structural e1 e2 exp_map in
( ( if n < > 0 then n else Typ . compare t1 t2 ) , exp_map )
| Lvar _ , Lvar _ ->
compare_exps_with_map e1 e2 exp_map
| Lfield ( e1 , f1 , t1 ) , Lfield ( e2 , f2 , t2 ) ->
let n , exp_map = exp_compare_structural e1 e2 exp_map in
( ( if n < > 0 then n
else
let n = Typ . Fieldname . compare f1 f2 in
if n < > 0 then n else Typ . compare t1 t2 )
, exp_map )
| Lindex ( e1 , f1 ) , Lindex ( e2 , f2 ) ->
let n , exp_map = exp_compare_structural e1 e2 exp_map in
if n < > 0 then ( n , exp_map ) else exp_compare_structural f1 f2 exp_map
| _ ->
( Exp . compare e1 e2 , exp_map )
let exp_typ_compare_structural ( e1 , t1 ) ( e2 , t2 ) exp_map =
let n , exp_map = exp_compare_structural e1 e2 exp_map in
( ( if n < > 0 then n else Typ . compare t1 t2 ) , exp_map )
(* * compare instructions from different procedures without considering loc's, ident's, and pvar's.
the [ exp_map ] param gives a mapping of names used in the procedure of [ instr1 ] to identifiers
used in the procedure of [ instr2 ] * )
let compare_structural_instr instr1 instr2 exp_map =
let id_typ_opt_compare_structural id_typ1 id_typ2 exp_map =
let id_typ_compare_structural ( id1 , typ1 ) ( id2 , typ2 ) =
let n , exp_map = exp_compare_structural ( Var id1 ) ( Var id2 ) exp_map in
if n < > 0 then ( n , exp_map ) else ( Typ . compare typ1 typ2 , exp_map )
in
match ( id_typ1 , id_typ2 ) with
| Some it1 , Some it2 ->
id_typ_compare_structural it1 it2
| None , None ->
( 0 , exp_map )
| None , _ ->
( - 1 , exp_map )
| _ , None ->
( 1 , exp_map )
in
let id_list_compare_structural ids1 ids2 exp_map =
let n = Int . compare ( List . length ids1 ) ( List . length ids2 ) in
if n < > 0 then ( n , exp_map )
else
List . fold2_exn
~ f : ( fun ( n , exp_map ) id1 id2 ->
if n < > 0 then ( n , exp_map ) else exp_compare_structural ( Var id1 ) ( Var id2 ) exp_map )
~ init : ( 0 , exp_map ) ids1 ids2
in
match ( instr1 , instr2 ) with
| Load ( id1 , e1 , t1 , _ ) , Load ( id2 , e2 , t2 , _ ) ->
let n , exp_map = exp_compare_structural ( Var id1 ) ( Var id2 ) exp_map in
if n < > 0 then ( n , exp_map )
else
let n , exp_map = exp_compare_structural e1 e2 exp_map in
( ( if n < > 0 then n else Typ . compare t1 t2 ) , exp_map )
| Store ( e11 , t1 , e21 , _ ) , Store ( e12 , t2 , e22 , _ ) ->
let n , exp_map = exp_compare_structural e11 e12 exp_map in
if n < > 0 then ( n , exp_map )
else
let n = Typ . compare t1 t2 in
if n < > 0 then ( n , exp_map ) else exp_compare_structural e21 e22 exp_map
| Prune ( cond1 , _ , true _ branch1 , ik1 ) , Prune ( cond2 , _ , true _ branch2 , ik2 ) ->
let n , exp_map = exp_compare_structural cond1 cond2 exp_map in
( ( if n < > 0 then n
else
let n = Bool . compare true _ branch1 true _ branch2 in
if n < > 0 then n else compare_if_kind ik1 ik2 )
, exp_map )
| Call ( ret_id1 , e1 , arg_ts1 , _ , cf1 ) , Call ( ret_id2 , e2 , arg_ts2 , _ , cf2 ) ->
let args_compare_structural args1 args2 exp_map =
let n = Int . compare ( List . length args1 ) ( List . length args2 ) in
if n < > 0 then ( n , exp_map )
else
List . fold2_exn
~ f : ( fun ( n , exp_map ) arg1 arg2 ->
if n < > 0 then ( n , exp_map ) else exp_typ_compare_structural arg1 arg2 exp_map )
~ init : ( 0 , exp_map ) args1 args2
in
let n , exp_map = id_typ_opt_compare_structural ret_id1 ret_id2 exp_map in
if n < > 0 then ( n , exp_map )
else
let n , exp_map = exp_compare_structural e1 e2 exp_map in
if n < > 0 then ( n , exp_map )
else
let n , exp_map = args_compare_structural arg_ts1 arg_ts2 exp_map in
( ( if n < > 0 then n else CallFlags . compare cf1 cf2 ) , exp_map )
| Nullify ( pvar1 , _ ) , Nullify ( pvar2 , _ ) ->
exp_compare_structural ( Lvar pvar1 ) ( Lvar pvar2 ) exp_map
| Abstract _ , Abstract _ ->
( 0 , exp_map )
| Remove_temps ( temps1 , _ ) , Remove_temps ( temps2 , _ ) ->
id_list_compare_structural temps1 temps2 exp_map
| Declare_locals ( ptl1 , _ ) , Declare_locals ( ptl2 , _ ) ->
let n = Int . compare ( List . length ptl1 ) ( List . length ptl2 ) in
if n < > 0 then ( n , exp_map )
else
List . fold2_exn
~ f : ( fun ( n , exp_map ) ( pv1 , t1 ) ( pv2 , t2 ) ->
if n < > 0 then ( n , exp_map )
else
let n , exp_map = exp_compare_structural ( Lvar pv1 ) ( Lvar pv2 ) exp_map in
if n < > 0 then ( n , exp_map ) else ( Typ . compare t1 t2 , exp_map ) )
~ init : ( 0 , exp_map ) ptl1 ptl2
| _ ->
( compare_instr instr1 instr2 , exp_map )
let atom_sub subst = atom_expmap ( exp_sub subst )
let atom_sub subst = atom_expmap ( exp_sub subst )
let hpred_sub subst =
let hpred_sub subst =