Re: [CIL users] Comparing expressions

[Nathan C. <co...@cs...>]

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