get-random

compiler/jasmin.mlpack.in

@@ -3,6 +3,7 @@ src/Arch
 src/Arch_full
 src/Array_expand
 src/Conv
+src/CoreConv
 src/Ct_checker_forward
 src/Evaluator
 src/Help
@@ -29,6 +30,8 @@ src/Ssa
 src/StackAlloc
 src/Subst
 src/Syntax
+src/Syscall_ocaml
+src/Syscall_t
 src/ToEC
 src/safety/safetyAbsExpr
 src/safety/safetyConfig

compiler/src/alias.ml

@@ -170,16 +170,24 @@ let assign_arr params a x e =
   | None, _ | _, None -> a
   | Some d, Some s -> merge_slices params a d s
 
+let syscall_cc (o : Syscall_t.syscall_t) =
+  match o with
+  | Syscall_t.RandomBytes _ -> [Some 0]
+
+let link_array_return params a xs es cc =
+  List.fold_left2 (fun a x ->
+          function
+          | None -> a
+          | Some n -> assign_arr params a x (List.nth es n)
+        )
+        a xs cc
+
+
 let rec analyze_instr_r params cc a =
   function
   | Cfor _ -> assert false
-  | Ccall (_, xs, fn, es) ->
-     List.fold_left2 (fun a x ->
-         function
-         | None -> a
-         | Some n -> assign_arr params a x (List.nth es n)
-       )
-       a xs (cc fn)
+  | Ccall (_, xs, fn, es) -> link_array_return params a xs es (cc fn)
+  | Csyscall (xs, o, es) -> link_array_return params a xs es (syscall_cc o)
   | Cassgn (x, _, ty, e) -> if is_ty_arr ty then assign_arr params a x e else a
   | Copn _ -> a
   | Cif(_, s1, s2) ->

compiler/src/arch_full.ml

@@ -53,6 +53,7 @@ module type Arch = sig
   val callee_save_vars : var list
   val rsp_var : var
   val all_registers : var list
+  val syscall_kill : Sv.t
 end
 
 module Arch_from_Core_arch (A : Core_arch) : Arch = struct
@@ -186,4 +187,5 @@ module Arch_from_Core_arch (A : Core_arch) : Arch = struct
 
   let all_registers = reg_vars @ regx_vars @ xreg_vars @ flag_vars
 
+  let syscall_kill = Sv.diff (Sv.of_list all_registers) (Sv.of_list callee_save_vars)
 end

compiler/src/arch_full.mli

@@ -51,6 +51,7 @@ module type Arch = sig
   val callee_save_vars : var list
   val rsp_var : var
   val all_registers : var list
+  val syscall_kill : Sv.t
 end
 
 module Arch_from_Core_arch (A : Core_arch) : Arch

compiler/src/conv.ml

@@ -1,39 +1,11 @@
 open Var0
 open Prog
+include CoreConv
+
 module W = Wsize
 module T = Type
 module C = Expr
 
-let rec pos_of_z z =
-  let open Z.Compare in
-  if z <= Z.one then BinNums.Coq_xH
-  else
-    let p = pos_of_z (Z.shift_right z 1) in
-    if (Z.erem z (Z.of_int 2)) = Z.one
-    then BinNums.Coq_xI p
-    else BinNums.Coq_xO p
-
-let rec z_of_pos pos =
-  let open Z in
-  match pos with
-  | BinNums.Coq_xH   -> Z.one
-  | BinNums.Coq_xO p -> Z.shift_left (z_of_pos p) 1
-  | BinNums.Coq_xI p -> Z.shift_left (z_of_pos p) 1 + Z.one
-
-let cz_of_z z =
-  let open Z.Compare in
-  if z = Z.zero then BinNums.Z0
-  else if z < Z.zero then BinNums.Zneg (pos_of_z (Z.abs z))
-  else BinNums.Zpos (pos_of_z z)
-
-let z_of_cz z =
-  match z with
-  | BinNums.Zneg p -> Z.neg (z_of_pos p)
-  | BinNums.Z0     -> Z.zero
-  | BinNums.Zpos p -> z_of_pos p
-
-let cz_of_int i = cz_of_z (Z.of_int i)
-
 let z_of_nat n =
   z_of_cz (BinInt.Z.of_nat n)
 
