Set return variables in CFG simplifcation based on post condition

Author: MQuaresma

compiler/entry/jazz2cl.ml

@@ -116,15 +116,16 @@ let parse_and_print print arch call_conv ecoutput joutput output file funname =
      let proc = CL.fun_to_proc (snd prog) (List.nth (snd prog) 0) in
      let formals',pre_ghost_instr,post_ghost_instr = CL_vsimpl.GhostVector.unfold_vectors proc.formals proc.ret_vars in
      let prog' = pre_ghost_instr @ proc.prog @ post_ghost_instr in
-     let cfg = CL_vsimpl.Cfg.cfg_of_prog_rev prog' in
-     let clean_cfg = CL_vsimpl.SimplVector.simpl_cfg cfg proc.ret_vars in
-     let prog' = CL_vsimpl.Cfg.prog_of_cfg clean_cfg in
      let (pre_epred, pre_rpred) = proc.pre in
      let (post_epred, post_rpred) = proc.post in
      let pre_epred' = CL_vsimpl.GhostVector.unfold_vghosts_epred formals' pre_epred in
      let pre_rpred' = CL_vsimpl.GhostVector.unfold_vghosts_rpred formals' pre_rpred in
      let post_epred' = CL_vsimpl.GhostVector.unfold_vghosts_epred formals' post_epred in
      let post_rpred' = CL_vsimpl.GhostVector.unfold_vghosts_rpred formals' post_rpred in
+     let ret_vars = CL_vsimpl.SimplVector.get_ret_vars post_epred' post_rpred' in
+     let cfg = CL_vsimpl.Cfg.cfg_of_prog_rev prog' in
+     let clean_cfg = CL_vsimpl.SimplVector.simpl_cfg cfg ret_vars in
+     let prog' = CL_vsimpl.Cfg.prog_of_cfg clean_cfg in
      let prog' = CL_vsimpl.GhostVector.unfold_cfg_clauses prog' formals' in
      let pre' = (pre_epred', pre_rpred') in
      let post' = (post_epred', post_rpred') in

compiler/src/CL_vsimpl.ml

@@ -288,6 +288,8 @@ end
 module SimplVector = struct
   open Cfg
   open CL.Instr
+  open CL.R
+  open CL.I
 
   let rec int_of_ty = function
     | CL.Uint n -> n
@@ -576,6 +578,64 @@ module SimplVector = struct
       | _ -> h :: remove_nops t
       end
 
+  let rec get_evars epred =
+    let rec aux e =
+      begin
+      match e with
+      | Iconst _ -> []
+      | Ivar v -> [v]
+      | Iunop (_, e') -> aux e'
+      | Ibinop (e1, _, e2) ->
+          (aux e1) @ (aux e2)
+      | Ilimbs (_, el) -> List.flatten (List.map aux el)
+      | IUnPack _ -> assert false
+      end
+    in
+    match epred with
+    | Eeq (e1, e2) ->
+      let vl1 = aux e1 in
+      let vl2 = aux e2 in
+      vl1 @ vl2
+    | Eeqmod (e1, e2, eps) ->
+      let vl1 = aux e1 in
+      let vl2 = aux e2 in
+      let vl3 = List.flatten (List.map aux eps) in
+      vl1 @ vl2 @ vl3
+
+    let rec get_rvars rpred =
+      let rec aux e =
+        begin
+        match e with
+        | Rvar v -> [v]
+        | Rconst _ -> []
+        | Ruext (e', _) ->  aux e'
+        | Rsext (e', _) -> aux e'
+        | Runop (_, e') -> aux e'
+        | Rbinop (e1, _, e2) -> (aux e1) @ (aux e2)
+        | RVget (v, _) -> [v]
+        | UnPack _ -> assert false
+        | Rlimbs (_, el) -> List.flatten (List.map aux el)
+        end
+      in
+      match rpred with
+      | RPcmp (e1, _, e2) ->
+        let vl1 = aux e1 in
+        let vl2 = aux e2 in
+        vl1 @ vl2
+      | RPnot e -> get_rvars e
+      | RPand rps -> List.flatten (List.map get_rvars rps)
+      | RPor rps -> List.flatten (List.map get_rvars rps)
+      | RPeqsmod (e1, e2, e3) ->
+        let vl1 = aux e1 in
+        let vl2 = aux e2 in
+        let vl3 = aux e3 in
+        vl1 @ vl2 @ vl3
+
+  let get_ret_vars epreds rpreds =
+    let epred_rvars = List.flatten (List.map get_evars epreds) in
+    let rpred_vars = List.flatten (List.map get_rvars rpreds) in
+    epred_rvars @ rpred_vars (* FIXME: remove dups *)
+
   let simpl_cfg cfg ret_vars =
     sr_lvals cfg;
     let nI = getPrevI cfg in

compiler/src/CL_vsimpl.mli

@@ -18,5 +18,6 @@ module GhostVector : sig
 end
 
 module SimplVector: sig
+  val get_ret_vars: CL.I.epred list -> CL.R.rpred list -> CL.tyvar list
   val simpl_cfg: Cfg.node -> CL.tyvar list -> Cfg.node
 end