Add assertions

changes/01-feature/1389-assert.md

@@ -0,0 +1,2 @@
+- Add support for assertions; `assert` is now a keyword
+  ([PR 1389](https://github.com/jasmin-lang/jasmin/pull/1389)).

compiler/linter/Analyser/BackwardAnalyser.ml

@@ -42,6 +42,12 @@ module type Logic = sig
     -> exprs
     -> domain
     -> domain annotation
+
+    val assertion :
+      Location.i_loc ->
+      string ->
+      expr ->
+      domain -> domain Annotation.annotation
 end
 
 module type S = sig
@@ -199,6 +205,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)
+      | Cassert (msg, e) ->
+          let annotation = Annotation.bind annotation (L.assertion loc msg e) in
+          (Cassert (msg, e), annotation)
       | Ccall (lvs, fn, es) ->
           let annotation = Annotation.bind annotation (L.funcall loc lvs fn es) in
           (Ccall (lvs, fn, es), annotation)

compiler/linter/Analyser/BackwardAnalyser.mli

@@ -116,6 +116,15 @@ module type Logic =
       Jasmin.Expr.assgn_tag ->
       'asm Jasmin.Sopn.sopn ->
       Jasmin.Prog.exprs -> domain -> domain Annotation.annotation
+
+    (**
+    Function to handle assert instruction
+    *)
+    val assertion :
+      Jasmin.Location.i_loc ->
+      string ->
+      Jasmin.Prog.expr ->
+      domain -> domain Annotation.annotation
   end
 
 (**

compiler/linter/Analyser/ForwardAnalyser.ml

@@ -31,6 +31,8 @@ module type Logic = sig
 
   val opn :
     Location.i_loc -> lvals -> E.assgn_tag -> 'asm Sopn.sopn -> exprs -> domain -> domain annotation
+
+  val assertion : Location.i_loc -> string -> expr -> domain -> domain annotation
 end
 
 module type S = sig
@@ -180,6 +182,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)
+      | Cassert (msg, e) ->
+          let annotation = Annotation.bind annotation (Logic.assertion loc msg e) in
+          (Cassert (msg, e), annotation)
       | Ccall (lvs, fn, es) ->
           let annotation = Annotation.bind annotation (Logic.funcall loc lvs fn es) in
           (Ccall (lvs, fn, es), annotation)

compiler/linter/Analyser/ForwardAnalyser.mli

@@ -138,6 +138,16 @@ module type Logic =
       Jasmin.Expr.assgn_tag ->
       'asm Jasmin.Sopn.sopn ->
       Jasmin.Prog.exprs -> domain -> domain Annotation.annotation
+
+    (**
+    Function to handle assert instruction
+    *)
+    val assertion :
+      Jasmin.Location.i_loc ->
+      string ->
+      Jasmin.Prog.expr ->
+      domain -> domain Annotation.annotation
+
   end
 
 (**

compiler/linter/Analysis/Liveness/LivenessAnalyser.ml

@@ -77,6 +77,9 @@ module LivenessDomain : BackwardAnalyser.Logic with type domain = Sv.t = struct
     | Oslh _ | Oasm _ | Opseudo_op _ ->
       Annotation (live_assigns domain lvs exprs)
 
+  let assertion _loc _msg e domain =
+    Annotation (Sv.union domain (Prog.vars_e e))
+
 end
 
 include BackwardAnalyser.Make (LivenessDomain)

compiler/linter/Analysis/ReachingDefinitions/RDAnalyser.ml

@@ -38,6 +38,7 @@ module ReachingDefinitionLogic :
   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
+  let assertion loc _ _ domain = logic loc [] domain
 end
 
 include ForwardAnalyser.Make (ReachingDefinitionLogic)

compiler/linter/Checker/DeadVariables.ml

@@ -31,7 +31,7 @@ let create_dv_error_instr loc =
 let has_keep_tag =
   function
   | Cassgn (_, tag, _, _) | Copn (_, tag, _, _) -> tag = AT_keep
-  | Csyscall _ | Cif _ | Cfor _ | Cwhile _ | Ccall _ -> false
+  | Csyscall _ | Cif _ | Cfor _ | Cwhile _ | Ccall _ | Cassert _ -> false
 
 let check_func func =
   let dv_errors = ref [] in

compiler/linter/Checker/VariableInitialisation.ml

@@ -54,6 +54,7 @@ let check_func fd =
     | Copn (xs, _, _, es) | Csyscall (xs, _, es) | Ccall (xs, _, es) ->
         check_lvs i_info xs;
         check_es i_info es
+    | Cassert (_, e)
     | Cif (e, _, _) -> check_e i_info e
     | Cfor (_, (_, e1, e2), _) -> check_es i_info [ e1; e2 ]
     | Cwhile (_, _, e, (_, i), _) -> check_e i e

compiler/safetylib/safetyInterpreter.ml

@@ -112,6 +112,8 @@ type safe_cond =
   | NotEqual of op_kind * expr * expr
   | Termination of bool (* the boolean signals whether this is a severe violation *)
 
+  | GeneralCond of expr
+
 let notZero(ws, e) = NotEqual(Op_w ws, e, pcast ws (Pconst (Z.of_int 0)))
 
 let severe_violation =
@@ -166,6 +168,8 @@ let pp_safety_cond fmt = function
 
   | Termination b -> Format.fprintf fmt "termination%s" (if b then "" else " has not been checked")
 
+  | GeneralCond e -> Format.fprintf fmt "%a" pp_expr e
+
 type violation_loc =
   | InProg of Prog.L.i_loc
   | InReturn of funname
@@ -454,6 +458,7 @@ let safe_opn pd asmOp safe opn es =
 let safe_instr pd asmOp ginstr = match ginstr.i_desc with
   | Cassgn (lv, _, _, e) -> safe_e_rec (safe_lval lv) e
   | Copn (lvs,_,opn,es) -> safe_opn pd asmOp (safe_lvals lvs @ safe_es es) opn es
+  | Cassert (_, e) -> safe_e_rec [ GeneralCond e ] e
   | Cif(e, _, _) -> safe_e e
   | Cwhile(_, _, _, _, _) -> []       (* We check the while condition later. *)
   | Ccall(lvs, _, es) | Csyscall(lvs, _, es) -> safe_lvals lvs @ safe_es es
@@ -758,6 +763,12 @@ end = struct
         | Some c ->
           AbsDom.is_bottom (AbsDom.meet_btcons state.abs c) end
 
+    | GeneralCond e ->
+       let ne = Papp1 (Onot, e) in
+       begin match AbsExpr.bexpr_to_btcons ne state.abs with
+       | None -> false
+       | Some c -> AbsDom.is_bottom (AbsDom.meet_btcons state.abs c) end
+
     (* These are checked elsewhere *)
     | AlignedPtr _ | AlignedExpr _ | Valid _ | Termination _ -> true
 
@@ -1251,6 +1262,7 @@ end = struct
       | Cassgn (lv, _, _, e)    -> nm_lv vs_for lv && nm_e vs_for e
       | Copn (lvs, _, _, es)    -> nm_lvs vs_for lvs && nm_es vs_for es
       | Csyscall(lvs, _ ,es)    -> nm_lvs vs_for lvs && nm_es vs_for es
+      | Cassert(_, e)           -> nm_e vs_for e
       | Cif (e, st, st')        ->
         nm_e vs_for e && nm_stmt vs_for st && nm_stmt vs_for st'
       | Cfor (i, _, st)         -> nm_stmt (i :: vs_for) st
@@ -1465,6 +1477,8 @@ end = struct
       | Csyscall(lvs, sc, es) ->
          aeval_syscall state sc lvs es
 
+      | Cassert _ -> state
+
       | Cif(e,c1,c2) ->
         aeval_if ginstr e c1 c2 state
 

compiler/safetylib/safetyPreanalysis.ml

@@ -86,6 +86,8 @@ end = struct
       Cassgn (mk_lval fn lv, tag, ty, mk_expr fn e)
     | Copn (lvls, tag, opn, exprs) ->
       Copn (mk_lvals fn lvls, tag, opn, mk_exprs fn exprs)
+    | Cassert (msg, e) ->
+       Cassert (msg, mk_expr fn e)
     | Csyscall (lvls, o, exprs) ->
         Csyscall(mk_lvals fn lvls, o, mk_exprs fn exprs)
     | Cif (e, st, st') ->
@@ -357,6 +359,8 @@ end = struct
           | _ -> assert false
       else None
 
+    | Cassert _ -> None
+
     | Cif (_, c1, c2) ->
       begin match pa_flag_setfrom v c1, pa_flag_setfrom v c2 with
         | None, None -> None
@@ -380,6 +384,8 @@ end = struct
     | Copn (lvs, _, _, es) | Csyscall(lvs, _, es) -> List.fold_left (fun st lv ->
         List.fold_left (fun st e -> pa_lv st lv e) st es) st lvs
 
+    | Cassert _ -> st
+
     | Cif (b, c1, c2) ->
       let vs,st = expr_vars st b in
       let st = { st with if_conds = b :: st.if_conds } in
@@ -547,6 +553,7 @@ end = struct
       let sv = collect_vars_lv sv lv in
       collect_vars_e sv e
     | Ccall _ -> raise Fcall
+    | Cassert (_, e) ->  collect_vars_e sv e
 
   and collect_vars_is sv is = List.fold_left collect_vars_i sv is
 

compiler/src/alias.ml

@@ -252,6 +252,7 @@ let rec analyze_instr_r params cc a =
     | None -> a 
     | Some l -> link_array_return params a xs es l
     end
+  | Cassert _ -> a
   | Cif(_, s1, s2) ->
      let a1 = analyze_stmt params cc a s1 |> normalize_map in
      let a2 = analyze_stmt params cc a s2 |> normalize_map in

compiler/src/autoSpill.ml

@@ -42,13 +42,14 @@ let vars_i = function
   | Cassgn (x, _, _, e) -> Sv.union (vars_lv x) (vars_e e)
   | Copn (xs, _, _, es) | Csyscall (xs, _, es) | Ccall (xs, _, es) ->
       List.fold Sv.union (vars_es es) (List.map vars_lv xs)
+  | Cassert (_, e) -> vars_e e
   | Cfor _ | Cif _ | Cwhile _ -> assert false
 
 let rec spill_all_i strategy i =
   let wrap i_desc = { i with i_desc; i_annot = [] } in
   let op o xs = xs |> spillable strategy |> mk_spill o |> wrap in
   match i.i_desc with
-  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ ->
+  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ | Cassert _ ->
       [ op Unspill (vars_i i.i_desc); i; op Spill (assigns i.i_desc) ]
   | Cif (e, c1, c2) ->
       [

compiler/src/compile.ml

@@ -50,7 +50,7 @@ let rec warn_extra_i pd msfsize asmOp i =
   | Cfor _ ->
       hierror ~loc:(Lmore i.i_loc) ~kind:"compilation error" ~internal:true
         "for loop remains"
-  | Ccall _ | Csyscall _ -> ()
+  | Ccall _ | Csyscall _ | Cassert _ -> ()
 
 let warn_extra_fd pd msfsize asmOp (_, fd) = List.iter (warn_extra_i pd msfsize asmOp) fd.f_body
 

compiler/src/conv.ml

@@ -164,6 +164,10 @@ and cinstr_r_of_instr_r p i =
       C.Csyscall(clval_of_lvals x, o, cexpr_of_exprs e) in
     C.MkI(p, ir)
 
+  | Cassert (msg, e) ->
+     let ir = C.Cassert (msg, cexpr_of_expr e) in
+     C.MkI (p, ir)
+
   | Cif(e,c1,c2) ->
     let c1 = cstmt_of_stmt c1 in
     let c2 = cstmt_of_stmt c2 in
@@ -204,6 +208,9 @@ and instr_r_of_cinstr_r = function
   | C.Csyscall(x,o,e) ->
     Csyscall(lval_of_clvals x, o, expr_of_cexprs e)
 
+  | C.Cassert (msg, e) ->
+     Cassert (msg, expr_of_cexpr e)
+
   | C.Cif(e,c1,c2) ->
     let c1 = stmt_of_cstmt c1 in
     let c2 = stmt_of_cstmt c2 in

compiler/src/ct_checker_forward.ml

@@ -561,6 +561,9 @@ let rec ty_instr is_ct_asm fenv env i =
     let env, _ = ty_exprs_max ~public:true env es in
     ty_lvals1 env xs (declassify_lvl ~loc i.i_annot Secret)
 
+  (* We ignore the contents of assertion *)
+  | Cassert _ -> env
+
   | Cif(e, c1, c2) ->
     let env, _ = ty_expr ~public:true env e in
     let env1 = ty_cmd is_ct_asm fenv env c1 in

compiler/src/evaluator.ml

@@ -23,6 +23,7 @@ let pp_error fmt err =
   | ErrType  -> "type error"
   | ErrArith -> "arithmetic error"
   | ErrSemUndef -> "undefined semantics"
+  | ErrAssert _ -> "assertion violation"
 
 let exn_exec (ii:instr_info) (r: 't exec) = 
   match r with
@@ -109,6 +110,12 @@ let small_step1 ep spp sip s =
       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 }
 
+    | Cassert (p,a) ->
+      let v = exn_exec ii (sem_pexpr nosubword ep spp true gd s1 a) in
+      let b = of_val_b ii v in
+      if not b then raise (Eval_error(ii, ErrAssert p));
+      { s with s_cmd = c }
+
     | Cif(e,c1,c2) ->
       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

compiler/src/glob_options.ml

@@ -141,6 +141,7 @@ let set_cc cc =
   in call_conv := cc
 
 let print_strings = function
+  | Compiler.RemoveAssertion             -> "rmassert", "remove logical assertion"
   | Compiler.Typing                      -> "typing"   , "typing"
   | Compiler.ParamsExpansion             -> "cstexp"   , "param expansion"
   | Compiler.InsertRenaming              -> "rename"   , "add renaming assignments at export function boundaries"

compiler/src/insert_copy_and_fix_length.ml

@@ -105,7 +105,7 @@ and iac_instr_r pd loc ir =
       Csyscall(xs, Syscall_t.RandomBytes (ws, Conv.pos_of_int len), es)
     end
 
-  | Ccall _ -> ir
+  | Ccall _ | Cassert _ -> ir
 
 let iac_func pd f =
   { f with f_body = iac_stmt pd f.f_body }

compiler/src/latex_printer.ml

@@ -328,6 +328,8 @@ let rec pp_instr depth fmt (annot, p) =
     F.fprintf fmt "%a%a;"
       pp_expr e
       (pp_opt pp_sidecond) cnd
+  | PIAssert (msg, e) ->
+     F.fprintf fmt "%a(%a, %a)" kw "assert" pp_string (L.unloc msg) pp_expr e
   | PIIf (b, th, el) ->
     begin
     F.fprintf fmt "%a %a %a"

compiler/src/lexer.mll

@@ -63,6 +63,7 @@
     "from"  , FROM   ;
     "global", GLOBAL ;
     "if"    , IF     ;
+    "assert", ASSERT ;
     "inline", INLINE ;
     "mut"   , MUTABLE;
     "namespace", NAMESPACE;

compiler/src/liveness.ml

@@ -45,6 +45,10 @@ and live_d weak d (s_o: Sv.t) =
      else s_o in
     s_i, s_o, Copn(xs,t,o,es)
 
+  | Cassert (msg, e) ->
+     let s_i = Sv.union (vars_e e) s_o in
+     s_i, s_o, Cassert (msg, e)
+
   | Cif(e,c1,c2) ->
     let s1, c1 = live_c weak c1 s_o in
     let s2, c2 = live_c weak c2 s_o in
@@ -103,7 +107,7 @@ let iter_call_sites (cbf: L.i_loc -> funname -> lvals -> Sv.t * Sv.t -> unit)
       match i.i_desc with
       | Ccall (xs, fn, _) -> cbf i.i_loc fn xs i.i_info
       | Csyscall (xs, op, _) -> cbs i.i_loc op xs i.i_info
-      | (Cassgn _ | Copn _ | Cif _ | Cfor _ | Cwhile _) -> ()
+      | (Cassgn _ | Copn _ | Cif _ | Cfor _ | Cwhile _ | Cassert _) -> ()
     ) f.f_body
 
 let pp_info fmt (s1, s2) =
@@ -122,7 +126,7 @@ let rec conflicts_i cf i =
   let cf = merge_class cf s1 in
 
   match i.i_desc with
-  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ ->
+  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ | Cassert _ ->
     merge_class cf s2
   | Cfor( _, _, c) ->
     conflicts_c (merge_class cf s2) c

compiler/src/parser.mly

@@ -23,6 +23,7 @@
 %token ALIGNED
 %token AMP
 %token AMPAMP
+%token ASSERT
 %token BANG
 %token BANGEQ
 %token COLON
@@ -381,6 +382,9 @@ pinstr_r:
     { let { Location.pl_loc = loc; Location.pl_desc = (f, args) } = fc in
       PIAssign ((None, []), `Raw, Location.mk_loc loc (PECall (f, args)), c) }
 
+| ASSERT LPAREN msg=loc(STRING) COMMA e=pexpr RPAREN SEMICOLON
+    { PIAssert(msg, e) }
+
 | s=pif { s }
 
 | FOR v=var EQ ce1=pexpr TO ce2=pexpr is=pblock

compiler/src/pretyping.ml

@@ -2137,6 +2137,10 @@ let rec tt_instr arch_info (env : 'asm Env.env) ((pannot,pi) : S.pinstr) : 'asm
 
   | S.PIAssign (ls, eqop, pe, ocp) -> env, tt_assign env env ls eqop pe ocp
 
+  | PIAssert (msg, pe) ->
+     let e  = tt_expr_bool arch_info.pd env pe in
+     env, [mk_i (P.Cassert (L.unloc msg, e))]
+
   | PIIf (cp, st, sf) ->
       let c  = tt_expr_bool arch_info.pd env cp in
       let st = tt_block arch_info env st in
@@ -2236,7 +2240,7 @@ let rec add_reserved_i env (_,i) =
      List.fold_left (fun env id -> Env.add_reserved env (L.unloc id)) env ids
   | S.PIdeclinit (_, ids) ->
       List.fold_left (fun env id -> Env.add_reserved env (L.unloc (fst (L.unloc id)))) env ids
-  | PIArrayInit _ | PIAssign _ -> env
+  | PIArrayInit _ | PIAssign _ | PIAssert _ -> env
   | PIIf(_, c, oc) -> add_reserved_oc (add_reserved_c' env c) oc
   | PIFor(_, _, c) -> add_reserved_c' env c
   | PIWhile(oc1, _, oc2) -> add_reserved_oc (add_reserved_oc env oc1) oc2