From: Nathan Cooprider <coop@cs...>  20060303 20:02:48

Does there exist or has someone written an effective way of comparing expressions? If not then I will be writing my own, but there is no sense in reinventing the wheel. . . 
From: Nathan Cooprider <coop@cs...>  20060304 16:46:48

I wrote my own. This is something I have thought would be useful for a while, but kept putting off for various reasons. The code is below (CIL maintainers: I put it at the end of the ciltools.ml file). Nathan Nathan Cooprider wrote: > Does there exist or has someone written an effective way of comparing > expressions? If not then I will be writing my own, but there is no > sense in reinventing the wheel. . . (** Comparing expressions without a Out_of_memory error **********************) let rec compare_exp x y = match x,y with Const(CEnum(e1,s1,ei1)),Const(CEnum(e2,s2,ei2)) > let s_comp = compare s1 s2 in if (s_comp <> 0) then s_comp else let e_comp = compare_exp e1 e2 in if (e_comp <> 0) then e_comp else compare ei1.ename ei2.ename  Lval(lv1), Lval(lv2)  AddrOf(lv1),AddrOf(lv2)  StartOf(lv1),StartOf(lv2) > compare_lval lv1 lv2  SizeOf(t1),SizeOf(t2)  AlignOf(t1),AlignOf(t2) > compare_type t1 t2  AlignOfE(e1), AlignOfE(e2) > compare_exp e1 e2  UnOp(o1,e1,t1),UnOp(o2,e2,t2) > let o_comp = compare o1 o2 in if (o_comp <> 0) then o_comp else let e_comp = compare_exp e1 e2 in if( e_comp <> 0) then e_comp else compare_type t1 t2  BinOp(o1,l1,r1,t1),BinOp(o2,l2,r2,t2) > let o_comp = compare o1 o2 in if (o_comp <> 0) then o_comp else let l_comp = compare_exp l1 l2 in if( l_comp <> 0) then l_comp else let r_comp = compare_exp r1 r2 in if ( r_comp<> 0) then r_comp else compare_type t1 t2  CastE(t1,e1),CastE(t2,e2) > let t_comp = compare_type t1 t2 in if (t_comp <> 0) then t_comp else compare_exp e1 e2  _, _ > compare x y and compare_lval x y = match x,y with (Var v1, o1), (Var v2, o2) > let v_comp = compare_var v1 v2 in if (v_comp <> 0) then v_comp else compare_offset o1 o2  (Mem p1, o1), (Mem p2, o2) > let e_comp = compare_exp p1 p2 in if (e_comp <> 0) then e_comp else compare_offset o1 o2  _, _ > compare x y and compare_type x y = compare (typeSig x) (typeSig y) and compare_var x y = compare x.vid y.vid and compare_offset x y = match x, y with Field(fi1,o1),Field(fi2,o2)> let f_comp = compare fi1.fname fi2.fname in if (f_comp <> 0) then f_comp else let c_comp = compare fi1.fcomp.ckey fi2.fcomp.ckey in if (c_comp <> 0) then c_comp else compare_offset o1 o2  Index(e1,o1),Index(e2,o2) > let e_comp = compare_exp e1 e2 in if (e_comp <> 0) then e_comp else compare_offset o1 o2  _, _ > compare x y 
From: Matt Harren <matth@cs...>  20060304 19:31:15

Nathan Cooprider wrote: > (** Comparing expressions without a Out_of_memory error > **********************) You'll get outofmemory errors when using = on Cil.exps because some CIL data structures are cyclic. But you can use (compare e1 e2), because compare will always terminate on CIL expressions. You only need a custom equality checker if you want to consider different expressions to be equivalent, e.g. ints and unsigned ints.  Matt 
From: Nathan Cooprider <coop@cs...>  20060304 21:17:37

Matt Harren wrote: > Nathan Cooprider wrote: > >> (** Comparing expressions without a Out_of_memory error >> **********************) > > You'll get outofmemory errors when using = on Cil.exps because some > CIL data structures are cyclic. But you can use (compare e1 e2), > because compare will always terminate on CIL expressions. You only > need a custom equality checker if you want to consider different > expressions to be equivalent, e.g. ints and unsigned ints. > >  Matt I just tried this and you are correct. I am not sure why I did not try this before. I had just been using '=' exclusively and did not try compare before writing my own. Oh well. Thanks. 