Improvements for ASL parser

- Fix pretty printing nested constraints

- Add flow typing for if condition then { throw exn }; ... blocks

- Add optimisations for bitvector concatenation in C

8 files changed, 73 insertions, 52 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 5003e432..326f742a 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -494,6 +494,24 @@ let analyze_primop' ctx id args typ =
   | "undefined_bit", _ ->
      AE_val (AV_C_fragment (F_lit (V_bit Sail2_values.B0), typ, CT_bit))
 
+  (* Optimized routines for all combinations of fixed and small bits
+     appends, where the result is guaranteed to be smaller than 64. *)
+  | "append", [AV_C_fragment (vec1, _, CT_fbits (n1, ord1)); AV_C_fragment (vec2, _, CT_fbits (n2, ord2))]
+       when ord1 = ord2 && n1 + n2 <= 64 ->
+     AE_val (AV_C_fragment (F_op (F_op (vec1, "<<", v_int n2), "|", vec2), typ, CT_fbits (n1 + n2, ord1)))
+
+  | "append", [AV_C_fragment (vec1, _, CT_sbits ord1); AV_C_fragment (vec2, _, CT_fbits (n2, ord2))]
+       when ord1 = ord2 && is_sbits_typ ctx typ ->
+     AE_val (AV_C_fragment (F_call ("append_sf", [vec1; vec2; v_int n2]), typ, ctyp_of_typ ctx typ))
+
+  | "append", [AV_C_fragment (vec1, _, CT_fbits (n1, ord1)); AV_C_fragment (vec2, _, CT_sbits ord2)]
+       when ord1 = ord2 && is_sbits_typ ctx typ ->
+     AE_val (AV_C_fragment (F_call ("append_fs", [vec1; v_int n1; vec2]), typ, ctyp_of_typ ctx typ))
+
+  | "append", [AV_C_fragment (vec1, _, CT_sbits ord1); AV_C_fragment (vec2, _, CT_sbits ord2)]
+       when ord1 = ord2 && is_sbits_typ ctx typ ->
+     AE_val (AV_C_fragment (F_call ("append_ss", [vec1; vec2]), typ, ctyp_of_typ ctx typ))
+
   | "undefined_vector", [AV_C_fragment (len, _, _); _] ->
      begin match destruct_vector ctx.tc_env typ with
      | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
@@ -2537,7 +2555,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
        | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp)
        | fname, _ -> fname
      in
