Refactoring of varmaps

compiler/src/compile.ml

@@ -133,7 +133,42 @@ let compile (type reg regx xreg rflag cond asm_op extra_op)
         :: !arrs
     in
     Hv.iter doarr harrs;
-    { Array_expansion.vars; arrs = !arrs }
+
+    let f_cc =
+      match fd.f_cc with
+      | Subroutine si ->
+          (* Since some arguments/returns are expended we need to fix the info *)
+          let tbl = Hashtbl.create 17 in
+          let newpos = ref 0 in
+          let mk_n x =
+            match x.v_kind, x.v_ty with
+            | Reg (_, Direct), Arr (_, n) -> n
+            | _, _ -> 1
+          in
+          let doarg i x =
+            Hashtbl.add tbl i !newpos;
+            newpos := !newpos + mk_n x
+          in
+          List.iteri doarg fd.f_args;
+          let doret o x =
+            match o with
+            | Some i -> [Some (Hashtbl.find tbl i)]
+            | None -> List.init (mk_n (L.unloc x)) (fun _ -> None)
+          in
+          let returned_params =
+            List.flatten (List.map2 doret si.returned_params fd.f_ret) in
+          FInfo.Subroutine { returned_params }
+
+      | _ -> fd.f_cc
+    in
+    let do_outannot x a =
+      try
+        let (_, va) = Hv.find harrs (L.unloc x) in
+        List.init (Array.length va) (fun _ -> [])
+      with Not_found -> [a] in
+    let f_outannot = List.flatten (List.map2 do_outannot fd.f_ret fd.f_outannot) in
+    let finfo = fd.f_loc, fd.f_annot, f_cc, f_outannot in
+    { Array_expansion.vars; arrs = !arrs; finfo }
   in
 
   let refresh_instr_info fn f =

compiler/src/evaluator.ml

@@ -4,9 +4,10 @@ open Type
 open Sem_type
 open Warray_
 open Var0
+open Varmap
 open Low_memory
 open Expr
-open Sem
+open Psem_defs
 open Values
 open Sem_params
 
@@ -37,7 +38,7 @@ let of_val_b ii v : bool =
 type 'asm stack = 
   | Sempty of instr_info * 'asm fundef
   | Scall of 
-      instr_info * 'asm fundef * lval list * sem_t exec Fv.t * 'asm instr list * 'asm stack
+      instr_info * 'asm fundef * lval list * Vm.t * 'asm instr list * 'asm stack
   | Sfor of instr_info * var_i * coq_Z list * 'asm instr list * 'asm instr list * 'asm stack
 
 type ('syscall_state, 'asm) state =
@@ -56,17 +57,17 @@ let return ep spp s =
     let s2 = s.s_estate in
     let m2 = s2.emem and vm2 = s2.evm in
     let vres = 
