Use UID to find unfolded vector formals instead of flag when dealing with output variables

Author: MQuaresma

compiler/src/CL_vsimpl.ml

@@ -128,17 +128,17 @@ module GhostVector = struct
   type vector =
     | U16x16
 
-  let get_vghost ghosts gname b =
-    let vghost = List.find (fun (v, _) -> v.v_name = gname) (if b then List.rev ghosts else ghosts) in (* FIXME: DIRTY HACK *)
+  let get_vghost ghosts gname =
+    let vghost = List.find (fun (v, _) -> v.v_name = gname) ghosts in
     vghost
 
   let get_unfolded_vector_namei v i =
-    String.concat "_" [v.v_name; "v" ; string_of_int i]
+    String.concat "_" [v.v_name; (string_of_uid v.v_id); "v" ; string_of_int i]
 
   let rec replace_vghosts_rexp ghosts r =
-    let aux (v, ty) i b =
+    let aux (v, ty) i =
       let name = get_unfolded_vector_namei v i in
-      let v' = get_vghost ghosts name b in
+      let v' = get_vghost ghosts name in
       Rvar v'
     in
     match r with
@@ -158,8 +158,11 @@ module GhostVector = struct
       let e2' = replace_vghosts_rexp ghosts e2 in
       Rbinop(e1', s, e2')
     | RVget(e,c) -> r