-     if fname = "reg_deref" then
+     if fname = "sail_assert" && !optimize_experimental then
+       empty
+     else if fname = "reg_deref" then
        if is_stack_ctyp ctyp then
          string (Printf.sprintf  " %s = *(%s);" (sgen_clexp_pure x) c_args)
        else
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4dd72980..bd32a8e3 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -731,26 +731,12 @@ let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (unit type_de
     let ranges = List.map (fun (id, range) -> (to_ast_id id, to_ast_range range)) ranges in
     TD_aux(TD_bitfield(id,typ,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
 
-let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (unit kind_def) envs_out =
+let to_ast_kdef (names, k_env, def_ord) (td:Parse_ast.kind_def) : unit kind_def =
   match td with
-  | Parse_ast.KD_aux(td,l) ->
-  (match td with
-  | Parse_ast.KD_abbrev(kind,id,name_scm_opt,typschm) ->
-    let id = to_ast_id id in
-    let key = id_to_string id in
-    let (kind,k) = to_ast_kind k_env kind in
-    (match k.k with
-     | K_Nat ->
-       let kd_nabrv =
-         (match typschm with
-          | Parse_ast.TypSchm_aux(Parse_ast.TypSchm_ts(Parse_ast.TypQ_aux(tq,_),atyp),_) ->
-            (match tq with
-             | Parse_ast.TypQ_no_forall ->
-               KD_aux(KD_nabbrev(kind,id,to_ast_namescm name_scm_opt, to_ast_nexp k_env atyp), (l,()))
-             | _ -> typ_error l "Def with kind Nat cannot have universal quantification" None None None)) in
-       kd_nabrv,(names,Envmap.insert k_env (key, k),def_ord)
-     | _ -> assert false
-    ))
+  | Parse_ast.KD_aux (Parse_ast.KD_nabbrev (kind, id, name_scm_opt, atyp), l) ->
+     let id = to_ast_id id in
+     let (kind, k) = to_ast_kind k_env kind in
+     KD_aux (KD_nabbrev (kind, id, to_ast_namescm name_scm_opt, to_ast_nexp k_env atyp), (l, ()))
 
 let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
   Rec_aux((match r with
@@ -892,7 +878,7 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
   | Parse_ast.DEF_fixity (prec, n, op) ->
      ((Finished(DEF_fixity (to_ast_prec prec, n, to_ast_id op)),envs),partial_defs)
   | Parse_ast.DEF_kind(k_def) ->
-     let kd,envs = to_ast_kdef envs k_def in
+     let kd = to_ast_kdef envs k_def in
      ((Finished(DEF_kind(kd))),envs),partial_defs
   | Parse_ast.DEF_type(t_def) ->
      let td,envs = to_ast_typedef envs t_def in
diff --git a/src/lexer.mll b/src/lexer.mll
index de8eed7f..f5a982eb 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -145,6 +145,7 @@ let kw_table =
      ("return",                  (fun x -> Return));
      ("scattered",               (fun x -> Scattered));
      ("sizeof",                  (fun x -> Sizeof));
+     ("constant",                (fun x -> Constant));
      ("constraint",              (fun x -> Constraint));
      ("struct",                  (fun x -> Struct));
      ("then",                    (fun x -> Then));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 30f87bc3..ddff51ea 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -494,7 +494,7 @@ val_spec_aux =  (* Value type specification *)
 
 type 
 kind_def_aux =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
-   KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
+   KD_nabbrev of kind * id * name_scm_opt * atyp (* type abbreviation *)
 
 type 
 dec_spec_aux =  (* Register declarations *)
diff --git a/src/parser.mly b/src/parser.mly
index 12286e13..fec38669 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -178,7 +178,7 @@ let rec desugar_rchain chain s e =
 %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Where
 %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Cast
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
-%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
+%token Undefined Union Newtype With Val Constant Constraint Throw Try Catch Exit Bitfield
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Mutual Var Ref Configuration
 
@@ -1446,6 +1446,10 @@ def:
     { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) }
   | default_def
     { DEF_default $1 }
+  | Constant id Eq typ
+    { DEF_kind (KD_aux (KD_nabbrev (K_aux (K_kind [BK_aux (BK_int, loc $startpos($1) $endpos($1))],
+					   loc $startpos($1) $endpos($1)), $2, mk_namesectn, $4),
+			loc $startpos $endpos)) }
   | Constraint id Lparen kid_list Rparen Eq nc
     { DEF_constraint ($2, $4, $7) }
   | Mutual Lcurly fun_def_list Rcurly
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 792c3d23..a2771ae1 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -151,7 +151,7 @@ let doc_nc nc =
     | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
     | _ -> atomic_nc nc
   in
-  nc0 (constraint_simp nc)
+  nc0 ~parenthesize:true (constraint_simp nc)
 
 let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   match typ_aux with
@@ -159,16 +159,15 @@ let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   | Typ_app (id, []) -> doc_id id
   | Typ_app (Id_aux (DeIid str, _), [x; y]) ->
      separate space [doc_typ_arg x; doc_typ_arg y]
-              (*
-  | Typ_app (id, [_; len; _; Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]) when Id.compare (mk_id "vector") id == 0 && Id.compare (mk_id "bit") tid == 0->
-     string "bits" ^^ parens (doc_typ_arg len)
-               *)
-  | Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 -> string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
+  | Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 ->
+     string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
   | Typ_var kid -> doc_kid kid
   (* Resugar set types like {|1, 2, 3|} *)
-  | Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
+  | Typ_exist ([kid1],
+               NC_aux (NC_set (kid2, ints), _),
+               Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
          when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 ->
      enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints)
   | Typ_exist (kids, nc, typ) ->
@@ -371,21 +370,16 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_assign (lexp, exp) ->
      separate space [doc_lexp lexp; equals; doc_exp exp]
   | E_for (id, exp1, exp2, exp3, order, exp4) ->
-     begin
-       let header =
-         string "foreach" ^^ space ^^
-           group (parens (separate (break 1)
-                                   [ doc_id id;
-                                     string "from " ^^ doc_atomic_exp exp1;
-                                     string "to " ^^ doc_atomic_exp exp2;
-                                     string "by " ^^ doc_atomic_exp exp3;
-                                     string "in " ^^ doc_ord order ]))
-       in
-       match exp4 with
-       | E_aux (E_block [_], _) -> header ^//^ doc_exp exp4
-       | E_aux (E_block _, _) -> header ^^ space ^^ doc_exp exp4
-       | _ -> header ^//^ doc_exp exp4
-     end
+     let header =
+       string "foreach" ^^ space ^^
+         group (parens (separate (break 1)
+                                 [ doc_id id;
+                                   string "from " ^^ doc_atomic_exp exp1;
+                                   string "to " ^^ doc_atomic_exp exp2;
+                                   string "by " ^^ doc_atomic_exp exp3;
+                                   string "in " ^^ doc_ord order ]))
+     in
+     header ^^ space ^^ doc_exp exp4
   (* Resugar an assert with an empty message *)
   | E_throw exp -> string "throw" ^^ parens (doc_exp exp)
   | E_try (exp, pexps) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 23629b51..81f5fe6d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2301,6 +2301,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
             in
             let texp = annot_exp_effect (E_assert (constr_exp, checked_msg)) unit_typ (mk_effect [BE_escape]) (Some unit_typ) in
             texp :: check_block l env exps typ
+         | ((E_aux (E_if (cond, (E_aux (E_throw _, _) | E_aux (E_block [E_aux (E_throw _, _)], _)), _), _) as exp) :: exps) ->
+            let texp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in
+            let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in
+            let env = add_opt_constraint (option_map nc_negate (assert_constraint env false cond')) env in
+            texp :: check_block l env exps typ
          | (exp :: exps) ->
             let texp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in
             texp :: check_block l env exps typ
@@ -3400,13 +3405,6 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
            let iuargs = List.map2 (fun utyp (n, uarg) -> (n, crule check_exp env uarg utyp)) utyps uargs in
            (iuargs, ret_typ, env)
          else typ_raise l (Err_unresolved_quants (f, quants, Env.get_locals env, Env.get_constraints env))
-(*
-           typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants
-                           ^ " not resolved during application of " ^ string_of_id f
-                           ^ " unresolved args: " ^ string_of_list ", " (fun (_, exp) -> string_of_exp exp) uargs
-                           ^ "\nAll constraints: " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)
-                           ^ "\nLocals: " ^ string_of_list ", " (fun (id, (mut, typ)) -> string_of_id id ^ " : " ^ string_of_typ typ) (Bindings.bindings (Env.get_locals env)))
- *)
        end
     | (utyps, (typ :: typs)), (uargs, ((n, arg) :: args))
          when List.for_all (fun kid -> is_bound kid env) (KidSet.elements (typ_frees typ)) ->
diff --git a/src/type_error.ml b/src/type_error.ml
index ada8e16b..a49334ac 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -238,6 +238,24 @@ let rec string_of_type_error err =
   ToBuffer.pretty 1. 400 b (pp_type_error err);
   "\n" ^ Buffer.contents b
 
+let rec collapse_errors = function
+  | (Err_no_overloading (_, (err :: errs)) as no_collapse) ->
+      let err = collapse_errors (snd err) in
+      let errs = List.map (fun (_, err) -> collapse_errors err) errs in
+      let fold_equal msg err =
+        match msg, err with
+        | Some msg, Err_no_overloading _ -> Some msg
+        | Some msg, Err_other _ -> Some msg
+        | Some msg, Err_no_casts _ -> Some msg
+        | Some msg, err when msg = string_of_type_error err -> Some msg
+        | _, _ -> None
+      in
+      begin match List.fold_left fold_equal (Some (string_of_type_error err)) errs with
+      | Some _ -> err
+      | None -> no_collapse
+      end
+  | err -> err
+
 let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
   fun env defs ->
   try Type_check.check env defs with