checking of constant/writable arguments

Fix printing of #inline function calls

CHANGELOG.md

@@ -9,6 +9,10 @@
   ([PR #177](https://github.com/jasmin-lang/jasmin/pull/177);
   fixes [#175](https://github.com/jasmin-lang/jasmin/issues/175)).
 
+- More precise pretyping for "reg const ptr" and function call.
+  ([PR #178](https://github.com/jasmin-lang/jasmin/pull/178);
+  fixes [#176](https://github.com/jasmin-lang/jasmin/issues/176)).
+
 ## New features
 
 - Fill an array with “random” data using `p = #randombytes(p);`

compiler/src/pretyping.ml

@@ -1217,7 +1217,6 @@ let tt_lvalue pd (env : 'asm Env.env) { L.pl_desc = pl; L.pl_loc = loc; } =
 
   | S.PLVar x ->
     let x = tt_var `NoParam env x in
-    reject_constant_pointers loc x ;
     loc, (fun _ -> P.Lvar (L.mk_loc loc x)), Some x.P.v_ty
 
   | S.PLArray (aa, ws, ({ pl_loc = xlc } as x), pi, olen) ->
@@ -1595,18 +1594,39 @@ let check_lval_pointer loc x =
   | _ -> rs_tyerror ~loc (NotAPointer x)
 
 let mk_call loc is_inline lvs f es =
-  begin match f.P.f_cc with 
-  | P.Internal | P.Export -> ()
-  | P.Subroutine _ ->
+  let open P in
+  begin match f.f_cc with
+  | Internal -> ()
+  | Export -> if is_inline <> E.InlineFun then rs_tyerror ~loc (string_error "call to export function needs to be inlined")
+  | Subroutine _ ->
     let check_lval = function
-      | P.Lnone _ | Lvar _ | Lasub _ -> ()
+      | Lnone _ | Lvar _ | Lasub _ -> ()
       | Lmem _ | Laset _ -> rs_tyerror ~loc (string_error "memory/array assignment are not allowed here") in
-    let check_e = function
-      | P.Pvar _ | P.Psub _ -> ()
+    let rec check_e = function
+      | Pvar _ | Psub _ -> ()
+      | Pif (_, _, e1, e2) -> check_e e1; check_e e2
       | _ -> rs_tyerror ~loc (string_error "only variables and subarray are allowed in arguments of non-inlined function") in
     List.iter check_lval lvs;
     List.iter check_e es
   end;
+
+  (* Check writability *)
+  let check_ptr_writable x =
+     match x.v_kind with
+     | Stack (Pointer Writable) | Reg (_, Pointer Writable) -> true
+     | _ -> false in
+  let check_w x e =
+    if check_ptr_writable x then
+      let rec aux  = function
+        | Pvar y | Psub(_, _, _, y, _) ->
+          let y = L.unloc y.gv in
+          if not (check_ptr_writable y || y.v_kind = Stack Direct) then
+            rs_tyerror ~loc (string_error "argument %a needs to be writable" Printer.pp_pvar y)
+        | Pif (_, _, e1, e2) -> aux e1; aux e2
+        | _ -> assert false in
+      aux e in
+  List.iter2 check_w f.f_args es;
+
   P.Ccall (is_inline, lvs, f.P.f_name, es)
 
 let tt_annot_vardecls dfl_writable pd env (annot, (ty,vs)) = 

compiler/src/printer.ml

@@ -258,11 +258,12 @@ let rec pp_gi pp_info pp_len pp_opn pp_var fmt i =
       (pp_cblock pp_info pp_len pp_opn pp_var) c (pp_ge pp_len pp_var) e
       (pp_cblock pp_info pp_len pp_opn pp_var) c'
 
-  | Ccall(_ii, x, f, e) -> (* FIXME ii *)
+  | Ccall(ii, x, f, e) ->
     let pp_x fmt = function
       | [] -> ()
       | x -> F.fprintf fmt "%a =@ " (pp_glvs pp_len pp_var) x in
-    F.fprintf fmt "@[<hov 2>%a%s(%a);@]"
+    F.fprintf fmt "@[<hov 2>%s%a%s(%a);@]"
+      (match ii with | E.InlineFun -> "#inline " | E.DoNotInline -> "")
       pp_x x f.fn_name (pp_ges pp_len pp_var) e
 
 (* -------------------------------------------------------------------- *)

compiler/tests/fail/pointers/test_writable_arguments.jazz

@@ -0,0 +1,15 @@
+fn f(reg ptr u64[1] t) -> reg ptr u64[1] {
+   t[0] = 1;
+   return t;
+}
+
+export fn gfail() -> reg u64{
+  stack u64[1] s;
+  reg const ptr  u64[1] t;
+  t = s;
+  s = f(t);
+  reg u64 r;
+  r = s[0];
+  return r;
+}
+

compiler/tests/success/eval_poly1305_u32.jazz

@@ -153,7 +153,7 @@ fn poly1305(reg u64 out, reg u64 in, reg u64 inlen, reg u64 k) -> reg u64 {
 
     } else {
       for i = 0 to 17 {
-        tmp32 = #set0_32();
+        _, _, _, _, _, tmp32 = #set0_32();
         of, cf, sf, _, zf = #CMP(inlen, i);
         if !zf && (sf ? of : !of) { // inlen > i
           tmp = (u8)[in + i];
@@ -162,7 +162,7 @@ fn poly1305(reg u64 out, reg u64 in, reg u64 inlen, reg u64 k) -> reg u64 {
         tmp32 = one if zf; // inlen == i
         c[i] = tmp32;
       }
-      inlen = #set0();
+      _, _, _, _, _, inlen = #set0();
     }
 
     h = add(h, c);
@@ -180,7 +180,7 @@ fn poly1305(reg u64 out, reg u64 in, reg u64 inlen, reg u64 k) -> reg u64 {
   c[16] = 0;
   add_and_store(out, h, c);
 
-  ret = #set0();
+  _, _, _, _, _, ret = #set0();
   return ret;
 }
 
@@ -235,7 +235,7 @@ in = 0x1000;
 
 inlen = 34;
 
-tmp = poly1305(out, in, inlen, k);
+#inline tmp = poly1305(out, in, inlen, k);
 
 for i = 0 to 16 {
   result[i] = (u8)[out + i];

compiler/tests/success/inline_call_to_export.jazz

@@ -0,0 +1,16 @@
+export
+fn sum(reg u64 x y) -> reg u64 {
+  reg u64 z;
+  z = #LEA(x + y);
+  return z;
+}
+
+/* Inline call to an export function from an inline function. */
+inline
+fn test() -> reg u64 {
+  reg u64 a;
+  #inline a = sum(42, 24);
+  return a;
+}
+
+exec test()

compiler/tests/success/pointers/test_writable_arguments.jazz

@@ -0,0 +1,14 @@
+fn f(reg ptr u64[1] t) -> reg ptr u64[1] {
+   t[0] = 1;
+   return t;
+}
+
+export fn g() -> reg u64{
+  stack u64[1] s;
+  reg ptr u64[1] t;
+  t = s;
+  s = f((0 <= 1) ? t : t);
+  reg u64 r;
+  r = s[0];
+  return r;
+}

compiler/tests/success/pointers/zerofill.jazz

@@ -0,0 +1,13 @@
+fn zerofill(reg mut ptr u64[1] x) -> reg ptr u64[1] {
+  x[0] = 0;
+  return x;
+}
+
+export
+fn main() -> reg u64 {
+  stack u64[1] s;
+  s = zerofill(s);
+  reg u64 r;
+  r = s[0];
+  return r;
+}

compiler/tests/success/vpsxldq.jazz

@@ -24,7 +24,7 @@ p = 0x480;
 g = 0x12345678901234567890123456789012;
 (u128)[p + 0] = g;
 
-test(p);
+#inline test(p);
 
 r[0] = (u256)[p + 0];
 r[1] = (u256)[p + 32];