-    | UnPack (e,us,i,b) ->
-      aux e i b
+    | UnPack (e,us,i) ->
+      aux e i
+    | Rlimbs (c, e) -> 
+      let e' = List.map (replace_vghosts_rexp ghosts) e in
+      Rlimbs (c, e')
 
   let rec unfold_ghosts_rpred ghosts pre =
     match pre with
@@ -186,9 +189,9 @@ module GhostVector = struct
     List.map (unfold_ghosts_rpred ghosts) pre
 
   let rec replace_vghosts_eexp ghosts e =
-    let aux (v, ty) i b =
+    let aux (v, ty) i =
       let name = get_unfolded_vector_namei v i in
-      let v' = get_vghost ghosts name b in
+      let v' = get_vghost ghosts name in
       Ivar v'
     in
     match e with
@@ -204,8 +207,8 @@ module GhostVector = struct
     | Ilimbs (c, l) ->
       let l' = List.map (replace_vghosts_eexp ghosts) l in
       Ilimbs (c, l')
-    | IUnPack (e, us, i, b) ->
-      aux e i b
+    | IUnPack (e, us, i) ->
+      aux e i
 
   let rec unfold_ghosts_epred ghosts pre =
     match pre with
@@ -280,29 +283,6 @@ module GhostVector = struct
       | h::t ->
         [unfold_clauses h formals] @ (unfold_cfg_clauses t formals)
       | [] -> []
-
-(* CHECK ME: CL doesn't support vector/arrays as arguments it seems; see preliminary.cl *)
-(*
-  let unfold_vectors_list formals ret_vars =
-    let aux ((v,ty) as tv) =
-      let mk_vector = Annot.filter_string_list None ["u16x16", U16x16] in
-      match Annot.ensure_uniq1 "vect" mk_vector (v.v_annot) with
-      | None -> [tv],[],[]
-      | Some U16x16 ->
-        let (l_16x16, lty_16x16) as l16x16 = I.var_to_tyvar ~vector:(16,16) v in
-        let ll16x16 = Llvar l16x16 in
-        if List.exists (is_eq_tyvar tv) ret_vars then
-          let a_1x256 = Avatome [Avar tv] in
-          [l16x16], [], [cast lty_16x16 ll16x16 a_1x256]
-        else
-          let vl16x16 = Avar l16x16 in
-          [l16x16], [cast ty (Llvar tv) vl16x16],[]
-    in
-    List.fold_left (fun (acc1,acc2,acc3) tv ->
-        let fs,ispre,ispost = aux tv in
-        fs @ acc1, ispre @ acc2, ispost @ acc3)
-      ([],[],[]) formals
-*)
 end
 
 module SimplVector = struct

compiler/src/toCL.ml

@@ -84,7 +84,7 @@ module CL = struct
       | Iunop  of string * eexp
       | Ibinop of eexp * string * eexp
       | Ilimbs of const * eexp list
-      | IUnPack of tyvar * int * int * bool
+      | IUnPack of tyvar * int * int
 
     let (!-) e1 = Iunop ("-", e1)
     let (-) e1 e2 = Ibinop (e1, "-", e2)
@@ -134,7 +134,7 @@ module CL = struct
       | Runop  of string * rexp
       | Rbinop of rexp * string * rexp
       | RVget  of tyvar * const
-      | UnPack of  tyvar * int * int * bool
+      | UnPack of  tyvar * int * int
       | Rlimbs of const * rexp list
 
     let const (i1,z1) = Rconst (i1,z1)
@@ -557,9 +557,7 @@ module I (S:S): I = struct
     | PappN(Oabstract {pa_name="ze_16_32"}, [v]) -> Ruext (!> v, 16)
     | PappN(Oabstract {pa_name="limbs_4u64"}, [q]) -> Rlimbs ((Z.of_int 64), (List.map (!>) (extract_list q [])))
     | PappN(Oabstract {pa_name="u256_as_16u16"}, [Pvar x ; Pconst z]) ->
-      UnPack (to_var ~sign x, 16, Z.to_int z, false)
-    | PappN(Oabstract {pa_name="u256_as_16u16"}, [Presult (_, x) ; Pconst z]) ->
-      UnPack (to_var ~sign x, 16, Z.to_int z, true)
+      UnPack (to_var ~sign x, 16, Z.to_int z)
     | _ -> error e
 
   let rec gexp_to_rpred ?(sign=S.s) e : CL.R.rpred =
@@ -579,8 +577,8 @@ module I (S:S): I = struct
     | Papp2(Olt int, e1, e2)  -> ult !> e1 !> e2
     | Papp2(Ogt int, e1, e2)  -> ugt !> e1 !> e2
     | Pif(_, e1, e2, e3) -> RPand [RPor [RPnot !>> e1; !>> e2];RPor[ !>> e1; !>> e3]]
-    | Pabstract ({name="eq"}, [e1;e2]) -> eq !> e1 !> e2
-    | Pabstract ({name="eqsmod"} as _opa, [e1;e2;e3]) -> RPeqsmod (!> e1, !> e2, !> e3)
+    | PappN (Oabstract {pa_name="eq"}, [e1;e2]) -> eq !> e1 !> e2
+    | PappN (Oabstract {pa_name="eqsmod"} as _opa, [e1;e2;e3]) -> RPeqsmod (!> e1, !> e2, !> e3)
     | _ -> error e
 
   let rec get_const x =
@@ -696,11 +694,8 @@ module I (S:S): I = struct
       mull !> b (power (Ivar v) !> a)
     | PappN (Oabstract {pa_name="mon0"}, [b]) ->
       !> b
-    | PappN (Oabstract {name="u256_as_16u16"}, [Pvar x; Pconst z]) ->
-      IUnPack (to_var ~sign x, 16, Z.to_int z, false)
-    | Pabstract ({name="u256_as_16u16"}, [Presult (_, x) ; Pconst z]) ->
-        IUnPack (to_var ~sign x, 16, Z.to_int z, true)
-    | Presult (_,x) -> Ivar (to_var ~sign x)
+    | PappN (Oabstract {pa_name="u256_as_16u16"}, [Pvar x; Pconst z]) ->
+      IUnPack (to_var ~sign x, 16, Z.to_int z)
     | _ -> error e
 
   let rec gexp_to_epred env ?(sign=S.s) e :CL.I.epred list =
@@ -1886,11 +1881,10 @@ module Mk(O:BaseOp) = struct
             [CL.Instr.assert_ pre_cl], [CL.Instr.assume post_cl]
         in
       (* FIXME: How are we sure that the variables in r are fresh ? *)
-      r , pre_cl @ post_cl
       let formals = List.map O.I.var_to_tyvar fd.f_args in
       let cond (a,_) (x,_) = (x.v_name = a.v_name) && (x.v_id = a.v_id) in
       let formals = filter_add cond formals (List.map O.I.gexp_to_var params) in
-      r , formals , [CL.Instr.assert_ pre_cl] @  [CL.Instr.assume post_cl]
+      r , formals, pre_cl @ post_cl
 
     | Cassgn (a, _, _, e) ->
       begin
@@ -1934,7 +1928,6 @@ module Mk(O:BaseOp) = struct
         let post = sub_fun_returns ci.f_ires r post in
         let post = to_clause env post in
         pre, post in
-    let lval,prog = pp_c env fds fd.f_body in
     let lval,formals_args,prog = pp_c env fds fd.f_body in
     let formals_lval = List.map (fun x -> O.I.get_lval (O.I.glval_to_lval x)) lval in
     let cond (a,_) (x,_) = (x.v_name = a.v_name) && (x.v_id = a.v_id) in

compiler/src/toCL.mli

@@ -23,7 +23,7 @@ module CL : sig
       | Iunop  of string * eexp
       | Ibinop of eexp * string * eexp
       | Ilimbs of const * eexp list
-      | IUnPack of tyvar * int * int * bool
+      | IUnPack of tyvar * int * int
 
     type epred =
       | Eeq of eexp * eexp
@@ -41,7 +41,7 @@ module CL : sig
       | Runop  of string * rexp
       | Rbinop of rexp * string * rexp
       | RVget  of tyvar * const
-      | UnPack of  tyvar * int * int * bool
+      | UnPack of  tyvar * int * int
       | Rlimbs of const * rexp list
 
     type rpred =