Arrays with non-constant lengths

compiler/linter/Analyser/BackwardAnalyser.ml

@@ -15,12 +15,12 @@ module type Logic = sig
 
   val forget : var_i -> domain -> domain annotation
 
-  val funcall : Location.i_loc -> lvals -> funname -> exprs -> domain -> domain annotation
+  val funcall : Location.i_loc -> lvals -> funname -> length list -> exprs -> domain -> domain annotation
 
   val syscall :
        Location.i_loc
     -> lvals
-    -> (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t
+    -> (Wsize.wsize * length) Syscall_t.syscall_t
     -> exprs
     -> domain
     -> domain annotation
@@ -199,9 +199,9 @@ struct
       | Copn (lvs, tag, sopn, es) ->
           let annotation = Annotation.bind annotation (L.opn loc lvs tag sopn es) in
           (Copn (lvs, tag, sopn, es), annotation)
-      | Ccall (lvs, fn, es) ->
-          let annotation = Annotation.bind annotation (L.funcall loc lvs fn es) in
-          (Ccall (lvs, fn, es), annotation)
+      | Ccall (lvs, fn, al, es) ->
+          let annotation = Annotation.bind annotation (L.funcall loc lvs fn al es) in
+          (Ccall (lvs, fn, al, es), annotation)
       | Csyscall (lvs, sc, es) ->
           let annotation = Annotation.bind annotation (L.syscall loc lvs sc es) in
           (Csyscall (lvs, sc, es), annotation)

compiler/linter/Analyser/BackwardAnalyser.mli

@@ -86,6 +86,7 @@ module type Logic =
       Jasmin.Location.i_loc ->
       Jasmin.Prog.lvals ->
       Jasmin.CoreIdent.funname ->
+      Jasmin.Prog.length list ->
       Jasmin.Prog.exprs -> domain -> domain Annotation.annotation
 
     (**
@@ -94,7 +95,7 @@ module type Logic =
     val syscall :
       Jasmin.Location.i_loc ->
       Jasmin.Prog.lvals ->
-      (Jasmin.Wsize.wsize * Jasmin.BinNums.positive) Jasmin.Syscall_t.syscall_t ->
+      (Jasmin.Wsize.wsize * Jasmin.CoreIdent.length) Jasmin.Syscall_t.syscall_t ->
       Jasmin.Prog.exprs -> domain -> domain Annotation.annotation
 
     (**

compiler/linter/Analyser/ForwardAnalyser.ml

@@ -17,12 +17,12 @@ module type Logic = sig
 
   val forget : var_i -> domain -> domain annotation
 
-  val funcall : Location.i_loc -> lvals -> funname -> exprs -> domain -> domain annotation
+  val funcall : Location.i_loc -> lvals -> funname -> length list -> exprs -> domain -> domain annotation
 
   val syscall :
        Location.i_loc
     -> lvals
-    -> (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t
+    -> (Wsize.wsize * length) Syscall_t.syscall_t
     -> exprs
     -> domain
     -> domain annotation
@@ -180,9 +180,9 @@ module Make (Logic : Logic) : S with type domain = Logic.domain = struct
       | Copn (lvs, tag, sopn, es) ->
           let annotation = Annotation.bind annotation (Logic.opn loc lvs tag sopn es) in
           (Copn (lvs, tag, sopn, es), annotation)
-      | Ccall (lvs, fn, es) ->
-          let annotation = Annotation.bind annotation (Logic.funcall loc lvs fn es) in
-          (Ccall (lvs, fn, es), annotation)
+      | Ccall (lvs, fn, al, es) ->
+          let annotation = Annotation.bind annotation (Logic.funcall loc lvs fn al es) in
+          (Ccall (lvs, fn, al, es), annotation)
       | Csyscall (lvs, sc, es) ->
           let annotation = Annotation.bind annotation (Logic.syscall loc lvs sc es) in
           (Csyscall (lvs, sc, es), annotation)

compiler/linter/Analyser/ForwardAnalyser.mli

@@ -108,6 +108,7 @@ module type Logic =
       Jasmin.Location.i_loc ->
       Jasmin.Prog.lvals ->
       Jasmin.CoreIdent.funname ->
+      Jasmin.Prog.length list ->
       Jasmin.Prog.exprs -> domain -> domain Annotation.annotation
 
     (**
@@ -116,7 +117,7 @@ module type Logic =
     val syscall :
       Jasmin.Location.i_loc ->
       Jasmin.Prog.lvals ->
-      (Jasmin.Wsize.wsize * Jasmin.BinNums.positive) Jasmin.Syscall_t.syscall_t ->
+      (Jasmin.Wsize.wsize * Jasmin.CoreIdent.length) Jasmin.Syscall_t.syscall_t ->
       Jasmin.Prog.exprs -> domain -> domain Annotation.annotation
 
     (**

compiler/linter/Analysis/Liveness/LivenessAnalyser.ml

@@ -43,13 +43,13 @@ module LivenessDomain : BackwardAnalyser.Logic with type domain = Sv.t = struct
     assert (not (Sv.mem (L.unloc var) domain));
     Annotation domain
 
-  let funcall (_ : Location.i_loc) (lvs : lvals) (_ : funname) (exprs : exprs) (domain : domain) =
+  let funcall (_ : Location.i_loc) (lvs : lvals) (_ : funname) (_ : length list) (exprs : exprs) (domain : domain) =
       Annotation (live_assigns domain lvs exprs)
 
   let syscall
     (_ : Location.i_loc)
     (lvs : lvals)
-    (_ : (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t)
+    (_ : (Wsize.wsize * length) Syscall_t.syscall_t)
     (exprs : exprs)
     (domain : domain) =
     Annotation (live_assigns domain lvs exprs)

compiler/linter/Analysis/ReachingDefinitions/RDAnalyser.ml

@@ -34,7 +34,7 @@ module ReachingDefinitionLogic :
     Annotation
       (RDDomain.add (List.fold_left written_lv Sv.empty lvs) loc domain)
 
-  let funcall loc lvs _ _ domain = logic loc lvs domain
+  let funcall loc lvs _ _ _ domain = logic loc lvs domain
   let syscall loc lvs _ _ domain = logic loc lvs domain
   let assign loc lv _ _ _ domain = logic loc [ lv ] domain
   let opn loc lvs _ _ _ domain = logic loc lvs domain

compiler/linter/Checker/VariableInitialisation.ml

@@ -51,7 +51,7 @@ let check_func fd =
     | Cassgn (x, _, _, e) ->
         check_lv i_info x;
         check_e i_info e
-    | Copn (xs, _, _, es) | Csyscall (xs, _, es) | Ccall (xs, _, es) ->
+    | Copn (xs, _, _, es) | Csyscall (xs, _, es) | Ccall (xs, _, _, es) ->
         check_lvs i_info xs;
         check_es i_info es
     | Cif (e, _, _) -> check_e i_info e

compiler/safetylib/safetyAbsExpr.ml

@@ -27,7 +27,13 @@ type msub = int gmsub
 let check_msub ms =
   let gv = ms.ms_v in
   (* array size, in bytes   *)
-  let arr_size = arr_range gv * (size_of_ws (arr_size gv)) in
+  let len = arr_range gv in
+  let len =
+    match len with
+    | Const len -> len
+    | _ -> assert false
+  in
+  let arr_size = len * (size_of_ws (arr_size gv)) in
   (* sub-array size, in bytes * *)
   let sub_size = ms.ms_len * (size_of_ws ms.ms_ws) in
   let offset = ms.ms_offset in
@@ -39,10 +45,16 @@ let check_msubo ms = match ms.ms_offset with
   | Some off -> check_msub { ms with ms_offset = off }
 
 let msub_of_arr gv sc =
+  let len = arr_range gv in
+  let len =
+    match len with
+    | Const len -> len
+    | _ -> assert false
+  in
   let msub = { ms_v      = gv;
                ms_sc     = sc;
                ms_ws     = arr_size gv;
-               ms_len    = arr_range gv;
+               ms_len    = len;
                ms_offset = Some 0; } in
   check_msubo msub;
   msub
@@ -215,15 +227,15 @@ let print_not_word_expr e =
   Format.eprintf "@[<v>Should be a word expression:@;\
                   @[%a@]@;Type:@;@[%a@]@]@."
     (Printer.pp_expr ~debug:(!Glob_options.debug)) e
-    (PrintCommon.pp_ty) (Conv.ty_of_cty (Conv.cty_of_ty (ty_expr e)))
+    (PrintCommon.pp_ty ~debug:false) (Conv.ty_of_cty (Conv.cty_of_ty (ty_expr e)))
 
 let check_is_int v =
   let gv = L.unloc v.gv in
   match gv.v_ty with
   | Bty Int -> ()
   | _ ->
     Format.eprintf "%s should be an int but is a %a@."
-      gv.v_name PrintCommon.pp_ty gv.v_ty;
+      gv.v_name (PrintCommon.pp_ty ~debug:false) gv.v_ty;
     raise (Aint_error "Bad type")
 
 let check_is_word v =
@@ -232,7 +244,7 @@ let check_is_word v =
   | Bty (U _) -> ()
   | _ ->
     Format.eprintf "%s should be a word but is a %a@."
-      gv.v_name PrintCommon.pp_ty gv.v_ty;
+      gv.v_name (PrintCommon.pp_ty ~debug:false) gv.v_ty;
     raise (Aint_error "Bad type")
 
 
@@ -415,8 +427,14 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
 
   (*-------------------------------------------------------------------------*)
   let arr_full_range x =
+    let len = arr_range x in
+    let len =
+      match len with
+      | Const len -> len
+      | _ -> assert false
+    in
     List.init
-      (arr_range x * size_of_ws (arr_size x))
+      (len * size_of_ws (arr_size x))
       (fun i -> AarraySlice (x, U8, i))
 
   (* let abs_arr_range_at abs x acc ws ei = match aeval_cst_int abs ei with
@@ -451,7 +469,7 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
 
   (*-------------------------------------------------------------------------*)
   (* Collect all variables appearing in e. *)
-  let ptr_expr_of_expr abs e =
+  let ptr_expr_of_expr abs (e:length gexpr) =
     let exception Expr_contain_load in
     let rec aux acc e = match e with
       | Pbool _ | Parr_init _ | Pconst _ -> acc
@@ -461,6 +479,11 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
       | Pget(_, access,ws,x,ei) ->
         abs_sub_arr_range abs (L.unloc x.gv,x.gs) access ws 1   ei @ acc
       | Psub (access, ws, len, x, ei) ->
+        let len =
+          match len with
+          | Const len -> len
+          | _ -> assert false
+        in
         abs_sub_arr_range abs (L.unloc x.gv,x.gs) access ws len ei @ acc
 
       | Papp1 (_, e1) -> aux acc e1
@@ -1067,6 +1090,11 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
       end
 
     | Lasub (acc, ws, len, x, ei) ->
+      let len =
+        match len with
+        | Const len -> len
+        | _ -> assert false
+      in
       let offset = match aeval_cst_int abs ei with
         | Some i -> Some (access_offset acc ws i)
         | None -> None in
@@ -1078,7 +1106,7 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
 
       MLasub (loc, msub)
 
-  let apply_offset_expr abs outv info (inv : int ggvar) offset_expr =
+  let apply_offset_expr abs outv info (inv : length ggvar) offset_expr =
     (* Global variable cannot alias to a input pointer. *)
     assert (inv.gs = Expr.Slocal);
     let inv = L.unloc inv.gv in
@@ -1145,6 +1173,11 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
 
   let msub_of_sub_expr abs = function
     | Psub (acc, ws, len, ggv, ei) ->
+      let len =
+        match len with
+        | CoreIdent.Const len -> len
+        | _ -> assert false
+      in
       let offset = match aeval_cst_int abs ei with
         | Some i -> Some (access_offset acc ws i)
         | None -> None in

compiler/safetylib/safetyAbsExpr.mli

@@ -14,7 +14,7 @@ val pcast : wsize -> expr -> expr
 
 val wsize_of_ty : 'a gty -> int
 
-val check_is_word : int ggvar -> unit
+val check_is_word : length ggvar -> unit
 
 (*---------------------------------------------------------------*)
 type 'a gmsub = { ms_v      : var;

compiler/safetylib/safetyInterpreter.ml

@@ -39,7 +39,7 @@ let pp_s_env fmt env =
   Format.printf fmt "@[<v>global variables:@;%a@]"
     (pp_list (fun fmt (_,(x,sw)) ->
          Format.fprintf fmt "@[%s: %a@]@,"
-           x PrintCommon.pp_ty (Conv.ty_of_cty sw)))
+           x (PrintCommon.pp_ty ~debug:false) (Conv.ty_of_cty sw)))
     (Sv.to_list env.s_glob)
     (pp_list (fun fmt i -> Format.fprintf fmt "%d" i))
 
@@ -133,6 +133,7 @@ let pp_ows fmt ws =
 
 let pp_arr_slice fmt slice =
   let open PrintCommon in
+  let pp_len = pp_len ~debug:false in
   let pp_var = Printer.pp_var ~debug:false in
   let pp_expr = Printer.pp_expr ~debug:false in
   let ws = non_default_wsize slice.as_arr slice.as_wsize in
@@ -141,7 +142,7 @@ let pp_arr_slice fmt slice =
       slice.as_arr slice.as_offset
   else
     pp_arr_slice pp_var pp_expr pp_len fmt slice.as_access ws slice.as_arr
-      slice.as_offset slice.as_len
+      slice.as_offset (Const slice.as_len)
 
 let pp_safety_cond fmt = function
   | Initv x -> Format.fprintf fmt "is_init %a" pp_var x
@@ -227,7 +228,7 @@ let add64 x e = Papp2 (E.Oadd ( E.Op_w U64), Pvar x, e)
 let in_bound x access ws e len =
   let ux = L.unloc x in
   match ux.v_ty with
-  | Arr(ws',n) -> [InBound ( n * size_of_ws ws',
+  | Arr(ws',Prog.Const n) -> [InBound ( n * size_of_ws ws',
                              { as_arr = ux;
                                as_len = len;
                                as_wsize = ws;
@@ -349,6 +350,11 @@ let rec safe_e_rec safe = function
     safe
 
   | Psub (access, ws, len, x, e) ->
+    let len =
+      match len with
+      | Const len -> len
+      | _ -> assert false
+    in
     in_bound    x.gv access ws e len @
     (* Remark that we do not have to check initialization for sub-arrays. *)
     (* Note that the length is scaled with the word-size, so we only
@@ -383,6 +389,11 @@ let safe_lval = function
     safe_e_rec [] e
 
   | Lasub(access,ws,len,x,e) ->
+    let len =
+      match len with
+      | Const len -> len
+      | _ -> assert false
+    in
     in_bound x access ws e len @
     arr_aligned (* x  *) access ws e @
     safe_e_rec [] e
@@ -430,6 +441,11 @@ let safe_opn safe opn es =
          let n = Papp2 (E.Omod (Unsigned, Op_int), n, Pconst (Z.of_int 32)) in
          [ InRange(Pconst (Conv.z_of_cz lo), Pconst (Conv.z_of_cz hi), n) ]
       | Wsize.AllInit(ws, p, i) ->
+        let p =
+          match p with
+          | Type.ALConst p -> p
+          | _ -> assert false
+        in
         let e = List.nth es (Conv.int_of_nat i) in
         let y = match e with Pvar y -> y | _ -> assert false in
         List.flatten
@@ -467,7 +483,7 @@ let safe_instr ginstr = match ginstr.i_desc with
   | Copn (lvs,_,opn,es) -> safe_opn (safe_lvals lvs @ safe_es es) opn es
   | Cif(e, _, _) -> safe_e e
   | Cwhile(_, _, _, _, _) -> []       (* We check the while condition later. *)
-  | Ccall(lvs, _, es) | Csyscall(lvs, _, es) -> safe_lvals lvs @ safe_es es
+  | Ccall(lvs, _, _, es) | Csyscall(lvs, _, es) -> safe_lvals lvs @ safe_es es
   | Cfor (_, (_, e1, e2), _) -> safe_es [e1;e2]
 
 let safe_return main_decl =
@@ -1622,7 +1638,7 @@ end = struct
       | Cfor (i, _, st)         -> nm_stmt (i :: vs_for) st
       | Cwhile (_, st1, e, _, st2) ->
         nm_e vs_for e && nm_stmt vs_for st1 && nm_stmt vs_for st2
-      | Ccall (lvs, fn, es)  ->
+      | Ccall (lvs, fn, _al, es)  ->
         let f' = get_fun_def prog fn |> oget in
         nm_lvs vs_for lvs && nm_es vs_for es && nm_fdecl f'
 
@@ -1755,7 +1771,12 @@ end = struct
   let aeval_syscall state sc lvs _es =
     match sc with
     | Syscall_t.RandomBytes (ws, len) ->
-       let n = BinInt.Z.to_pos (Type.arr_size ws len) in
+       let len =
+         match len with
+         | Prog.Const len -> len
+         | _ -> assert false
+       in
+       let n = Conv.pos_of_int (Prog.arr_size ws len) in
        let cells = match lvs with
          | [ Lnone _ ] -> []
          | [ Lvar x ] -> cells_of_array x 0 n
@@ -2054,7 +2075,7 @@ end = struct
         { state with abs = abs; }
 
 
-      | Ccall(lvs, f, es) ->
+      | Ccall(lvs, f, _al, es) ->
         let f_decl = get_fun_def state.prog f |> oget in
         let fn = f_decl.f_name in