@@ -277,11 +249,17 @@ and cinstr_r_of_instr_r tbl p i tl =
     let ir  =
       C.Cassgn(clval_of_lval tbl x, t, cty_of_ty ty, cexpr_of_expr tbl e) in
     C.MkI(p, ir) :: tl
+
   | Copn(x,t,o,e) ->
     let ir =
       C.Copn(clval_of_lvals tbl x, t, o, cexpr_of_exprs tbl e) in
     C.MkI(p, ir) :: tl
 
+  | Csyscall(x,o,e) ->
+    let ir =
+      C.Csyscall(clval_of_lvals tbl x, o, cexpr_of_exprs tbl e) in
+    C.MkI(p, ir) :: tl
+
   | Cif(e,c1,c2) ->
     let c1 = cstmt_of_stmt tbl c1 [] in
     let c2 = cstmt_of_stmt tbl c2 [] in
@@ -321,6 +299,9 @@ and instr_r_of_cinstr_r tbl = function
   | C.Copn(x,t,o,e) ->
     Copn(lval_of_clvals tbl x, t, o, expr_of_cexprs tbl e)
 
+  | C.Csyscall(x,o,e) ->
+    Csyscall(lval_of_clvals tbl x, o, expr_of_cexprs tbl e)
+
   | C.Cif(e,c1,c2) ->
     let c1 = stmt_of_cstmt tbl c1 in
     let c2 = stmt_of_cstmt tbl c2 in
@@ -484,3 +465,11 @@ let error_of_cerror pp_err tbl e =
     err_sub_kind = pass;
     err_internal = e.pel_internal;
   }
+
+(* -------------------------------------------------------------------------- *)
+let fresh_reg_ptr tbl name ty =
+  let name = string_of_string0 name in
+  let ty = ty_of_cty ty in
+  let p = Prog.V.mk name (Reg (Normal, Pointer Writable)) ty L._dummy [] in
+  let cp = cvar_of_var tbl p in
+  cp.Var0.Var.vname

compiler/src/conv.mli

@@ -72,3 +72,8 @@ val to_array :
 val error_of_cerror :
   (Format.formatter -> Compiler_util.pp_error -> unit) ->
   'info coq_tbl -> Compiler_util.pp_error_loc -> Utils.hierror
+
+
+(* ---------------------------------------------------- *)
+val fresh_reg_ptr :
+  'a coq_tbl -> 'b (* coq string *) -> Type.stype -> Eqtype.Equality.sort (* Var0.var *)

compiler/src/coreConv.ml

@@ -0,0 +1,30 @@
+let rec pos_of_z z =
+  let open Z.Compare in
+  if z <= Z.one then BinNums.Coq_xH
+  else
+    let p = pos_of_z (Z.shift_right z 1) in
+    if (Z.erem z (Z.of_int 2)) = Z.one
+    then BinNums.Coq_xI p
+    else BinNums.Coq_xO p
+
+let rec z_of_pos pos =
+  let open Z in
+  match pos with
+  | BinNums.Coq_xH   -> Z.one
+  | BinNums.Coq_xO p -> Z.shift_left (z_of_pos p) 1
+  | BinNums.Coq_xI p -> Z.shift_left (z_of_pos p) 1 + Z.one
+
+let cz_of_z z =
+  let open Z.Compare in
+  if z = Z.zero then BinNums.Z0
+  else if z < Z.zero then BinNums.Zneg (pos_of_z (Z.abs z))
+  else BinNums.Zpos (pos_of_z z)
+
+let z_of_cz z =
+  match z with
+  | BinNums.Zneg p -> Z.neg (z_of_pos p)
+  | BinNums.Z0     -> Z.zero
+  | BinNums.Zpos p -> z_of_pos p
+
+let cz_of_int i = cz_of_z (Z.of_int i)
+let int_of_cz z = Z.to_int (z_of_cz z)

