Add more syscalls to Jasmin

compiler/src/alias.ml

@@ -178,6 +178,10 @@ let assign_arr params a x e =
 let syscall_cc (o : 'a Syscall_t.syscall_t) =
   match o with
   | Syscall_t.RandomBytes _ -> [Some 0]
+  | Syscall_t.Open _ -> [None]
+  | Syscall_t.Close -> [None]
+  | Syscall_t.Write _ -> [Some 0]
+  | Syscall_t.Read _ -> [Some 0]
 
 let link_array_return params a xs es cc =
   List.fold_left2 (fun a x ->

compiler/src/conv.ml

@@ -6,6 +6,7 @@ include CoreConv
 module W = Wsize
 module T = Type
 module C = Expr
+module Csys = Syscall
 
 let z_of_nat n =
   z_of_cz (BinInt.Z.of_nat n)
@@ -135,6 +136,14 @@ let expr_of_cexprs es = List.map (expr_of_cexpr) es
 
 (* ------------------------------------------------------------------------ *)
 
+let csyscall_of_syscall sc = 
+  match sc with
+  | Syscall_t.RandomBytes n -> Csys.RandomBytes n
+  | Syscall_t.Open n -> Csys.Open n
+  | Syscall_t.Close -> Csys.Close
+  | Syscall_t.Write n -> Csys.Write n
+  | Syscall_t.Read n -> Csys.Read n
+
 let rec cinstr_of_instr i =
   let n = i.i_loc, i.i_annot in
   cinstr_r_of_instr_r n i.i_desc
@@ -153,7 +162,7 @@ and cinstr_r_of_instr_r p i =
 
   | Csyscall(x,o,e) ->
     let ir =
-      C.Csyscall(clval_of_lvals x, o, cexpr_of_exprs e) in
+      C.Csyscall(clval_of_lvals x, csyscall_of_syscall o, cexpr_of_exprs e) in
     C.MkI(p, ir)
 
   | Cif(e,c1,c2) ->
@@ -179,13 +188,22 @@ and cinstr_r_of_instr_r p i =
 and cstmt_of_stmt c =
   List.map cinstr_of_instr c
 
+let syscall_of_csyscall sc = 
+  match sc with
+  | Csys.RandomBytes n -> Syscall_t.RandomBytes n
+  | Csys.Open n -> Syscall_t.Open n
+  | Csys.Close -> Syscall_t.Close
+  | Csys.Write n -> Syscall_t.Write n
+  | Csys.Read n -> Syscall_t.Read n
+
 let rec instr_of_cinstr i =
   match i with
   | C.MkI(p, ir) ->
     let i_loc, i_annot = p in
     let i_desc = instr_r_of_cinstr_r ir in
     { i_desc; i_loc; i_info = (); i_annot }
 
+
 and instr_r_of_cinstr_r = function
   | C.Cassgn(x,t, ty,e) ->
     Cassgn(lval_of_clval x, t, ty_of_cty ty, expr_of_cexpr e)
@@ -194,7 +212,7 @@ and instr_r_of_cinstr_r = function
     Copn(lval_of_clvals x, t, o, expr_of_cexprs e)
 
   | C.Csyscall(x,o,e) ->
-    Csyscall(lval_of_clvals x, o, expr_of_cexprs e)
+    Csyscall(lval_of_clvals x, syscall_of_csyscall o, expr_of_cexprs e)
 
   | C.Cif(e,c1,c2) ->
     let c1 = stmt_of_cstmt c1 in

compiler/src/conv.mli

@@ -45,6 +45,9 @@ val lval_of_clval :  Expr.lval -> Prog.lval
 val cexpr_of_expr :  expr -> Expr.pexpr
 val expr_of_cexpr :  Expr.pexpr -> expr
 
+val csyscall_of_syscall : BinNums.positive Syscall_t.syscall_t -> Syscall.syscall_t
+val syscall_of_csyscall : Syscall.syscall_t -> BinNums.positive Syscall_t.syscall_t
+
 val cufdef_of_fdef :  (unit, 'asm) func -> Var0.funname * 'asm Expr._ufundef
 val fdef_of_cufdef :  Var0.funname * 'asm Expr._ufundef -> (unit, 'asm) func
 

compiler/src/evaluator.ml

@@ -104,7 +104,7 @@ let small_step1 ep spp sip s =
     | Csyscall(xs,o, es) ->
       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
+        exn_exec ii (syscall_sem__ ep._pd sip._sc_sem 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 }
 

compiler/src/insert_copy_and_fix_length.ml

@@ -86,6 +86,32 @@ and iac_instr_r pd loc ir =
         | _ -> assert false in
       let p = Conv.pos_of_int (Prog.size_of ty) in
       Csyscall(xs, Syscall_t.RandomBytes p, es)
+    | Syscall_t.Open _ ->
+      (* Fix the size it is dummy for the moment *)
+      let ty =
+        match es with
+        | [e] -> Typing.ty_expr pd loc e
+        | _ -> assert false in
+      let p = Conv.pos_of_int (Prog.size_of ty) in
+      Csyscall(xs, Syscall_t.Open p, es)
+    | Syscall_t.Close ->
+      Csyscall (xs, Syscall_t.Close, es)
+    | Syscall_t.Write _ ->
+      (* Fix the size it is dummy for the moment *)
+      let ty =
+        match es with
+        | [e; _] -> Typing.ty_expr pd loc e
+        | _ -> assert false in
+      let p = Conv.pos_of_int (Prog.size_of ty) in
+      Csyscall(xs, Syscall_t.Write p, es)
+      | Syscall_t.Read _ ->
+        (* Fix the size it is dummy for the moment *)
+        let ty =
+          match es with
+          | [e; _] -> Typing.ty_expr pd loc e
+          | _ -> assert false in
+        let p = Conv.pos_of_int (Prog.size_of ty) in
+        Csyscall(xs, Syscall_t.Read p, es)
     end
 
   | Ccall _ -> ir

compiler/src/pp_arm_m4.ml

@@ -163,6 +163,10 @@ let pp_mnemonic_ext (ARM_op (_, opts) as op) suff args =
 let pp_syscall (o : _ Syscall_t.syscall_t) =
   match o with
   | Syscall_t.RandomBytes _ -> "__jasmin_syscall_randombytes__"
+  | Syscall_t.Open _ -> "__jasmin_syscall_open__"
+  | Syscall_t.Close -> "__jasmin_syscall_close__"
+  | Syscall_t.Write _ -> "__jasmin_syscall_write__"
+  | Syscall_t.Read _ -> "__jasmin_syscall_read__"
 
 (* To conform to the Unified Assembly Language (UAL) of ARM, IT instructions
    must be introduced *in addition* to conditional suffixes. *)
@@ -281,7 +285,7 @@ let pp_instr fn i =
       [ LInstr ("pop", [ "{pc}" ]) ]
 
   | SysCall op ->
-      [LInstr ("bl", [ pp_syscall op ])]
+      [LInstr ("bl", [ pp_syscall (Conv.syscall_of_csyscall op) ])]
 
   | AsmOp (op, args) ->
       let id = instr_desc arm_decl arm_op_decl (None, op) in

compiler/src/ppasm.ml

@@ -405,6 +405,10 @@ module Printer (BP:BPrinter) = struct
   let pp_syscall (o : 'a Syscall_t.syscall_t) =
     match o with
     | Syscall_t.RandomBytes _ -> "__jasmin_syscall_randombytes__"
+    | Syscall_t.Open _ -> "__jasmin_syscall_open__"
+    | Syscall_t.Close -> "__jasmin_syscall_close__"
+    | Syscall_t.Write _ -> "__jasmin_syscall_write__"
+    | Syscall_t.Read _ -> "__jasmin_syscall_read__"
 
   (* -------------------------------------------------------------------- *)
   let pp_instr name (i : (_, _, _, _, _, _) Arch_decl.asm_i_r) =
@@ -436,7 +440,7 @@ module Printer (BP:BPrinter) = struct
 
     | SysCall(op) ->
       let name = "call" in
-      let args = [pp_syscall op] in
+      let args = [pp_syscall (Conv.syscall_of_csyscall op)] in
       `Instr(name, args)
 
     | AsmOp(op, args) ->

compiler/src/pretyping.ml

@@ -1760,6 +1760,110 @@ let rec tt_instr arch_info (env : 'asm Env.env) ((annot,pi) : S.pinstr) : 'asm E
       let _ = tt_as_array (loc, ty) in
       let es = tt_exprs_cast arch_info.pd env (L.loc pi) args [ty] in
       env, [mk_i (P.Csyscall([x], Syscall_t.RandomBytes (Conv.pos_of_int 1), es))]
+  | S.PIAssign ((ls, xs), `Raw, { pl_desc = PEPrim (f, args) }, None) when L.unloc f = "open" ->
+    (* FIXME syscall *)
+    (* This is dirty but ... *)
+    if ls <> None then rs_tyerror ~loc:(L.loc pi) (string_error "open expects no implicit arguments");
+    let loc, x, ty =
+      match xs with
+      | [x] ->
+        let loc, x, oty = tt_lvalue arch_info.pd env x in
+        let ty =
+          match oty with
+          | None -> rs_tyerror ~loc (string_error "_ lvalue not accepted here")
+          | Some ty -> ty in
+        loc, x ty, ty
+      | _ ->
+        rs_tyerror ~loc:(L.loc pi)
+          (string_error "only a single variable is allowed as destination of open") in
+    let _ = tt_as_word (loc, ty) in
+    let e, ty = 
+      match args with
+      | [e] -> tt_expr arch_info.pd env e
+      | _ -> rs_tyerror ~loc:(L.loc pi) (string_error "only a single variable is allowed as input of open")
+    in
+    (** FIXME: Pass an actual location *)
+    let _ = tt_as_array (L._dummy, ty) in
+    env, [mk_i (P.Csyscall([x], Syscall_t.Open (Conv.pos_of_int 1), [e]))]
+  | S.PIAssign ((ls, xs), `Raw, { pl_desc = PEPrim (f, args) }, None) when L.unloc f = "close" ->
+    (* FIXME syscall *)
+    (* This is dirty but ... *)
+    if ls <> None then rs_tyerror ~loc:(L.loc pi) (string_error "close expects no implicit arguments");
+    let loc, x, ty =
+      match xs with
+      | [x] ->
+        let loc, x, oty = tt_lvalue arch_info.pd env x in
+        let ty =
+          match oty with
+          | None -> rs_tyerror ~loc (string_error "_ lvalue not accepted here")
+          | Some ty -> ty in
+        loc, x ty, ty
+      | _ ->
+        rs_tyerror ~loc:(L.loc pi)
+          (string_error "only a single variable is allowed as destination of close") in
+    let _ = tt_as_word (loc, ty) in
+    let e, ty = 
+      match args with
+      | [e] -> tt_expr arch_info.pd env e
+      | _ -> rs_tyerror ~loc:(L.loc pi) (string_error "only a single variable is allowed as input of open")
+    in
+    (** FIXME: Pass an actual location *)
+    let _ = tt_as_word (L._dummy, ty) in
+    env, [mk_i (P.Csyscall([x], Syscall_t.Close, [e]))]
+  | S.PIAssign ((ls, xs), `Raw, { pl_desc = PEPrim (f, args) }, None) when L.unloc f = "write" ->
+    (* FIXME syscall *)
+    (* This is dirty but ... *)
+    if ls <> None then rs_tyerror ~loc:(L.loc pi) (string_error "write expects no implicit arguments");
+    let loc, x, ty =
+      match xs with
+      | [x] ->
+        let loc, x, oty = tt_lvalue arch_info.pd env x in
+        let ty =
+          match oty with
+          | None -> rs_tyerror ~loc (string_error "_ lvalue not accepted here")
+          | Some ty -> ty in
+        loc, x ty, ty
+      | _ ->
+        rs_tyerror ~loc:(L.loc pi)
+          (string_error "only a single variable is allowed as destination of write") in
+    let e = 
+      match args with
+      | [e; f] -> 
+          let e, ty = tt_expr arch_info.pd env e in
+          let _ = tt_as_array (L._dummy, ty) in
+          let e2, ty2 = tt_expr arch_info.pd env f in
+          let _ = tt_as_word (L._dummy, ty2) in
+          [e; e2]
+      | _ -> rs_tyerror ~loc:(L.loc pi) (string_error "write expects two variables as input")
+    in
+    env, [mk_i (P.Csyscall([x], Syscall_t.Write (Conv.pos_of_int 1), e))]
+  | S.PIAssign ((ls, xs), `Raw, { pl_desc = PEPrim (f, args) }, None) when L.unloc f = "read" ->
+      (* FIXME syscall *)
+      (* This is dirty but ... *)
+      if ls <> None then rs_tyerror ~loc:(L.loc pi) (string_error "read expects no implicit arguments");
+      let loc, x, ty =
+        match xs with
+        | [x] ->
+          let loc, x, oty = tt_lvalue arch_info.pd env x in
+          let ty =
+            match oty with
+            | None -> rs_tyerror ~loc (string_error "_ lvalue not accepted here")
+            | Some ty -> ty in
+          loc, x ty, ty
+        | _ ->
+          rs_tyerror ~loc:(L.loc pi)
+            (string_error "only a single variable is allowed as destination of read") in
+      let e = 
+        match args with
+        | [e; f] -> 
+            let e, ty = tt_expr arch_info.pd env e in
+            let _ = tt_as_array (L._dummy, ty) in
+            let e2, ty2 = tt_expr arch_info.pd env f in
+            let _ = tt_as_word (L._dummy, ty2) in
+            [e; e2]
+        | _ -> rs_tyerror ~loc:(L.loc pi) (string_error "read expects two variables as input")
+      in
+      env, [mk_i (P.Csyscall([x], Syscall_t.Read (Conv.pos_of_int 1), e))]
 
   | S.PIAssign ((ls, xs), `Raw, { pl_desc = PEPrim (f, args) }, None) when L.unloc f = "swap" ->
       if ls <> None then rs_tyerror ~loc:(L.loc pi) (string_error "swap expects no implicit arguments");

compiler/src/printCommon.ml

@@ -94,8 +94,13 @@ let string_of_op2 = function
 let pp_opn pd asmOp fmt o = pp_string0 fmt (Sopn.string_of_sopn pd asmOp o)
 
 (* -------------------------------------------------------------------- *)
-let pp_syscall (o : 'a Syscall_t.syscall_t) =
-  match o with Syscall_t.RandomBytes _ -> "#randombytes"
+let pp_syscall (o : Syscall.syscall_t) =
+  match o with 
+  | Syscall.RandomBytes _ -> "#randombytes"
+  | Syscall.Open _ -> "#open"
+  | Syscall.Close -> "#close"
+  | Syscall.Write _ -> "#write"
+  | Syscall.Read _ -> "#read"
 
 (* -------------------------------------------------------------------- *)
 let pp_bool fmt b = if b then fprintf fmt "true" else fprintf fmt "false"

compiler/src/printCommon.mli

@@ -10,7 +10,7 @@ val string_of_op1 : Expr.sop1 -> string
 val string_of_op2 : Expr.sop2 -> string
 val pp_opn :
   Wsize.wsize -> 'asm Sopn.asmOp -> Format.formatter -> 'asm Sopn.sopn -> unit
-val pp_syscall : BinNums.positive Syscall_t.syscall_t -> string
+val pp_syscall : Syscall.syscall_t -> string
 val pp_bool : Format.formatter -> bool -> unit
 val pp_kind : Format.formatter -> Wsize.v_kind -> unit
 val pp_btype : Format.formatter -> Prog.base_ty -> unit

compiler/src/printer.ml

@@ -150,7 +150,7 @@ let rec pp_gi pp_info pp_len pp_opn pp_var fmt i =
 
   | Csyscall(x, o, e) ->
       F.fprintf fmt "@[<hov 2>%a =@ %s(%a);@]"
-        (pp_glvs pp_len pp_var) x (pp_syscall o) (pp_ges pp_len pp_var) e
+        (pp_glvs pp_len pp_var) x (pp_syscall (Conv.csyscall_of_syscall o)) (pp_ges pp_len pp_var) e
 
   | Cif(e, c, []) ->
     F.fprintf fmt "@[<v>if %a %a@]"

compiler/src/syscall_ocaml.ml

@@ -1,3 +1,5 @@
+open Ssralg
+
 type state = unit
 
 (* FIXME syscall : I don't think that this implementation is a good one.
@@ -19,4 +21,27 @@ let get_random (s : state) (z:BinNums.coq_Z) =
   assert (0 <= n);
   s, List.init n random_char
 
-let sc_sem : state Syscall.syscall_sem = get_random
+
+(** FIXME: Reurn actual fd *)
+let open_file (s : state) (filename: GRing.ComRing.sort list) =
+  s, (Word0.wrepr Wsize.U64 (CoreConv.cz_of_int 1))
+
+(** FIXME: actually close file *)
+let close_file (s : state) fd =
+  s, (Word0.wrepr Wsize.U64 (CoreConv.cz_of_int 1))
+
+
+(** FIXME: actually write to file*)
+let write_to_file (s: state) data fd =
+  s, data
+
+let read_from_file (s: state) data fd =
+  s, data
+
+let sc_sem : state Syscall.syscall_sem = {
+  get_random = get_random;
+  open_file =  open_file;
+  close_file = close_file;
+  write_to_file = write_to_file;
+  read_from_file = read_from_file;
+}

compiler/src/syscall_t.ml

@@ -1,2 +1,6 @@
 type 'a syscall_t =
   | RandomBytes of 'a
+  | Open of 'a
+  | Close
+  | Write of 'a
+  | Read of 'a