-      exn_exec ii (mapM (fun (x:var_i) -> get_var vm2 x.v_var) f.f_res) in
+      exn_exec ii (mapM (fun (x:var_i) -> get_var nosubword true vm2 x.v_var) f.f_res) in
     let vres' = exn_exec ii (mapM2 ErrType truncate_val f.f_tyout vres) in
     raise (Final(m2, vres'))
 
   | Scall(ii,f,xs,vm1,c,stk) ->
     let gd = s.s_prog.p_globs in
     let {escs = scs2; emem = m2; evm = vm2} = s.s_estate in
     let vres = 
-      exn_exec ii (mapM (fun (x:var_i) -> get_var vm2 x.v_var) f.f_res) in
+      exn_exec ii (mapM (fun (x:var_i) -> get_var nosubword true vm2 x.v_var) f.f_res) in
     let vres' = exn_exec ii (mapM2 ErrType truncate_val f.f_tyout vres) in
-    let s1 = exn_exec ii (write_lvals ep spp gd {escs = scs2; emem = m2; evm = vm1 } xs vres') in
+    let s1 = exn_exec ii (write_lvals nosubword ep spp true gd {escs = scs2; emem = m2; evm = vm1 } xs vres') in
     { s with 
       s_cmd = c;
       s_estate = s1;
@@ -76,7 +77,7 @@ let return ep spp s =
     match ws with
     | [] -> { s with s_cmd = c; s_stk = stk }
     | w::ws ->
-      let s1 = exn_exec ii (write_var ep i (Vint w) s.s_estate) in
+      let s1 = exn_exec ii (write_var nosubword ep true i (Vint w) s.s_estate) in
       { s with s_cmd = body;
                s_estate = s1;
                s_stk = Sfor(ii, i, ws, body, c, stk) }
@@ -91,31 +92,30 @@ let small_step1 ep spp sip s =
     match ir with
 
     | Cassgn(x,_,ty,e) ->
-      let v  = exn_exec ii (sem_pexpr ep spp gd s1 e) in
+      let v  = exn_exec ii (sem_pexpr nosubword ep spp true gd s1 e) in
       let v' = exn_exec ii (truncate_val ty v) in
-      let s2 = exn_exec ii (write_lval ep spp gd x v' s1) in
+      let s2 = exn_exec ii (write_lval nosubword ep spp true gd x v' s1) in
       { s with s_cmd = c; s_estate = s2 }
 
     | Copn(xs,_,op,es) ->
-      let s2 = exn_exec ii (sem_sopn ep spp sip._asmop gd op s1 xs es) in
+      let s2 = exn_exec ii (sem_sopn nosubword ep spp sip._asmop gd op s1 xs es) in
       { s with s_cmd = c; s_estate = s2 }
 
     | Csyscall(xs,o, es) ->
-        let ves = exn_exec ii (sem_pexprs ep spp gd s1 es) in
-        let ((scs, m), vs) =
-          exn_exec ii (exec_syscall sip._sc_sem ep._pd s1.escs s1.emem o ves)
-        in
-        let s2 = exn_exec ii (write_lvals ep spp gd {escs = scs; emem = m; evm = s1.evm} xs vs) in
+      let ves = exn_exec ii (sem_pexprs nosubword ep spp true gd s1 es) in
+      let ((scs, m), vs) =
+        exn_exec ii (syscall_sem__ sip._sc_sem ep._pd s1.escs s1.emem o ves) in
+      let s2 = exn_exec ii (write_lvals nosubword ep spp true gd {escs = scs; emem = m; evm = s1.evm} xs vs) in
       { s with s_cmd = c; s_estate = s2 }
 
     | Cif(e,c1,c2) ->
-      let b = of_val_b ii (exn_exec ii (sem_pexpr ep spp gd s1 e)) in
+      let b = of_val_b ii (exn_exec ii (sem_pexpr nosubword ep spp true gd s1 e)) in
       let c = (if b then c1 else c2) @ c in
       { s with s_cmd = c }
 
     | Cfor (i,((d,lo),hi), body) ->
-      let vlo = of_val_z ii (exn_exec ii (sem_pexpr ep spp gd s1 lo)) in
-      let vhi = of_val_z ii (exn_exec ii (sem_pexpr ep spp gd s1 hi)) in
+      let vlo = of_val_z ii (exn_exec ii (sem_pexpr nosubword ep spp true gd s1 lo)) in
+      let vhi = of_val_z ii (exn_exec ii (sem_pexpr nosubword ep spp true gd s1 hi)) in
       let rng = wrange d vlo vhi in
       let s =
         {s with s_cmd = []; s_stk = Sfor(ii, i, rng, body, c, s.s_stk) } in
@@ -125,7 +125,7 @@ let small_step1 ep spp sip s =
       { s with s_cmd = c1 @ MkI(ii, Cif(e, c2@[i],[])) :: c }
 
     | Ccall(_,xs,fn,es) ->
-      let vargs' = exn_exec ii (sem_pexprs ep spp gd s1 es) in
+      let vargs' = exn_exec ii (sem_pexprs nosubword ep spp true gd s1 es) in
       let f = 
         match get_fundef s.s_prog.p_funcs fn with
         | Some f -> f
@@ -134,7 +134,7 @@ let small_step1 ep spp sip s =
       let {escs; emem = m1; evm = vm1}  = s1 in
       let stk = Scall(ii,f, xs, vm1, c, s.s_stk) in
       let sf = 
-        exn_exec ii (write_vars ep f.f_params vargs {escs; emem = m1; evm = vmap0}) in
+        exn_exec ii (write_vars nosubword ep true f.f_params vargs {escs; emem = m1; evm = Vm.init nosubword}) in
       {s with s_cmd = f.f_body;
               s_estate = sf;
               s_stk = stk }
@@ -144,10 +144,10 @@ let rec small_step ep spp sip s =
   small_step ep spp sip (small_step1 ep spp sip s)
 
 let init_state ep scs0 p ii fn args m =
-  let f = Option.get (get_fundef p.p_funcs fn) in
+  let f = BatOption.get (get_fundef p.p_funcs fn) in
   let vargs = exn_exec ii (mapM2 ErrType truncate_val f.f_tyin args) in
-  let s_estate = { escs = scs0; emem = m; evm = vmap0 } in
-  let s_estate = exn_exec ii (write_vars ep f.f_params vargs s_estate) in
+  let s_estate = { escs = scs0; emem = m; evm = Vm.init nosubword} in
+  let s_estate = exn_exec ii (write_vars nosubword ep true f.f_params vargs s_estate) in
   { s_prog = p; s_cmd = f.f_body; s_estate; s_stk = Sempty (ii, f) }
 
 

compiler/tests/success/subroutines/x86-64/arr_exp.jazz

@@ -0,0 +1,20 @@
+fn test (reg u64[2] t) -> reg u64[2] {
+   inline int i;
+   for i = 0 to 2 {
+     t[i] += 1;
+   }
+   return t;
+}
+
+export fn main () -> reg u64 {
+  reg u64[2] t;
+  reg u64 r;
+  inline int i;
+  for i = 0 to 2 {
+    t[i] = i;
+  }
+  t = test(t);
+  t[0] += t[1];
+  r = t[0];
+  return r;
+}

compiler/tests/success/subroutines/x86-64/arr_exp_finfo.jazz

@@ -0,0 +1,63 @@
+fn test1 (reg u64[2] t, reg ptr u64[2] p) -> reg ptr u64[2], reg u64[2] {
+   inline int i;
+   for i = 0 to 2 {
+     t[i] += 1;
+     p[i] += 1;
+   }
+
+   return p, t;
+}
+
+fn test2 (reg u64[2] t, reg ptr u64[2] p) -> reg u64[2], reg ptr u64[2] {
+   inline int i;
+   for i = 0 to 2 {
+     t[i] += 1;
+     p[i] += 1;
+   }
+
+   return t, p;
+}
+
+fn test3 (reg ptr u64[2] p, reg u64[2] t) -> reg ptr u64[2], reg u64[2] {
+   inline int i;
+   for i = 0 to 2 {
+     t[i] += 1;
+     p[i] += 1;
+   }
+
+   return p, t;
+}
+
+fn test4 (reg ptr u64[2] p, reg u64[2] t) -> reg u64[2], reg ptr u64[2] {
+   inline int i;
+   for i = 0 to 2 {
+     t[i] += 1;
+     p[i] += 1;
+   }
+
+   return t, p;
+}
+
+
+
+export fn main () -> reg u64 {
+  stack u64[2] s;
+  reg u64[2] t;
+  reg ptr u64[2] p;
+  reg u64 r;
+  inline int i;
+  p = s;
+  for i = 0 to 2 {
+    t[i] = i;
+    p[i] = i;
+  }
+  p,t = test1(t,p);
+  t,p = test2(t,p);
+  p,t = test3(p,t);
+  t,p = test4(p,t);
+  t[0] += t[1];
+  t[0] += p[0];
+  t[0] += p[1];
+  r = t[0];
+  return r;
+}

proofs/_CoqProject

@@ -56,6 +56,7 @@ compiler/dead_calls.v
 compiler/dead_calls_proof.v
 compiler/dead_code.v
 compiler/dead_code_proof.v
+compiler/direct_call_proof.v
 compiler/inline.v
 compiler/inline_proof.v
 compiler/jasmin_compiler.v
@@ -110,11 +111,11 @@ lang/lowering_lemmas.v
 lang/memory_example.v
 lang/memory_model.v
 lang/one_varmap.v
-lang/psem_of_sem_proof.v
-lang/psem_facts.v
 lang/psem.v
+lang/psem_defs.v
+lang/psem_of_sem_proof.v
 lang/pseudo_operator.v
-lang/sem.v
+lang/psem_facts.v
 lang/sem_one_varmap.v
 lang/sem_op_typed.v
 lang/sem_one_varmap_facts.v
@@ -131,6 +132,7 @@ lang/type.v
 lang/utils.v
 lang/values.v
 lang/var.v
+lang/varmap.v
 lang/waes.v
 lang/warray_.v
 lang/word.v