compiler/src/ct_checker_forward.ml

@@ -496,7 +496,8 @@ let rec ty_instr fenv env i =
     let env, lvl = ty_expr ~public:false env e in
     ty_lval env x (declassify_lvl i.i_annot lvl)
 
-  | Copn(xs, _, _, es) ->
+  | Copn(xs, _, _, es) | Csyscall(xs, _, es) ->
+    (* FIXME syscall: syscall are assumed constant time ... *)
     let env, lvl = ty_exprs_max ~public:false env es in
     ty_lvals1 env xs (declassify_lvl i.i_annot lvl)
 

compiler/src/evaluator.ml

@@ -39,16 +39,16 @@ type 'asm stack =
       instr_info * 'asm fundef * lval list * sem_t exec Fv.t * 'asm instr list * 'asm stack
   | Sfor of instr_info * var_i * coq_Z list * 'asm instr list * 'asm instr list * 'asm stack
 
-type 'asm state = 
+type ('syscall_state, 'asm) state =
   { s_prog : 'asm prog;
     s_cmd  : 'asm instr list;
-    s_estate : estate;
+    s_estate : 'syscall_state estate;
     s_stk  : 'asm stack;
   }
 
 exception Final of Memory.mem * values
 
-let return pd s =
+let return pd (sc_sem: 'syscall_state Syscall.syscall_sem) s =
   assert (s.s_cmd = []);
   match s.s_stk with
   | Sempty(ii, f) ->
@@ -61,12 +61,11 @@ let return pd s =
 
   | Scall(ii,f,xs,vm1,c,stk) ->
     let gd = s.s_prog.p_globs in
-    let s2 = s.s_estate in
-    let m2 = s2.emem and vm2 = s2.evm 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
     let vres' = exn_exec ii (mapM2 ErrType truncate_val f.f_tyout vres) in
-    let s1 = exn_exec ii (write_lvals pd gd {emem = m2; evm = vm1 } xs vres') in
+    let s1 = exn_exec ii (write_lvals pd sc_sem gd {escs = scs2; emem = m2; evm = vm1 } xs vres') in
     { s with 
       s_cmd = c;
       s_estate = s1;
@@ -76,80 +75,86 @@ let return pd s =
     match ws with
     | [] -> { s with s_cmd = c; s_stk = stk }
     | w::ws ->
-      let s1 = exn_exec ii (write_var pd i (Vint w) s.s_estate) in
+      let s1 = exn_exec ii (write_var pd sc_sem i (Vint w) s.s_estate) in
       { s with s_cmd = body;
                s_estate = s1;
                s_stk = Sfor(ii, i, ws, body, c, stk) }
 
-let small_step1 pd asmOp s =
+let small_step1 pd (sc_sem: 'syscall_state Syscall.syscall_sem) asmOp s =
   match s.s_cmd with
-  | [] -> return pd s
+  | [] -> return pd sc_sem s
   | i :: c ->
     let MkI(ii,ir) = i in
     let gd = s.s_prog.p_globs in
     let s1 = s.s_estate in
     match ir with
 
     | Cassgn(x,_,ty,e) ->
-      let v  = exn_exec ii (sem_pexpr pd gd s1 e) in
+      let v  = exn_exec ii (sem_pexpr pd sc_sem gd s1 e) in
       let v' = exn_exec ii (truncate_val ty v) in
-      let s2 = exn_exec ii (write_lval pd gd x v' s1) in
+      let s2 = exn_exec ii (write_lval pd sc_sem gd x v' s1) in
       { s with s_cmd = c; s_estate = s2 }
 
     | Copn(xs,_,op,es) ->
-      let s2 = exn_exec ii (sem_sopn pd asmOp gd op s1 xs es) in
+      let s2 = exn_exec ii (sem_sopn pd sc_sem 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 pd sc_sem gd s1 es) in
+        let ((scs, m), vs) = exn_exec ii (exec_syscall pd sc_sem s1.escs s1.emem o ves) in
+        let s2 = exn_exec ii (write_lvals pd sc_sem 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 pd gd s1 e)) in
+      let b = of_val_b ii (exn_exec ii (sem_pexpr pd sc_sem 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 pd gd s1 lo)) in
-      let vhi = of_val_z ii (exn_exec ii (sem_pexpr pd gd s1 hi)) in
+      let vlo = of_val_z ii (exn_exec ii (sem_pexpr pd sc_sem gd s1 lo)) in
+      let vhi = of_val_z ii (exn_exec ii (sem_pexpr pd sc_sem 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
-      return pd s
+      return pd sc_sem s
 
     | Cwhile (_, c1, e, c2) ->
       { s with s_cmd = c1 @ MkI(ii, Cif(e, c2@[i],[])) :: c }
 
     | Ccall(_,xs,fn,es) ->
-      let vargs' = exn_exec ii (sem_pexprs pd gd s1 es) in
+      let vargs' = exn_exec ii (sem_pexprs pd sc_sem gd s1 es) in
       let f = 
         match get_fundef s.s_prog.p_funcs fn with
         | Some f -> f
         | None -> assert false in
       let vargs = exn_exec ii (mapM2 ErrType truncate_val f.f_tyin vargs') in
-      let m1 = s1.emem and vm1 = s1.evm in
+      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 pd f.f_params vargs {emem = m1; evm = vmap0}) in
+        exn_exec ii (write_vars pd sc_sem f.f_params vargs {escs; emem = m1; evm = vmap0}) in
       {s with s_cmd = f.f_body;
               s_estate = sf;
               s_stk = stk }
 
 
-let rec small_step pd asmOp s =
-  small_step pd asmOp (small_step1 pd asmOp s)
+let rec small_step pd sc_sem asmOp s =
+  small_step pd sc_sem asmOp (small_step1 pd sc_sem asmOp s)
 
-let init_state p fn m = 
+let init_state scs0 p fn m =
   let f = 
     match get_fundef p.p_funcs fn with
     | Some f -> f
     | None -> assert false in
   assert (f.f_tyin = []);
   { s_prog = p;
     s_cmd = f.f_body;
-    s_estate = {emem = m; evm = vmap0 };
+    s_estate = {escs = scs0; emem = m; evm = vmap0 };
     s_stk = Sempty(Coq_xO Coq_xH, f) }
 
 
-let exec pd asmOp p fn m =
-  let s = init_state p fn m in
-  try small_step pd asmOp s
+let exec pd sc_sem asmOp scs0 p fn m =
+  let s = init_state scs0 p fn m in
+  try small_step pd sc_sem asmOp s
   with Final(m,vs) -> m, vs 
 
 (* ----------------------------------------------------------- *)

compiler/src/evaluator.mli

@@ -1,12 +1,13 @@
 exception Eval_error of Expr.instr_info * Utils0.error
 
 val exec :
-  Wsize.wsize ->
-  'asm Sopn.asmOp ->
-  'asm Expr.prog ->
+  Wsize.coq_PointerData ->
+  'a Syscall.syscall_sem ->
+  'b Sopn.asmOp ->
+  'a Syscall.syscall_state_t Syscall.syscall_state_t ->
+  'b Expr.prog ->
   Utils0.funname ->
-  Low_memory.Memory.mem ->
-  Low_memory.Memory.mem * Values.values
+  Low_memory.Memory.mem -> Low_memory.Memory.mem * Values.values
 
 val pp_val : Format.formatter -> Values.value -> unit