From c1305bf912ff1cc0920c2bb011fee30623504a34 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 22 Oct 2018 16:03:41 +0100
Subject: Fix lem arguments for functions with tuple arguments

Make lem output understand difference between functions taking a tuple
and functions taking multiple arguments. Previously it assumed that no
functions ever took a tuple as an argument, which is incorrect for
mappings.
---
 src/pretty_print_lem.ml  | 57 +++++++++++++++++++++++-------------------------
 src/pretty_print_sail.ml |  5 +++--
 2 files changed, 30 insertions(+), 32 deletions(-)

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 8138a04e..68825c8f 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -1228,42 +1228,35 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
             else empty)
     | _ -> raise (Reporting_basic.err_unreachable l __POS__ "register with non-constant indices")
 
-let args_of_typ l env typ =
-  let typs = match typ with
-    | Typ_aux (Typ_tup typs, _) -> typs
-    | typ -> [typ] in
+let args_of_typs l env typs =
   let arg i typ =
     let id = mk_id ("arg" ^ string_of_int i) in
     P_aux (P_id id, (l, mk_tannot env typ no_effect)),
     E_aux (E_id id, (l, mk_tannot env typ no_effect)) in
   List.split (List.mapi arg typs)
 
-let rec untuple_args_pat fun_typ (P_aux (paux, ((l, _) as annot)) as pat) =
+let rec untuple_args_pat (P_aux (paux, ((l, _) as annot)) as pat) arg_typs =
+  let env = env_of_annot annot in
   let identity = (fun body -> body) in
-  let env = env_of_annot annot in 
-  (* Hack until we get proper multiple-argument-patterns *)
-  match fun_typ with
-  | Typ_aux(Typ_fn([_], _, _), _) -> [pat], identity
-  | _ -> begin
-      let (Typ_aux (taux, _)) = typ_of_annot annot in
-      match paux, taux with
-      | P_tup [], _ ->
-         let annot = (l, mk_tannot Env.empty unit_typ no_effect) in
-         [P_aux (P_lit (mk_lit L_unit), annot)], identity
-      | P_tup pats, _ -> pats, identity
-      | P_wild, Typ_tup typs ->
-         let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)) in
-         List.map wild typs, identity
-      | P_typ (_, pat), _ -> untuple_args_pat fun_typ pat
-      | P_as _, Typ_tup _ | P_id _, Typ_tup _ ->
-         let argpats, argexps = args_of_typ l env (pat_typ_of pat) in
-         let argexp = E_aux (E_tuple argexps, annot) in
-         let bindargs (E_aux (_, bannot) as body) =
-           E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in
-         argpats, bindargs
-      | _, _ ->
-         [pat], identity
-    end
+  match paux, arg_typs with
+  | P_tup [], _ ->
+     let annot = (l, mk_tannot Env.empty unit_typ no_effect) in
+     [P_aux (P_lit (mk_lit L_unit), annot)], identity
+  | P_wild, [Typ_aux (Typ_tup typs, _)] ->
+     let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)) in
+     List.map wild typs, identity
+  | P_typ (_, pat), _ -> untuple_args_pat pat arg_typs
+  | P_as _, [Typ_aux (Typ_tup _, _)]
+    | P_id _, [Typ_aux (Typ_tup _, _)]
+    | P_tup _, [Typ_aux (Typ_tup _, _)] ->
+     let argpats, argexps = args_of_typs l env arg_typs in
+     let argexp = E_aux (E_tuple argexps, annot) in
+     let bindargs (E_aux (_, bannot) as body) =
+       E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in
+     argpats, bindargs
+  | P_tup pats, _ -> pats, identity
+  | _, _ ->
+     [pat], identity
 
 let doc_rec_lem force_rec (Rec_aux(r,_)) = match r with
   | Rec_nonrec when not force_rec -> space
@@ -1281,12 +1274,16 @@ let doc_fun_body_lem ctxt exp =
 
 let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let typ = typ_of_annot annot in
+  let arg_typs = match typ with
+    | Typ_aux (Typ_fn (arg_typs, typ_ret, _), _) -> arg_typs
+    | Typ_aux (_, l) -> raise (unreachable l __POS__ "Non-function type for funcl")
+  in
   let pat,guard,exp,(l,_) = destruct_pexp pexp in
   let ctxt =
     { early_ret = contains_early_return exp;
       bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ);
       top_env = env_of_annot annot } in
-  let pats, bind = untuple_args_pat (typ_of_annot annot) pat in
+  let pats, bind = untuple_args_pat pat arg_typs in
   let patspp = separate_map space (doc_pat_lem ctxt true) pats in
   let _ = match guard with
     | None -> ()
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 8f78b7dc..08ede660 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -354,6 +354,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_throw exp -> string "throw" ^^ parens (doc_exp exp)
   | E_try (exp, pexps) ->
      separate space [string "try"; doc_exp exp; string "catch"; doc_pexps pexps]
+  | E_return (E_aux (E_lit (L_aux (L_unit, _)), _)) -> string "return()"
   | E_return exp -> string "return" ^^ parens (doc_exp exp)
   | E_internal_return exp -> string "internal_return" ^^ parens (doc_exp exp)
   | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 ->
@@ -367,8 +368,8 @@ and doc_infix n (E_aux (e_aux, _) as exp) =
          match Bindings.find op !fixities with
          | (Infix, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]
          | (Infix, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r])
-         | (InfixL, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]
-         | (InfixL, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r])
+         | (InfixL, m) when m >= n -> separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r]
+         | (InfixL, m) -> parens (separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r])
          | (InfixR, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]
          | (InfixR, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r])
        with
-- 
cgit v1.2.3


From 16df05e36d126a1a78e02e20d1dd1320e294d050 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 22 Oct 2018 17:35:51 +0100
Subject: Coq: work around constructors with tupled arguments

---
 src/pretty_print_coq.ml |  7 +++++++
 src/rewrites.ml         | 11 ++++++++++-
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 806234d6..99d63b55 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -694,6 +694,13 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
             List.map (subst_unifiers unifiers) arg_typs
          | _ -> assert false
        in
+       (* Constructors that were specified without a return type might get
+          an extra tuple in their type; expand that here if necessary.
+          TODO: this should go away if we enforce proper arities. *)
+       let arg_typs = match pats, arg_typs with
+         | _::_::_, [Typ_aux (Typ_tup typs,_)] -> typs
+         | _,_ -> arg_typs
+       in
        let ppp = doc_unop (doc_id_ctor id)
          (parens (separate_map comma (doc_pat ctxt true true) (List.combine pats arg_typs))) in
        if apat_needed then parens ppp else ppp
diff --git a/src/rewrites.ml b/src/rewrites.ml
index cdb15717..c470d906 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4595,7 +4595,16 @@ let rec remove_clause_from_pattern ctx (P_aux (rm_pat,ann)) res_pat =
      (match res_pat with
      | RP_app (id',residual_args) ->
         if Id.compare id id' == 0 then
-          let res_pats' = subpats args residual_args in
+          let res_pats' =
+            (* Constructors that were specified without a return type might get
+               an extra tuple in their type; expand that here if necessary.
+               TODO: this should go away if we enforce proper arities. *)
+            match args, residual_args with
+            | [], [RP_any]
+            | _::_::_, [RP_any]
+              -> subpats args (List.map (fun _ -> RP_any) args)
+            | _,_ ->
+               subpats args residual_args in
           List.map (fun rps -> RP_app (id,rps)) res_pats'
         else [res_pat]
      | RP_any ->
-- 
cgit v1.2.3


From 104fd550bd99f2c22655f7d7aa173715054234fd Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 22 Oct 2018 17:36:17 +0100
Subject: Update Coq patch for RISC-V, add string_take to Coq library

---
 lib/coq/Sail2_string.v |  4 +++
 riscv/coq.patch        | 83 +++++++++++++++++++++++++++++++++++++-------------
 2 files changed, 65 insertions(+), 22 deletions(-)

diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index 0a63ff2c..a02556b2 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -11,6 +11,10 @@ Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) :=
   let n := Z.to_nat (projT1 n) in
   String.substring n (String.length s - n) s.
 
+Definition string_take s (n : {n : Z & ArithFact (n >= 0)}) :=
+  let n := Z.to_nat (projT1 n) in
+  String.substring 0 n s.
+
 Definition string_length s : {n : Z & ArithFact (n >= 0)} :=
  build_ex (Z.of_nat (String.length s)).
 
diff --git a/riscv/coq.patch b/riscv/coq.patch
index 2dc1b4aa..d1cf3041 100644
--- a/riscv/coq.patch
+++ b/riscv/coq.patch
@@ -1,6 +1,43 @@
---- riscv.v	2018-10-01 18:21:50.121189040 +0100
-+++ riscv.v.good	2018-10-01 18:21:24.485040512 +0100
-@@ -10537,14 +10537,13 @@
+--- riscv.v.orig	2018-10-22 17:27:20.456069232 +0100
++++ riscv.v	2018-10-22 17:29:35.588974872 +0100
+@@ -1366,7 +1366,7 @@
+ 
+ Definition ex_nat (n : ({n : Z & ArithFact (n >= 0)})) 
+ : {syn_n : Z & ArithFact (syn_n >= 0)} :=
+-   build_ex(n).
++   (n).
+ 
+ Definition ex_int (n : (Z))  : {syn_n : Z & ArithFact (True)} := build_ex(n).
+ 
+@@ -1441,6 +1441,9 @@
+    let v64 : bits 64 := EXTS 64 v in
+    subrange_vec_dec (shift_bits_right v64 shift) 31 0.
+ 
++Definition n_leading_spaces s : {n : Z & ArithFact (n >= 0)} :=
++ build_ex (Z.of_nat (n_leading_spaces s)).
++(*
+ Fixpoint n_leading_spaces (arg0 : string) 
+ : {n : Z & ArithFact (n >= 0)} :=
+    build_ex(let s := (arg0) in
+@@ -1456,7 +1459,7 @@
+                                                                                 (build_ex 1)))))))
+                   : {n : Z & ArithFact (n >= 0)}))))
+      else 0).
+-
++*)
+ Definition spc_forwards '(tt : (unit))  : string := " ".
+ 
+ Definition spc_backwards (arg0 : string) 
+@@ -1470,7 +1473,7 @@
+    let 'n := projT1 (n_leading_spaces s) in
+    let p0_ := n in
+    if sumbool_of_bool ((Z.eqb p0_ 0)) then None
+-   else Some ((tt, n)).
++   else Some ((tt, build_ex n)).
+ 
+ Definition opt_spc_forwards '(tt : (unit))  : string := "".
+ 
+@@ -11079,14 +11082,13 @@
     returnm ((EXTZ 56 (shiftl (_get_Satp64_PPN satp64) PAGESIZE_BITS))
      : mword 56).
  
@@ -17,7 +54,7 @@
               (projT1 (sub_range (build_ex SV39_LEVEL_BITS) (build_ex 1))) 0)) PTE39_LOG_SIZE in
     let pte_addr := add_vec ptb pt_ofs in
     (phys_mem_read Data (EXTZ 64 pte_addr) 8 false false false) >>= fun w__0 : MemoryOpResult (mword (8 * 8)) =>
-@@ -10557,27 +10556,27 @@
+@@ -11099,27 +11101,27 @@
         let is_global := orb global (eq_vec (_get_PTE_Bits_G pattr) ((bool_to_bits true)  : mword 1)) in
         (if ((isInvalidPTE pbits)) then returnm ((PTW_Failure (PTW_Invalid_PTE))  : PTW_Result )
          else if ((isPTEPtr pbits)) then
@@ -51,7 +88,7 @@
                        if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask)
                               (EXTZ 44 (vec_of_bits [B0]  : mword 1)))) then
                          PTW_Failure
-@@ -10587,10 +10586,10 @@
+@@ -11129,10 +11131,10 @@
                            or_vec (_get_SV39_PTE_PPNi pte)
                              (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in
                          PTW_Success
@@ -64,7 +101,7 @@
             : PTW_Result))
          : M (PTW_Result)
      end)
-@@ -10716,7 +10715,7 @@
+@@ -11258,7 +11260,7 @@
          : M (TR39_Result)
      | None =>
         (curPTB39 tt) >>= fun w__6 : mword 56 =>
@@ -73,12 +110,13 @@
         (match w__7 with
          | PTW_Failure (f) => returnm ((TR39_Failure (f))  : TR39_Result )
          | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) =>
-@@ -15425,137 +15424,143 @@
+@@ -15511,138 +15513,145 @@
     returnm (true
      : bool).
  
--Fixpoint execute (merge_var : ast) 
+-Fixpoint execute (arg0 : ast) 
 -: M (bool) :=
+-   let merge_var := (arg0) in
 -   match merge_var with
 +Definition expand_ast (i : ast) : ast :=
 +match i with
@@ -270,36 +308,37 @@
 +| i => i
 +end.
 +
-+Fixpoint execute (merge_var : ast) 
++Fixpoint execute (arg0 : ast) 
 +: M (bool) :=
++   let merge_var := (arg0) in
 +let merge_var := expand_ast merge_var in
 +   match merge_var with
++
     | UTYPE (imm,rd,op) => (execute_UTYPE imm rd op)  : M (bool)
     | RISCV_JAL (imm,rd) => (execute_RISCV_JAL imm rd)  : M (bool)
     | RISCV_JALR (imm,rs1,rd) => (execute_RISCV_JALR imm rs1 rd)  : M (bool)
-@@ -15595,6 +15600,7 @@
+@@ -15682,6 +15691,7 @@
     | THREAD_START (arg0) => returnm ((execute_THREAD_START arg0)  : bool)
     | ILLEGAL (s) => (execute_ILLEGAL s)  : M (bool)
-    | C_ILLEGAL (arg0) => (execute_C_ILLEGAL arg0)  : M (bool)
+    | C_ILLEGAL (s) => (execute_C_ILLEGAL s)  : M (bool)
 +| _ => Fail "Unexpanded instruction"
     end.
  
- Definition assembly_forwards (arg_ : ast) 
-@@ -27093,7 +27099,7 @@
-     else returnm (tt  : unit)) >>
+ Definition assembly_forwards (arg0 : ast) 
+@@ -36869,6 +36879,7 @@
     returnm (stepped
      : bool).
--
+ 
 +(*
- Definition loop '(tt : unit) 
+ Definition loop '(tt : (unit)) 
  : M (unit) :=
     let insns_per_tick := plat_insns_per_tick tt in
-@@ -27135,7 +27141,7 @@
+@@ -36909,7 +36920,7 @@
+            : M (Z)) >>= fun i : Z =>
         returnm (i, step_no))) >>= fun '(i, step_no) =>
     returnm (tt
-     : unit).
--
-+*)
- Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} 
+-    : unit).
++    : unit).*)
+ 
+ Definition read_kind_of_num (arg0 : Z) `{ArithFact (0 <= arg0 /\ arg0 <= 11)} 
  : read_kind :=
-    let p0_ := arg_ in
-- 
cgit v1.2.3


From e489f2d37efa4c320004d35c3025c77e0a0c60d0 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 22 Oct 2018 18:29:18 +0100
Subject: Coq: use function type more carefully in untupling And update the
 RISC-V patch accordingly.

---
 riscv/coq.patch         | 66 +++++++++++++++++++++----------------------------
 src/pretty_print_coq.ml | 29 +++++++++++-----------
 2 files changed, 42 insertions(+), 53 deletions(-)

diff --git a/riscv/coq.patch b/riscv/coq.patch
index d1cf3041..6c40e6e2 100644
--- a/riscv/coq.patch
+++ b/riscv/coq.patch
@@ -1,43 +1,34 @@
---- riscv.v.orig	2018-10-22 17:27:20.456069232 +0100
-+++ riscv.v	2018-10-22 17:29:35.588974872 +0100
-@@ -1366,7 +1366,7 @@
- 
- Definition ex_nat (n : ({n : Z & ArithFact (n >= 0)})) 
- : {syn_n : Z & ArithFact (syn_n >= 0)} :=
--   build_ex(n).
-+   (n).
- 
- Definition ex_int (n : (Z))  : {syn_n : Z & ArithFact (True)} := build_ex(n).
- 
-@@ -1441,6 +1441,9 @@
+--- riscv.v	2018-10-22 18:20:01.512785981 +0100
++++ riscv.v.good	2018-10-22 18:19:27.556562080 +0100
+@@ -1260,6 +1260,9 @@
     let v64 : bits 64 := EXTS 64 v in
     subrange_vec_dec (shift_bits_right v64 shift) 31 0.
  
 +Definition n_leading_spaces s : {n : Z & ArithFact (n >= 0)} :=
 + build_ex (Z.of_nat (n_leading_spaces s)).
 +(*
- Fixpoint n_leading_spaces (arg0 : string) 
+ Fixpoint n_leading_spaces (s : string) 
  : {n : Z & ArithFact (n >= 0)} :=
-    build_ex(let s := (arg0) in
-@@ -1456,7 +1459,7 @@
+    build_ex(let p0_ := s in
+@@ -1273,7 +1276,7 @@
+                                                                              (string_drop s
                                                                                  (build_ex 1)))))))
                    : {n : Z & ArithFact (n >= 0)}))))
-      else 0).
--
-+*)
- Definition spc_forwards '(tt : (unit))  : string := " ".
+-     else 0).
++     else 0).*)
  
- Definition spc_backwards (arg0 : string) 
-@@ -1470,7 +1473,7 @@
+ Definition spc_forwards '(tt : unit)  : string := " ".
+ 
+@@ -1284,7 +1287,7 @@
     let 'n := projT1 (n_leading_spaces s) in
     let p0_ := n in
     if sumbool_of_bool ((Z.eqb p0_ 0)) then None
 -   else Some ((tt, n)).
 +   else Some ((tt, build_ex n)).
  
- Definition opt_spc_forwards '(tt : (unit))  : string := "".
+ Definition opt_spc_forwards '(tt : unit)  : string := "".
  
-@@ -11079,14 +11082,13 @@
+@@ -10432,14 +10435,13 @@
     returnm ((EXTZ 56 (shiftl (_get_Satp64_PPN satp64) PAGESIZE_BITS))
      : mword 56).
  
@@ -54,7 +45,7 @@
               (projT1 (sub_range (build_ex SV39_LEVEL_BITS) (build_ex 1))) 0)) PTE39_LOG_SIZE in
     let pte_addr := add_vec ptb pt_ofs in
     (phys_mem_read Data (EXTZ 64 pte_addr) 8 false false false) >>= fun w__0 : MemoryOpResult (mword (8 * 8)) =>
-@@ -11099,27 +11101,27 @@
+@@ -10452,27 +10454,27 @@
         let is_global := orb global (eq_vec (_get_PTE_Bits_G pattr) ((bool_to_bits true)  : mword 1)) in
         (if ((isInvalidPTE pbits)) then returnm ((PTW_Failure (PTW_Invalid_PTE))  : PTW_Result )
          else if ((isPTEPtr pbits)) then
@@ -88,7 +79,7 @@
                        if ((neq_vec (and_vec (_get_SV39_PTE_PPNi pte) mask)
                               (EXTZ 44 (vec_of_bits [B0]  : mword 1)))) then
                          PTW_Failure
-@@ -11129,10 +11131,10 @@
+@@ -10482,10 +10484,10 @@
                            or_vec (_get_SV39_PTE_PPNi pte)
                              (and_vec (EXTZ 44 (_get_SV39_Vaddr_VPNi va)) mask) in
                          PTW_Success
@@ -101,7 +92,7 @@
             : PTW_Result))
          : M (PTW_Result)
      end)
-@@ -11258,7 +11260,7 @@
+@@ -10611,7 +10613,7 @@
          : M (TR39_Result)
      | None =>
         (curPTB39 tt) >>= fun w__6 : mword 56 =>
@@ -110,13 +101,12 @@
         (match w__7 with
          | PTW_Failure (f) => returnm ((TR39_Failure (f))  : TR39_Result )
          | PTW_Success (pAddr,pte,pteAddr,(existT _ level _),global) =>
-@@ -15511,138 +15513,145 @@
+@@ -14651,137 +14653,144 @@
     returnm (true
      : bool).
  
--Fixpoint execute (arg0 : ast) 
+-Fixpoint execute (merge_var : ast) 
 -: M (bool) :=
--   let merge_var := (arg0) in
 -   match merge_var with
 +Definition expand_ast (i : ast) : ast :=
 +match i with
@@ -308,37 +298,37 @@
 +| i => i
 +end.
 +
-+Fixpoint execute (arg0 : ast) 
++Fixpoint execute (merge_var : ast) 
 +: M (bool) :=
-+   let merge_var := (arg0) in
 +let merge_var := expand_ast merge_var in
 +   match merge_var with
 +
     | UTYPE (imm,rd,op) => (execute_UTYPE imm rd op)  : M (bool)
     | RISCV_JAL (imm,rd) => (execute_RISCV_JAL imm rd)  : M (bool)
     | RISCV_JALR (imm,rs1,rd) => (execute_RISCV_JALR imm rs1 rd)  : M (bool)
-@@ -15682,6 +15691,7 @@
+@@ -14821,6 +14830,7 @@
     | THREAD_START (arg0) => returnm ((execute_THREAD_START arg0)  : bool)
     | ILLEGAL (s) => (execute_ILLEGAL s)  : M (bool)
     | C_ILLEGAL (s) => (execute_C_ILLEGAL s)  : M (bool)
 +| _ => Fail "Unexpanded instruction"
     end.
  
- Definition assembly_forwards (arg0 : ast) 
-@@ -36869,6 +36879,7 @@
+ Definition assembly_forwards (arg_ : ast) 
+@@ -35792,7 +35802,7 @@
     returnm (stepped
      : bool).
  
-+(*
- Definition loop '(tt : (unit)) 
+-Definition loop '(tt : unit) 
++(*Definition loop '(tt : unit) 
  : M (unit) :=
     let insns_per_tick := plat_insns_per_tick tt in
-@@ -36909,7 +36920,7 @@
+    let i : Z := 0 in
+@@ -35832,7 +35842,7 @@
             : M (Z)) >>= fun i : Z =>
         returnm (i, step_no))) >>= fun '(i, step_no) =>
     returnm (tt
 -    : unit).
 +    : unit).*)
  
- Definition read_kind_of_num (arg0 : Z) `{ArithFact (0 <= arg0 /\ arg0 <= 11)} 
+ Definition read_kind_of_num (arg_ : Z) `{ArithFact (0 <= arg_ /\ arg_ <= 11)} 
  : read_kind :=
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 99d63b55..f1726ce4 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1768,33 +1768,28 @@ let args_of_typ l env typs =
     E_aux (E_id id, (l, mk_tannot env typ no_effect)) in
   List.split (List.mapi arg typs)
 
-let rec untuple_args_pat typ (P_aux (paux, ((l, _) as annot)) as pat) =
+let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) =
   let env = env_of_annot annot in
-  let tup_typs = match typ with
-    | Typ_aux (Typ_tup typs, _) -> Some typs
-    | _ -> match Env.expand_synonyms env typ with
-      | Typ_aux (Typ_tup typs, _) -> Some typs
-      | _ -> None
-  in
   let identity = (fun body -> body) in
-  match paux, tup_typs with
+  match paux, typs with
   | P_tup [], _ ->
      let annot = (l, mk_tannot Env.empty unit_typ no_effect) in
      [P_aux (P_lit (mk_lit L_unit), annot), unit_typ], identity
-  | P_tup pats, Some typs -> List.combine pats typs, identity
-  | P_tup pats, _ -> raise (Reporting_basic.err_unreachable l __POS__ "Tuple pattern against non-tuple type")
-  | P_wild, Some typs ->
+  | P_tup pats, _ -> List.combine pats typs, identity
+  | P_wild, _ ->
      let wild typ = P_aux (P_wild, (l, mk_tannot env typ no_effect)), typ in
      List.map wild typs, identity
-  | P_typ (_, pat), _ -> untuple_args_pat typ pat
-  | P_as _, Some typs | P_id _, Some typs ->
+  | P_typ (_, pat), _ -> untuple_args_pat typs pat
+  | P_as _, _::_::_ | P_id _, _::_::_ ->
      let argpats, argexps = args_of_typ l env typs in
      let argexp = E_aux (E_tuple argexps, annot) in
      let bindargs (E_aux (_, bannot) as body) =
        E_aux (E_let (LB_aux (LB_val (pat, argexp), annot), body), bannot) in
      argpats, bindargs
-  | _, _ ->
+  | _, [typ] ->
      [pat,typ], identity
+  | _, _ ->
+     unreachable l __POS__ "Unexpected pattern/type combination"
 
 let doc_rec (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> string "Definition"
@@ -1930,7 +1925,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let ids_to_avoid = all_ids pexp in
   let bound_kids = tyvars_of_typquant tq in
   let pat,guard,exp,(l,_) = destruct_pexp pexp in
-  let pats, bind = untuple_args_pat (mk_typ (Typ_tup arg_typs)) pat in (* FIXME is this needed any more? *)
+  let pats, bind = untuple_args_pat arg_typs pat in (* FIXME is this needed any more? *)
   let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in
   let eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in
   let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in
@@ -1957,6 +1952,10 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let doc_binder (P_aux (p,ann) as pat, typ) =
     let env = env_of_annot ann in
     let exp_typ = Env.expand_synonyms env typ in
+    let () =
+      debug ctxt (lazy (" pattern " ^ string_of_pat pat));
+      debug ctxt (lazy (" with expanded type " ^ string_of_typ exp_typ))
+    in
     match p with
     | P_id id
     | P_typ (_,P_aux (P_id id,_))
-- 
cgit v1.2.3


From 2cef8d0c31a09ea4fac9a48faff882dde4e98641 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Mon, 10 Sep 2018 12:16:42 -0700
Subject: RISC-V: Refactor c platform bits.

---
 riscv/Makefile              |  5 +++--
 riscv/riscv_platform.c      | 21 ++++++++++++---------
 riscv/riscv_platform_impl.c | 17 +++++++++++++++++
 riscv/riscv_platform_impl.h | 20 ++++++++++++++++++++
 4 files changed, 52 insertions(+), 11 deletions(-)
 create mode 100644 riscv/riscv_platform_impl.c
 create mode 100644 riscv/riscv_platform_impl.h

diff --git a/riscv/Makefile b/riscv/Makefile
index 80b3ebf7..5b615971 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -4,7 +4,8 @@ SAIL_DIR ?= $(realpath ..)
 SAIL ?= $(SAIL_DIR)/sail
 C_WARNINGS ?=
 #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
-C_SRCS = riscv_prelude.c riscv_platform.c
+C_INCS = riscv_prelude.h riscv_platform_impl.h riscv_platform.h
+C_SRCS = riscv_prelude.c riscv_platform_impl.c riscv_platform.c
 
 export SAIL_DIR
 
@@ -38,7 +39,7 @@ coverage: _sbuild/coverage.native
 riscv.c: $(SAIL_SRCS) main.sail Makefile
 	$(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) main.sail 1> $@
 
-riscv_c: riscv.c riscv_prelude.h $(C_SRCS) Makefile
+riscv_c: riscv.c $(C_INCS) $(C_SRCS) Makefile
 	gcc $(C_WARNINGS) -O2 riscv.c $(C_SRCS) ../lib/*.c -lgmp -lz -I ../lib -o riscv_c
 
 latex: $(SAIL_SRCS) Makefile
diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index 7f6ec470..31ec09c4 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -1,41 +1,44 @@
 #include "sail.h"
 #include "rts.h"
 #include "riscv_prelude.h"
+#include "riscv_platform_impl.h"
+
+/* This file contains the definitions of the C externs of Sail model. */
 
 bool plat_enable_dirty_update(unit u)
-{ return false; }
+{ return rv_enable_dirty_update; }
 
 bool plat_enable_misaligned_access(unit u)
-{ return false; }
+{ return rv_enable_misaligned; }
 
 mach_bits plat_ram_base(unit u)
 {
-  return UINT64_C(0x80000000);
+  return rv_ram_base;
 }
 
 mach_bits plat_ram_size(unit u)
 {
-  return UINT64_C(0x80000000);
+  return rv_rom_base;
 }
 
 mach_bits plat_rom_base(unit u)
 {
-  return UINT64_C(0x1000);
+  return rv_rom_base;
 }
 
 mach_bits plat_rom_size(unit u)
 {
-  return UINT64_C(0x100);
+  return rv_rom_size;
 }
 
 mach_bits plat_clint_base(unit u)
 {
-  return UINT64_C(0x2000000);
+  return rv_clint_base;
 }
 
 mach_bits plat_clint_size(unit u)
 {
-  return UINT64_C(0xc0000);
+  return rv_clint_size;
 }
 
 bool within_phys_mem(mach_bits addr, sail_int len)
@@ -62,7 +65,7 @@ void plat_insns_per_tick(sail_int *rop, unit u)
 
 mach_bits plat_htif_tohost(unit u)
 {
-  return UINT64_C(0x80001000);
+  return rv_htif_tohost;
 }
 
 unit memea(mach_bits len, sail_int n)
diff --git a/riscv/riscv_platform_impl.c b/riscv/riscv_platform_impl.c
new file mode 100644
index 00000000..1a1d42a7
--- /dev/null
+++ b/riscv/riscv_platform_impl.c
@@ -0,0 +1,17 @@
+#include "riscv_platform_impl.h"
+
+/* Settings of the platform implementation, with common defaults. */
+
+bool rv_enable_dirty_update = false;
+bool rv_enable_misaligned   = false;
+
+uint64_t rv_ram_base = UINT64_C(0x80000000);
+uint64_t rv_ram_size = UINT64_C(0x80000000);
+
+uint64_t rv_rom_base = UINT64_C(0x1000);
+uint64_t rv_rom_size = UINT64_C(0x100);
+
+uint64_t rv_clint_base = UINT64_C(0x2000000);
+uint64_t rv_clint_size = UINT64_C(0xc0000);
+
+uint64_t rv_htif_tohost = UINT64_C(0x80001000);
diff --git a/riscv/riscv_platform_impl.h b/riscv/riscv_platform_impl.h
new file mode 100644
index 00000000..baae2749
--- /dev/null
+++ b/riscv/riscv_platform_impl.h
@@ -0,0 +1,20 @@
+#pragma once
+
+#include <stdbool.h>
+#include <stdint.h>
+
+/* Settings of the platform implementation. */
+
+extern bool rv_enable_dirty_update;
+extern bool rv_enable_misaligned;
+
+extern uint64_t rv_ram_base;
+extern uint64_t rv_ram_size;
+
+extern uint64_t rv_rom_base;
+extern uint64_t rv_rom_size;
+
+extern uint64_t rv_clint_base;
+extern uint64_t rv_clint_size;
+
+extern uint64_t rv_htif_tohost;
-- 
cgit v1.2.3


From 03779a58bcf5fa0c413ae28d218faf7630aa056a Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Mon, 10 Sep 2018 18:46:58 -0700
Subject: RTS: allow elf-loader to provide entry info.

---
 lib/elf.c | 13 +++++++------
 lib/elf.h |  4 +++-
 lib/rts.c |  2 +-
 3 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/lib/elf.c b/lib/elf.c
index 8c5c5f56..e1eae1b7 100644
--- a/lib/elf.c
+++ b/lib/elf.c
@@ -306,7 +306,7 @@ void loadProgHdr64(bool le, const char* buffer, Elf64_Off off, const int total_f
     }
 }
 
-void loadELFHdr(const char* buffer, const int total_file_size) {
+void loadELFHdr(const char* buffer, const int total_file_size, bool *is32bit_p, uint64_t *entry) {
     if (total_file_size < sizeof(Elf32_Ehdr)) {
         fprintf(stderr, "File too small, not big enough even for 32-bit ELF header\n");
         exit(EXIT_FAILURE);
@@ -333,7 +333,8 @@ void loadELFHdr(const char* buffer, const int total_file_size) {
 	for(int i = 0; i < rdHalf32(le, ehdr->e_phnum); ++i) {
 	  loadProgHdr32(le, buffer, rdOff32(le, ehdr->e_phoff) + i * rdHalf32(le, ehdr->e_phentsize), total_file_size);
 	}
-
+        if (is32bit_p) *is32bit_p = true;
+        if (entry) *entry = (uint64_t) ehdr->e_entry;
 	return;
     } else if (hdr->e_ident[EI_CLASS] == ELFCLASS64) {
         if (total_file_size < sizeof(Elf64_Ehdr)) {
@@ -352,7 +353,8 @@ void loadELFHdr(const char* buffer, const int total_file_size) {
 	for(int i = 0; i < rdHalf64(le, ehdr->e_phnum); ++i) {
 	  loadProgHdr64(le, buffer, rdOff64(le, ehdr->e_phoff) + i * rdHalf64(le, ehdr->e_phentsize), total_file_size);
 	}
-
+        if (is32bit_p) *is32bit_p = false;
+        if (entry) *entry = ehdr->e_entry;
 	return;
     } else {
         fprintf(stderr, "Unrecognized ELF file format\n");
@@ -360,7 +362,7 @@ void loadELFHdr(const char* buffer, const int total_file_size) {
     }
 }
 
-void load_elf(char *filename) {
+void load_elf(char *filename, bool *is32bit_p, uint64_t *entry) {
     // Read input file into memory
     char* buffer = NULL;
     int   size   = 0;
@@ -377,8 +379,7 @@ void load_elf(char *filename) {
         if (s < 0) { goto fail; }
         read += s;
     }
-
-    loadELFHdr(buffer, read);
+    loadELFHdr(buffer, read, is32bit_p, entry);
     free(buffer);
     return;
 
diff --git a/lib/elf.h b/lib/elf.h
index e5f90365..8ce99dbb 100644
--- a/lib/elf.h
+++ b/lib/elf.h
@@ -1,5 +1,7 @@
 #pragma once
 
 #include<string.h>
+#include<stdbool.h>
+#include<stdint.h>
 
-void load_elf(char *filename);
+void load_elf(char *filename, bool *is32bit_p, uint64_t *entry);
diff --git a/lib/rts.c b/lib/rts.c
index 1be10137..6bd97934 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -520,7 +520,7 @@ int process_arguments(int argc, char *argv[])
       break;
 
     case 'e':
-      load_elf(optarg);
+      load_elf(optarg, NULL, NULL);
       break;
 
     case 'n':
-- 
cgit v1.2.3


From a6842cd2393827a3d3263079313c988b2ce116df Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Mon, 10 Sep 2018 18:51:19 -0700
Subject: RISC-V: An initial C Sail model linked against Spike for testing.

---
 riscv/Makefile     |  12 +++++
 riscv/riscv_sail.h |  18 +++++++
 riscv/riscv_sim.c  | 152 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 182 insertions(+)
 create mode 100644 riscv/riscv_sail.h
 create mode 100644 riscv/riscv_sim.c

diff --git a/riscv/Makefile b/riscv/Makefile
index 5b615971..88c46823 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -7,6 +7,12 @@ C_WARNINGS ?=
 C_INCS = riscv_prelude.h riscv_platform_impl.h riscv_platform.h
 C_SRCS = riscv_prelude.c riscv_platform_impl.c riscv_platform.c
 
+TV_SPIKE_DIR = /home/mundkur/src/hw/l3/l3riscv
+C_FLAGS = -I $(TV_SPIKE_DIR)/src/cpp -I ../lib
+C_LIBS  = -L $(TV_SPIKE_DIR) -ltv_spike -Wl,-rpath=$(TV_SPIKE_DIR)
+C_LIBS += -L $(RISCV)/lib -lfesvr -lriscv -Wl,-rpath=$(RISCV)/lib
+C_LIBS += -lgmp -lz
+
 export SAIL_DIR
 
 all: platform Riscv.thy
@@ -42,6 +48,12 @@ riscv.c: $(SAIL_SRCS) main.sail Makefile
 riscv_c: riscv.c $(C_INCS) $(C_SRCS) Makefile
 	gcc $(C_WARNINGS) -O2 riscv.c $(C_SRCS) ../lib/*.c -lgmp -lz -I ../lib -o riscv_c
 
+riscv_model.c: $(SAIL_SRCS) main.sail Makefile
+	$(SAIL) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) main.sail 1> $@
+
+riscv_sim: riscv_model.c riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile
+	gcc -g $(C_WARNINGS) $(C_FLAGS) -O2 riscv_model.c riscv_sim.c $(C_SRCS) ../lib/*.c $(C_LIBS) -o $@
+
 latex: $(SAIL_SRCS) Makefile
 	$(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS)
 
diff --git a/riscv/riscv_sail.h b/riscv/riscv_sail.h
new file mode 100644
index 00000000..b89a448a
--- /dev/null
+++ b/riscv/riscv_sail.h
@@ -0,0 +1,18 @@
+/* Top-level entry points into the Sail model. */
+
+typedef int unit;
+#define UNIT 0
+typedef uint64_t mach_bits;
+
+unit zinit_platform(unit);
+unit zinit_sys(unit);
+bool zstep(sail_int);
+
+void model_init(void);
+void model_fini(void);
+
+extern bool zhtif_done;
+extern mach_bits zhtif_exit_code;
+extern bool have_exception;
+extern mach_bits zPC;
+extern mach_bits zminstret;
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
new file mode 100644
index 00000000..e2062053
--- /dev/null
+++ b/riscv/riscv_sim.c
@@ -0,0 +1,152 @@
+#include <getopt.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+#include "elf.h"
+#include "sail.h"
+#include "rts.h"
+#include "riscv_platform.h"
+#include "riscv_platform_impl.h"
+#include "riscv_sail.h"
+#include "tv_spike_intf.h"
+
+struct tv_spike_t *s = NULL;
+
+static bool do_dump_dts = false;
+
+static struct option options[] = {
+  {"enable-dirty",      no_argument,       0, 'd'},
+  {"enable-misaligned", no_argument,       0, 'm'},
+  {"dump-dts",          no_argument,       0, 's'},
+  {"verbosity",         required_argument, 0, 'v'},
+  {"help",              no_argument,       0, 'h'},
+  {0, 0, 0, 0}
+};
+
+static void print_usage(const char *argv0, int ec)
+{
+  fprintf(stdout, "Usage: %s [options] <elf_file>\n", argv0);
+  struct option *opt = options;
+  while (opt->name) {
+    fprintf(stdout, "\t -%c\t %s\n", (char)opt->val, opt->name);
+    opt++;
+  }
+  exit(ec);
+}
+
+char *process_args(int argc, char **argv)
+{
+  int c, idx = 1;
+  while(true) {
+    c = getopt_long(argc, argv, "dmsv:h", options, &idx);
+    if (c == -1) break;
+    switch (c) {
+    case 'd':
+      rv_enable_dirty_update = true;
+      break;
+    case 'm':
+      rv_enable_misaligned = true;
+      break;
+    case 's':
+      do_dump_dts = true;
+      break;
+    case 'h':
+      print_usage(argv[0], 0);
+      break;
+    default:
+      fprintf(stderr, "Unrecognized optchar %c\n", c);
+      print_usage(argv[0], 1);
+    }
+  }
+
+  if (idx >= argc) print_usage(argv[0], 0);
+  return argv[idx];
+}
+
+uint64_t load_sail(char *f)
+{
+  bool is32bit;
+  uint64_t entry;
+  load_elf(f, &is32bit, &entry);
+  if (is32bit) {
+    fprintf(stderr, "32-bit RISC-V not yet supported.\n");
+    exit(1);
+  }
+  fprintf(stdout, "ELF Entry @ %lx\n", entry);
+  return entry;
+}
+
+/* for now, override the reset-vector using the elf entry */
+void init_spike(const char *f, uint64_t entry)
+{
+  s = tv_init("RV64IMAFDC");
+  tv_set_verbose(s, 1);
+  tv_load_elf(s, f);
+  tv_reset(s);
+  tv_set_pc(s, entry);
+}
+
+void init_sail(uint64_t entry)
+{
+  model_init();
+  zinit_platform(UNIT);
+  zinit_sys(UNIT);
+  zPC = entry;
+}
+
+void run_sail(void)
+{
+  bool spike_done;
+  bool stepped;
+  /* initialize the step number */
+  mach_int step_no = 0;
+
+  while (!zhtif_done) {
+    { /* run a Sail step */
+      sail_int sail_step;
+      CREATE(sail_int)(&sail_step);
+      CONVERT_OF(sail_int, mach_int)(&sail_step, step_no);
+      stepped = zstep(sail_step);
+      if (have_exception) goto step_exception;
+    }
+    if (stepped) step_no++;
+
+    { /* run a Spike step */
+      tv_step(s);
+      spike_done = tv_is_done(s);
+    }
+
+    if (zhtif_done) {
+      if (!spike_done) {
+        fprintf(stdout, "Sail done (exit-code %ld), but not Spike!\n", zhtif_exit_code);
+        exit(1);
+      }
+      /* check exit code */
+      if (zhtif_exit_code == 0)
+        fprintf(stdout, "SUCCESS\n");
+      else
+        fprintf(stdout, "FAILURE: %ld\n", zhtif_exit_code);
+    } else {
+      if (spike_done) {
+        fprintf(stdout, "Spike done, but not Sail!\n");
+        exit(1);
+      }
+      /* TODO: update time */
+    }
+  }
+
+ step_exception:
+  model_fini();
+  tv_free(s);
+}
+
+int main(int argc, char **argv)
+{
+  char *file = process_args(argc, argv);
+  uint64_t entry = load_sail(file);
+
+  init_sail(entry);
+  init_spike(file, entry);
+
+  run_sail();
+}
-- 
cgit v1.2.3


From 7fb28eb35fc7ccca80fcc69c6f727e6d9f383ad1 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Wed, 12 Sep 2018 16:19:26 -0700
Subject: RISC-V: Flesh out more of the tandem checks in the C platform
 simulator.

---
 riscv/riscv_sail.h |  31 +++++++++++++--
 riscv/riscv_sim.c  | 110 +++++++++++++++++++++++++++++++++++++++++++++++++++--
 2 files changed, 134 insertions(+), 7 deletions(-)

diff --git a/riscv/riscv_sail.h b/riscv/riscv_sail.h
index b89a448a..596a8263 100644
--- a/riscv/riscv_sail.h
+++ b/riscv/riscv_sail.h
@@ -1,18 +1,41 @@
-/* Top-level entry points into the Sail model. */
+/* Top-level interfaces to the Sail model.
+   Ideally, this would be autogenerated.
+ */
 
 typedef int unit;
 #define UNIT 0
 typedef uint64_t mach_bits;
 
+void model_init(void);
+void model_fini(void);
+
 unit zinit_platform(unit);
 unit zinit_sys(unit);
 bool zstep(sail_int);
 
-void model_init(void);
-void model_fini(void);
-
 extern bool zhtif_done;
 extern mach_bits zhtif_exit_code;
 extern bool have_exception;
+
+/* machine state */
+
+extern uint32_t zcur_privilege;
+
 extern mach_bits zPC;
+
+extern mach_bits
+        zx1,  zx2,  zx3,  zx4,  zx5,  zx6,  zx7,
+  zx8,  zx9,  zx10, zx11, zx12, zx13, zx14, zx15,
+  zx16, zx17, zx18, zx19, zx20, zx21, zx22, zx23,
+  zx24, zx25, zx26, zx27, zx28, zx29, zx30, zx31;
+
+extern mach_bits zmepc, zmtval;
+extern mach_bits zsepc, zstval;
+
+struct zMcause {mach_bits zMcause_chunk_0;};
+struct zMcause zmcause, zscause;
+
 extern mach_bits zminstret;
+
+struct zMisa {mach_bits zMisa_chunk_0;};
+struct zMisa zmisa;
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index e2062053..c11e6268 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -10,6 +10,23 @@
 #include "riscv_sail.h"
 #include "tv_spike_intf.h"
 
+/* Selected CSRs from riscv-isa-sim/riscv/encoding.h */
+#define CSR_STVEC 0x105
+#define CSR_SEPC 0x141
+#define CSR_SCAUSE 0x142
+#define CSR_STVAL 0x143
+
+#define CSR_MSTATUS 0x300
+#define CSR_MISA 0x301
+#define CSR_MEDELEG 0x302
+#define CSR_MIDELEG 0x303
+#define CSR_MIE 0x304
+#define CSR_MTVEC 0x305
+#define CSR_MEPC 0x341
+#define CSR_MCAUSE 0x342
+#define CSR_MTVAL 0x343
+#define CSR_MIP 0x344
+
 struct tv_spike_t *s = NULL;
 
 static bool do_dump_dts = false;
@@ -79,7 +96,7 @@ uint64_t load_sail(char *f)
 /* for now, override the reset-vector using the elf entry */
 void init_spike(const char *f, uint64_t entry)
 {
-  s = tv_init("RV64IMAFDC");
+  s = tv_init("RV64IMAC");
   tv_set_verbose(s, 1);
   tv_load_elf(s, f);
   tv_reset(s);
@@ -94,10 +111,83 @@ void init_sail(uint64_t entry)
   zPC = entry;
 }
 
+int init_check(struct tv_spike_t *s)
+{
+  int passed = 1;
+  passed &= tv_check_csr(s, CSR_MISA, zmisa.zMisa_chunk_0);
+  return passed;
+}
+
+void finish(int ec)
+{
+  model_fini();
+  tv_free(s);
+  exit(ec);
+}
+
+int compare_states(struct tv_spike_t *s)
+{
+  int passed = 1;
+
+  // fix default C enum map for cur_privilege
+  uint8_t priv = (zcur_privilege == 2) ? 3 : zcur_privilege;
+  passed &= tv_check_priv(s, priv);
+
+  passed &= tv_check_pc(s, zPC);
+
+  passed &= tv_check_gpr(s, 1, zx1);
+  passed &= tv_check_gpr(s, 2, zx2);
+  passed &= tv_check_gpr(s, 3, zx3);
+  passed &= tv_check_gpr(s, 4, zx4);
+  passed &= tv_check_gpr(s, 5, zx5);
+  passed &= tv_check_gpr(s, 6, zx6);
+  passed &= tv_check_gpr(s, 7, zx7);
+  passed &= tv_check_gpr(s, 8, zx8);
+  passed &= tv_check_gpr(s, 9, zx9);
+  passed &= tv_check_gpr(s, 10, zx10);
+  passed &= tv_check_gpr(s, 11, zx11);
+  passed &= tv_check_gpr(s, 12, zx12);
+  passed &= tv_check_gpr(s, 13, zx13);
+  passed &= tv_check_gpr(s, 14, zx14);
+  passed &= tv_check_gpr(s, 15, zx15);
+  passed &= tv_check_gpr(s, 15, zx15);
+  passed &= tv_check_gpr(s, 16, zx16);
+  passed &= tv_check_gpr(s, 17, zx17);
+  passed &= tv_check_gpr(s, 18, zx18);
+  passed &= tv_check_gpr(s, 19, zx19);
+  passed &= tv_check_gpr(s, 20, zx20);
+  passed &= tv_check_gpr(s, 21, zx21);
+  passed &= tv_check_gpr(s, 22, zx22);
+  passed &= tv_check_gpr(s, 23, zx23);
+  passed &= tv_check_gpr(s, 24, zx24);
+  passed &= tv_check_gpr(s, 25, zx25);
+  passed &= tv_check_gpr(s, 25, zx25);
+  passed &= tv_check_gpr(s, 26, zx26);
+  passed &= tv_check_gpr(s, 27, zx27);
+  passed &= tv_check_gpr(s, 28, zx28);
+  passed &= tv_check_gpr(s, 29, zx29);
+  passed &= tv_check_gpr(s, 30, zx30);
+  passed &= tv_check_gpr(s, 31, zx31);
+
+  /* some selected CSRs for now */
+
+  passed &= tv_check_csr(s, CSR_MCAUSE, zmcause.zMcause_chunk_0);
+  passed &= tv_check_csr(s, CSR_MEPC, zmepc);
+  passed &= tv_check_csr(s, CSR_MTVAL, zmtval);
+
+  passed &= tv_check_csr(s, CSR_SCAUSE, zscause.zMcause_chunk_0);
+  passed &= tv_check_csr(s, CSR_SEPC, zsepc);
+  passed &= tv_check_csr(s, CSR_STVAL, zstval);
+
+  return passed;
+}
+
 void run_sail(void)
 {
   bool spike_done;
   bool stepped;
+  bool diverged = false;
+
   /* initialize the step number */
   mach_int step_no = 0;
 
@@ -131,13 +221,25 @@ void run_sail(void)
         fprintf(stdout, "Spike done, but not Sail!\n");
         exit(1);
       }
+
+      if (!compare_states(s)) {
+        diverged = true;
+        break;
+      }
+
       /* TODO: update time */
     }
   }
 
+ dump_state:
+  if (diverged) {
+    /* TODO */
+  }
+  finish(diverged);
+
  step_exception:
-  model_fini();
-  tv_free(s);
+  fprintf(stdout, "Sail exception!");
+  goto dump_state;
 }
 
 int main(int argc, char **argv)
@@ -148,5 +250,7 @@ int main(int argc, char **argv)
   init_sail(entry);
   init_spike(file, entry);
 
+  if (!init_check(s)) finish(1);
+
   run_sail();
 }
-- 
cgit v1.2.3


From b220094e7f68246cebf528130c3db93081178878 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Mon, 17 Sep 2018 16:28:30 -0700
Subject: RISC-V: flush logs at each step.

---
 riscv/riscv_sim.c | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index c11e6268..982b98f3 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -182,6 +182,14 @@ int compare_states(struct tv_spike_t *s)
   return passed;
 }
 
+void flush_logs(void)
+{
+  fprintf(stderr, "\n");
+  fflush(stderr);
+  fprintf(stdout, "\n");
+  fflush(stdout);
+}
+
 void run_sail(void)
 {
   bool spike_done;
@@ -198,12 +206,14 @@ void run_sail(void)
       CONVERT_OF(sail_int, mach_int)(&sail_step, step_no);
       stepped = zstep(sail_step);
       if (have_exception) goto step_exception;
+      flush_logs();
     }
     if (stepped) step_no++;
 
     { /* run a Spike step */
       tv_step(s);
       spike_done = tv_is_done(s);
+      flush_logs();
     }
 
     if (zhtif_done) {
-- 
cgit v1.2.3


From a665e2160692e509b75966ceb96b8eb3a84a8375 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Tue, 18 Sep 2018 17:17:36 -0700
Subject: RISC-V: Allow Spike linkage to be conditionally enabled.

---
 riscv/Makefile    | 18 +++++++++++++-----
 riscv/riscv_sim.c | 25 +++++++++++++++++++++----
 2 files changed, 34 insertions(+), 9 deletions(-)

diff --git a/riscv/Makefile b/riscv/Makefile
index 88c46823..72abc5da 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -4,14 +4,22 @@ SAIL_DIR ?= $(realpath ..)
 SAIL ?= $(SAIL_DIR)/sail
 C_WARNINGS ?=
 #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
+C_FLAGS = -I ../lib
 C_INCS = riscv_prelude.h riscv_platform_impl.h riscv_platform.h
 C_SRCS = riscv_prelude.c riscv_platform_impl.c riscv_platform.c
 
+ENABLE_SPIKE = 0
 TV_SPIKE_DIR = /home/mundkur/src/hw/l3/l3riscv
-C_FLAGS = -I $(TV_SPIKE_DIR)/src/cpp -I ../lib
-C_LIBS  = -L $(TV_SPIKE_DIR) -ltv_spike -Wl,-rpath=$(TV_SPIKE_DIR)
-C_LIBS += -L $(RISCV)/lib -lfesvr -lriscv -Wl,-rpath=$(RISCV)/lib
-C_LIBS += -lgmp -lz
+SPIKE_FLAGS = -I $(TV_SPIKE_DIR)/src/cpp
+SPIKE_LIBS  = -L $(TV_SPIKE_DIR) -ltv_spike -Wl,-rpath=$(TV_SPIKE_DIR)
+SPIKE_LIBS += -L $(RISCV)/lib -lfesvr -lriscv -Wl,-rpath=$(RISCV)/lib
+
+C_LIBS = -lgmp -lz
+
+ifeq ($(ENABLE_SPIKE),1)
+C_FLAGS += $(SPIKE_FLAGS)
+C_LIBS  += $(SPIKE_LIBS)
+endif
 
 export SAIL_DIR
 
@@ -121,6 +129,6 @@ clean:
 	-rm -f platform_main.native platform coverage.native
 	-rm -f riscv.vo riscv_types.vo riscv_extras.vo riscv.v riscv_types.v
 	-rm -f riscv_duopod.vo riscv_duopod_types.vo riscv_duopod.v riscv_duopod_types.v
-	-rm -f riscv.c
+	-rm -f riscv.c riscv_model.c riscv_sim
 	-Holmake cleanAll
 	ocamlbuild -clean
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index 982b98f3..ea6f7377 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -8,7 +8,12 @@
 #include "riscv_platform.h"
 #include "riscv_platform_impl.h"
 #include "riscv_sail.h"
+
+#ifdef SPIKE
 #include "tv_spike_intf.h"
+#else
+struct tv_spike_t;
+#endif
 
 /* Selected CSRs from riscv-isa-sim/riscv/encoding.h */
 #define CSR_STVEC 0x105
@@ -27,9 +32,8 @@
 #define CSR_MTVAL 0x343
 #define CSR_MIP 0x344
 
-struct tv_spike_t *s = NULL;
-
 static bool do_dump_dts = false;
+struct tv_spike_t *s = NULL;
 
 static struct option options[] = {
   {"enable-dirty",      no_argument,       0, 'd'},
@@ -96,13 +100,18 @@ uint64_t load_sail(char *f)
 /* for now, override the reset-vector using the elf entry */
 void init_spike(const char *f, uint64_t entry)
 {
+#ifdef SPIKE
   s = tv_init("RV64IMAC");
   tv_set_verbose(s, 1);
   tv_load_elf(s, f);
   tv_reset(s);
   tv_set_pc(s, entry);
+#else
+  s = NULL;
+#endif
 }
 
+
 void init_sail(uint64_t entry)
 {
   model_init();
@@ -114,14 +123,18 @@ void init_sail(uint64_t entry)
 int init_check(struct tv_spike_t *s)
 {
   int passed = 1;
+#ifdef SPIKE
   passed &= tv_check_csr(s, CSR_MISA, zmisa.zMisa_chunk_0);
+#endif
   return passed;
 }
 
 void finish(int ec)
 {
   model_fini();
+#ifdef SPIKE
   tv_free(s);
+#endif
   exit(ec);
 }
 
@@ -129,6 +142,7 @@ int compare_states(struct tv_spike_t *s)
 {
   int passed = 1;
 
+#ifdef SPIKE
   // fix default C enum map for cur_privilege
   uint8_t priv = (zcur_privilege == 2) ? 3 : zcur_privilege;
   passed &= tv_check_priv(s, priv);
@@ -178,6 +192,7 @@ int compare_states(struct tv_spike_t *s)
   passed &= tv_check_csr(s, CSR_SCAUSE, zscause.zMcause_chunk_0);
   passed &= tv_check_csr(s, CSR_SEPC, zsepc);
   passed &= tv_check_csr(s, CSR_STVAL, zstval);
+#endif
 
   return passed;
 }
@@ -210,6 +225,7 @@ void run_sail(void)
     }
     if (stepped) step_no++;
 
+#ifdef SPIKE
     { /* run a Spike step */
       tv_step(s);
       spike_done = tv_is_done(s);
@@ -236,9 +252,10 @@ void run_sail(void)
         diverged = true;
         break;
       }
-
-      /* TODO: update time */
     }
+#endif
+
+    /* TODO: update time */
   }
 
  dump_state:
-- 
cgit v1.2.3


From ca6494d94d9f219de8e46062134258f0c9e2245c Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Tue, 18 Sep 2018 17:23:47 -0700
Subject: RISC-V: Add some debug logs for within_phys_mem.

---
 riscv/riscv_platform.c    |  6 ++++++
 riscv/riscv_platform.sail | 25 +++++++++++++++++++------
 2 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index 31ec09c4..be926f6a 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -13,31 +13,37 @@ bool plat_enable_misaligned_access(unit u)
 
 mach_bits plat_ram_base(unit u)
 {
+  fprintf(stderr, "plat_ram_base: -> %0" PRIx64 "\n", rv_ram_base);
   return rv_ram_base;
 }
 
 mach_bits plat_ram_size(unit u)
 {
+  fprintf(stderr, "plat_ram_size: -> %0" PRIx64 "\n", rv_ram_size);
   return rv_rom_base;
 }
 
 mach_bits plat_rom_base(unit u)
 {
+  fprintf(stderr, "plat_rom_base: -> %0" PRIx64 "\n", rv_rom_base);
   return rv_rom_base;
 }
 
 mach_bits plat_rom_size(unit u)
 {
+  fprintf(stderr, "plat_rom_size: -> %0" PRIx64 "\n", rv_rom_size);
   return rv_rom_size;
 }
 
 mach_bits plat_clint_base(unit u)
 {
+  fprintf(stderr, "plat_clint_base: -> %0" PRIx64 "\n", rv_clint_base);
   return rv_clint_base;
 }
 
 mach_bits plat_clint_size(unit u)
 {
+  fprintf(stderr, "plat_clint_size: -> %0" PRIx64 "\n", rv_clint_size);
   return rv_clint_size;
 }
 
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 80f546b8..c4af9c79 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -42,15 +42,28 @@ function phys_mem_segments() =
 
 /* Physical memory map predicates */
 
-function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+function within_phys_mem(addr : xlenbits, width : atom('n)) -> forall 'n. bool = {
+  let ram_base = plat_ram_base ();
+  let rom_base = plat_rom_base ();
+  let ram_size = plat_ram_size ();
+  let rom_size = plat_rom_size ();
+
   /* todo: iterate over segment list */
-  if (  plat_ram_base() <=_u addr
-      & (addr + sizeof('n)) <=_u (plat_ram_base() + plat_ram_size ()))
+  if (  ram_base <=_u addr
+      & (addr + sizeof('n)) <=_u (ram_base + ram_size))
        then true
-  else if (  plat_rom_base() <=_u addr
-           & (addr + sizeof('n)) <=_u (plat_rom_base() + plat_rom_size()))
+  else if (  rom_base <=_u addr
+           & (addr + sizeof('n)) <=_u (rom_base + rom_size))
        then true
-  else false
+  else {
+    print("within_phys_mem: " ^ BitStr(addr) ^ " not within phys-mem:");
+    print("  plat_rom_base: " ^ BitStr(rom_base));
+    print("  plat_rom_size: " ^ BitStr(rom_size));
+    print("  plat_ram_base: " ^ BitStr(ram_base));
+    print("  plat_ram_size: " ^ BitStr(ram_size));
+    false
+  }
+}
 
 function within_clint(addr : xlenbits, width : atom('n)) -> forall 'n. bool =
     plat_clint_base() <=_u addr
-- 
cgit v1.2.3


From 955a82be31f48aab4a8c21f5d4f94c305abf0f3a Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 20 Sep 2018 16:24:47 +0100
Subject: Fix typo in plat_ram_size

---
 riscv/riscv_platform.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index be926f6a..a16f7c88 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -20,7 +20,7 @@ mach_bits plat_ram_base(unit u)
 mach_bits plat_ram_size(unit u)
 {
   fprintf(stderr, "plat_ram_size: -> %0" PRIx64 "\n", rv_ram_size);
-  return rv_rom_base;
+  return rv_ram_size;
 }
 
 mach_bits plat_rom_base(unit u)
-- 
cgit v1.2.3


From 44919f6064e2031014918f786993677696e86629 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Thu, 20 Sep 2018 17:59:04 -0700
Subject: RTS: Add elf symbol lookup support.

---
 lib/elf.c | 185 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++----
 lib/elf.h |   1 +
 2 files changed, 176 insertions(+), 10 deletions(-)

diff --git a/lib/elf.c b/lib/elf.c
index e1eae1b7..4355b44c 100644
--- a/lib/elf.c
+++ b/lib/elf.c
@@ -103,6 +103,7 @@ uint64_t rev64(uint64_t x) {
 #define PT_LOAD         1  /* Loadable segment */
 
 #define SHT_SYMTAB      2  /* Symbol table type */
+#define SHT_STRTAB      3  /* String table type */
 
 /* How to extract and insert information held in the st_info field.  */
 
@@ -306,7 +307,7 @@ void loadProgHdr64(bool le, const char* buffer, Elf64_Off off, const int total_f
     }
 }
 
-void loadELFHdr(const char* buffer, const int total_file_size, bool *is32bit_p, uint64_t *entry) {
+void checkELFHdr(const char* buffer, const int total_file_size) {
     if (total_file_size < sizeof(Elf32_Ehdr)) {
         fprintf(stderr, "File too small, not big enough even for 32-bit ELF header\n");
         exit(EXIT_FAILURE);
@@ -319,7 +320,6 @@ void loadELFHdr(const char* buffer, const int total_file_size, bool *is32bit_p,
         fprintf(stderr, "Invalid ELF magic bytes. Not an ELF file?\n");
         exit(EXIT_FAILURE);
     }
-
     if (hdr->e_ident[EI_CLASS] == ELFCLASS32) {
         bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
         Elf32_Ehdr *ehdr = (Elf32_Ehdr*) &buffer[0];
@@ -329,13 +329,6 @@ void loadELFHdr(const char* buffer, const int total_file_size, bool *is32bit_p,
             fprintf(stderr, "Invalid ELF type or machine for class (32-bit)\n");
             exit(EXIT_FAILURE);
         }
-
-	for(int i = 0; i < rdHalf32(le, ehdr->e_phnum); ++i) {
-	  loadProgHdr32(le, buffer, rdOff32(le, ehdr->e_phoff) + i * rdHalf32(le, ehdr->e_phentsize), total_file_size);
-	}
-        if (is32bit_p) *is32bit_p = true;
-        if (entry) *entry = (uint64_t) ehdr->e_entry;
-	return;
     } else if (hdr->e_ident[EI_CLASS] == ELFCLASS64) {
         if (total_file_size < sizeof(Elf64_Ehdr)) {
             fprintf(stderr, "File too small, specifies 64-bit ELF but not big enough for 64-bit ELF header\n");
@@ -349,13 +342,32 @@ void loadELFHdr(const char* buffer, const int total_file_size, bool *is32bit_p,
             fprintf(stderr, "Invalid ELF type or machine for class (64-bit)\n");
             exit(EXIT_FAILURE);
         }
+    } else {
+        fprintf(stderr, "Unrecognized ELF file format\n");
+        exit(EXIT_FAILURE);
+    }
+}
+
+void loadELFHdr(const char* buffer, const int total_file_size, bool *is32bit_p, uint64_t *entry) {
+    checkELFHdr(buffer, total_file_size);
 
+    Elf32_Ehdr *hdr = (Elf32_Ehdr*) &buffer[0];
+    if (hdr->e_ident[EI_CLASS] == ELFCLASS32) {
+        bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
+        Elf32_Ehdr *ehdr = (Elf32_Ehdr*) &buffer[0];
+	for(int i = 0; i < rdHalf32(le, ehdr->e_phnum); ++i) {
+	  loadProgHdr32(le, buffer, rdOff32(le, ehdr->e_phoff) + i * rdHalf32(le, ehdr->e_phentsize), total_file_size);
+	}
+        if (is32bit_p) *is32bit_p = true;
+        if (entry) *entry = (uint64_t) ehdr->e_entry;
+    } else if (hdr->e_ident[EI_CLASS] == ELFCLASS64) {
+        bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
+        Elf64_Ehdr *ehdr = (Elf64_Ehdr*) &buffer[0];
 	for(int i = 0; i < rdHalf64(le, ehdr->e_phnum); ++i) {
 	  loadProgHdr64(le, buffer, rdOff64(le, ehdr->e_phoff) + i * rdHalf64(le, ehdr->e_phentsize), total_file_size);
 	}
         if (is32bit_p) *is32bit_p = false;
         if (entry) *entry = ehdr->e_entry;
-	return;
     } else {
         fprintf(stderr, "Unrecognized ELF file format\n");
         exit(EXIT_FAILURE);
@@ -388,6 +400,159 @@ fail:
     exit(EXIT_FAILURE);
 }
 
+// symbol lookup for very simple ELF files (single symtab, two strtabs): looks up a
+// single symbol at a time, but avoids retaining memory.
+
+int lookupSymbol(const char *buffer, const int total_file_size, const char *symname, uint64_t *value) {
+    checkELFHdr(buffer, total_file_size);
+    Elf32_Ehdr *hdr = (Elf32_Ehdr*) &buffer[0];
+    if (hdr->e_ident[EI_CLASS] == ELFCLASS32) {
+        bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
+        Elf32_Ehdr *ehdr = (Elf32_Ehdr*) &buffer[0];
+        if (total_file_size < rdOff32(le, ehdr->e_shoff)
+                              + rdHalf32(le, ehdr->e_shnum)*sizeof(Elf32_Shdr)) {
+            fprintf(stderr, "File too small for %d sections from offset %d\n",
+                    rdHalf32(le, ehdr->e_shnum), rdOff32(le, ehdr->e_shoff));
+            exit(EXIT_FAILURE);
+        }
+        if (rdHalf32(le, ehdr->e_shtrndx) >= rdHalf32(le, ehdr->e_shnum)) {
+            fprintf(stderr, "Invalid string section table index %d\n", hdr->e_shtrndx);
+            exit(EXIT_FAILURE);
+        }
+        Elf32_Shdr *shdr = (Elf32_Shdr *)&buffer[ehdr->e_shoff];
+        Elf32_Shdr *shstrtab = (Elf32_Shdr *)&shdr[rdHalf32(le, ehdr->e_shtrndx)];
+        if (total_file_size < rdOff32(le, shstrtab->sh_offset) + rdWord32(le, shstrtab->sh_size)) {
+            fprintf(stderr, "File too small for string section\n");
+            exit(EXIT_FAILURE);
+        }
+        const char *shstrbuf = buffer + rdOff32(le, shstrtab->sh_offset);
+        Elf32_Word strtabidx = 0, symtabidx = 0;
+        for (Elf32_Word i = 0; i < rdHalf32(le, ehdr->e_shnum); i++) {
+            if (rdWord32(le, shdr[i].sh_type) == SHT_SYMTAB) {
+                symtabidx = i;
+            }
+            if (rdWord32(le, shdr[i].sh_type) == SHT_STRTAB) {
+                // skip section name string table
+                if (i != rdHalf32(le, ehdr->e_shtrndx)) {
+                    strtabidx = i;
+                }
+            }
+        }
+        if (!strtabidx || !symtabidx) {
+            fprintf(stderr, "ELF: unable to find string or symbol table\n");
+            return -1;
+        }
+        const char *strtab = buffer + rdOff32(le, shdr[strtabidx].sh_offset);
+        Elf32_Word strtab_size = rdWord32(le, shdr[strtabidx].sh_size);
+        Elf32_Sym *sym_ent = (Elf32_Sym *)(buffer + rdOff32(le, shdr[symtabidx].sh_offset));
+        for (Elf32_Word i = 0; i < rdWord32(le, shdr[symtabidx].sh_size)/sizeof(*sym_ent); i++) {
+            Elf32_Word sidx = rdWord32(le, sym_ent[i].st_name);
+            if (sidx >= strtab_size) {
+                fprintf(stderr, "Symbol name index out of bounds\n");
+                exit(EXIT_FAILURE);
+            }
+            Elf32_Word max_len = strtab_size - sidx;
+            const char *sname = strtab + sidx;
+            if (strnlen(sname, max_len) >= max_len) {
+                fprintf(stderr, "Unterminated symbol name\n");
+                exit(EXIT_FAILURE);
+            }
+            if (!strcmp(sname, symname)) {
+                if (value) *value = (uint64_t) rdAddr32(le, sym_ent[i].st_value);
+                return 0;
+            }
+        }
+        return -1;
+    } else if (hdr->e_ident[EI_CLASS] == ELFCLASS64) {
+        bool le = hdr->e_ident[EI_DATA] == ELFDATA2LSB;
+        Elf64_Ehdr *ehdr = (Elf64_Ehdr*) &buffer[0];
+        if (total_file_size < rdOff64(le, ehdr->e_shoff)
+                              + rdHalf64(le, ehdr->e_shnum)*sizeof(Elf64_Shdr)) {
+            fprintf(stderr, "File too small for %d sections from offset %ld\n",
+                    rdHalf64(le, ehdr->e_shnum), rdOff64(le, ehdr->e_shoff));
+            exit(EXIT_FAILURE);
+        }
+        if (rdHalf64(le, ehdr->e_shtrndx) >= rdHalf64(le, ehdr->e_shnum)) {
+            fprintf(stderr, "Invalid string section table index %d\n", hdr->e_shtrndx);
+            exit(EXIT_FAILURE);
+        }
+        Elf64_Shdr *shdr = (Elf64_Shdr *)&buffer[ehdr->e_shoff];
+        Elf64_Shdr *shstrtab = (Elf64_Shdr *)&shdr[rdHalf64(le, ehdr->e_shtrndx)];
+        if (total_file_size < rdOff64(le, shstrtab->sh_offset) + rdWord64(le, shstrtab->sh_size)) {
+            fprintf(stderr, "File too small for string section\n");
+            exit(EXIT_FAILURE);
+        }
+        const char *shstrbuf = buffer + rdOff64(le, shstrtab->sh_offset);
+        Elf64_Word strtabidx = 0, symtabidx = 0;
+        for (Elf64_Word i = 0; i < rdHalf64(le, ehdr->e_shnum); i++) {
+            if (rdWord64(le, shdr[i].sh_type) == SHT_SYMTAB) {
+                symtabidx = i;
+            }
+            if (rdWord64(le, shdr[i].sh_type) == SHT_STRTAB) {
+                // skip section name string table
+                if (i != rdHalf64(le, ehdr->e_shtrndx)) {
+                    strtabidx = i;
+                }
+            }
+        }
+        if (!strtabidx || !symtabidx) {
+            fprintf(stderr, "ELF: unable to find string or symbol table\n");
+            return -1;
+        }
+        const char *strtab = buffer + rdOff64(le, shdr[strtabidx].sh_offset);
+        Elf64_Xword strtab_size = rdXword64(le, shdr[strtabidx].sh_size);
+        Elf64_Sym *sym_ent = (Elf64_Sym *)(buffer + rdOff64(le, shdr[symtabidx].sh_offset));
+        for (Elf64_Xword i = 0; i < rdXword64(le, shdr[symtabidx].sh_size)/sizeof(*sym_ent); i++) {
+            Elf64_Word sidx = rdWord64(le, sym_ent[i].st_name);
+            if (sidx >= strtab_size) {
+                fprintf(stderr, "Symbol name index out of bounds\n");
+                exit(EXIT_FAILURE);
+            }
+            Elf64_Word max_len = strtab_size - sidx;
+            const char *sname = strtab + sidx;
+            if (strnlen(sname, max_len) >= max_len) {
+                fprintf(stderr, "Unterminated symbol name\n");
+                exit(EXIT_FAILURE);
+            }
+            if (!strcmp(sname, symname)) {
+                if (value) *value = (uint64_t) rdAddr64(le, sym_ent[i].st_value);
+                return 0;
+            }
+        }
+        return -1;
+    } else {
+        fprintf(stderr, "Unrecognized ELF file format\n");
+        exit(EXIT_FAILURE);
+    }
+}
+
+int lookup_sym(const char *filename, const char *symname, uint64_t *value) {
+    // Read input file into memory
+    char* buffer = NULL;
+    int   size   = 0;
+    int   chunk  = (1<<24); // increments output buffer this much
+    int   read   = 0;
+    int   ret    = 0;
+    gzFile in = gzopen(filename, "rb");
+    if (in == NULL) { goto fail; }
+    while (!gzeof(in)) {
+        size = read + chunk;
+        buffer = (char*)realloc(buffer, size);
+        if (buffer == NULL) { goto fail; }
+
+        int s = gzread(in, buffer+read, size - read);
+        if (s < 0) { goto fail; }
+        read += s;
+    }
+    ret = lookupSymbol(buffer, read, symname, value);
+    free(buffer);
+    return ret;
+
+fail:
+    fprintf(stderr, "Unable to read file %s\n", filename);
+    exit(EXIT_FAILURE);
+}
+
 ////////////////////////////////////////////////////////////////
 // ELF Loader
 ////////////////////////////////////////////////////////////////
diff --git a/lib/elf.h b/lib/elf.h
index 8ce99dbb..6f592afd 100644
--- a/lib/elf.h
+++ b/lib/elf.h
@@ -5,3 +5,4 @@
 #include<stdint.h>
 
 void load_elf(char *filename, bool *is32bit_p, uint64_t *entry);
+int  lookup_sym(const char *filename, const char *symname, uint64_t *value);
-- 
cgit v1.2.3


From 92bcc59480b1c70827bad89217cdde6511429632 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Thu, 20 Sep 2018 18:09:14 -0700
Subject: RISC-V: set htif tohost port address using ELF symbol.

---
 riscv/riscv_platform.c | 37 ++++++-------------------------------
 riscv/riscv_sim.c      |  6 ++++++
 2 files changed, 12 insertions(+), 31 deletions(-)

diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index a16f7c88..758bf46f 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -12,47 +12,22 @@ bool plat_enable_misaligned_access(unit u)
 { return rv_enable_misaligned; }
 
 mach_bits plat_ram_base(unit u)
-{
-  fprintf(stderr, "plat_ram_base: -> %0" PRIx64 "\n", rv_ram_base);
-  return rv_ram_base;
-}
+{ return rv_ram_base; }
 
 mach_bits plat_ram_size(unit u)
-{
-  fprintf(stderr, "plat_ram_size: -> %0" PRIx64 "\n", rv_ram_size);
-  return rv_ram_size;
-}
+{ return rv_ram_size; }
 
 mach_bits plat_rom_base(unit u)
-{
-  fprintf(stderr, "plat_rom_base: -> %0" PRIx64 "\n", rv_rom_base);
-  return rv_rom_base;
-}
+{ return rv_rom_base; }
 
 mach_bits plat_rom_size(unit u)
-{
-  fprintf(stderr, "plat_rom_size: -> %0" PRIx64 "\n", rv_rom_size);
-  return rv_rom_size;
-}
+{ return rv_rom_size; }
 
 mach_bits plat_clint_base(unit u)
-{
-  fprintf(stderr, "plat_clint_base: -> %0" PRIx64 "\n", rv_clint_base);
-  return rv_clint_base;
-}
+{ return rv_clint_base; }
 
 mach_bits plat_clint_size(unit u)
-{
-  fprintf(stderr, "plat_clint_size: -> %0" PRIx64 "\n", rv_clint_size);
-  return rv_clint_size;
-}
-
-bool within_phys_mem(mach_bits addr, sail_int len)
-{
-  printf("within_phys_mem\n");
-  exit(EXIT_FAILURE);
-  return 0;
-}
+{ return rv_clint_size; }
 
 unit load_reservation(mach_bits addr)
 { return UNIT; }
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index ea6f7377..024bd71e 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -94,6 +94,12 @@ uint64_t load_sail(char *f)
     exit(1);
   }
   fprintf(stdout, "ELF Entry @ %lx\n", entry);
+  /* locate htif ports */
+  if (lookup_sym(f, "tohost", &rv_htif_tohost) < 0) {
+    fprintf(stderr, "Unable to locate htif tohost port.\n");
+    exit(1);
+  }
+  fprintf(stderr, "tohost located at %0" PRIx64 "\n", rv_htif_tohost);
   return entry;
 }
 
-- 
cgit v1.2.3


From 00408df7ee7c7ffbac836202071521998556589b Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Fri, 28 Sep 2018 10:59:56 -0700
Subject: RISC-V: fix up platform bits for lr/sc.

---
 riscv/riscv_platform.c | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index 758bf46f..fa3b49aa 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -5,6 +5,9 @@
 
 /* This file contains the definitions of the C externs of Sail model. */
 
+static mach_bits reservation = 0;
+static bool reservation_valid = false;
+
 bool plat_enable_dirty_update(unit u)
 { return rv_enable_dirty_update; }
 
@@ -30,13 +33,20 @@ mach_bits plat_clint_size(unit u)
 { return rv_clint_size; }
 
 unit load_reservation(mach_bits addr)
-{ return UNIT; }
+{
+  reservation = addr;
+  reservation_valid = true;
+  return UNIT;
+}
 
 bool match_reservation(mach_bits addr)
-{ return false; }
+{ return reservation_valid && reservation == addr; }
 
 unit cancel_reservation(unit u)
-{ return UNIT; }
+{
+  reservation_valid = false;
+  return UNIT;
+}
 
 unit plat_term_write(mach_bits c)
 { return UNIT; }
-- 
cgit v1.2.3


From a23fb23f91922152104852e92c672588a4bfa977 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Fri, 28 Sep 2018 16:39:58 -0700
Subject: RISC-V: add default reset vector.

---
 riscv/riscv_platform_impl.h |  3 +++
 riscv/riscv_sim.c           | 39 +++++++++++++++++++++++++++++++++++----
 2 files changed, 38 insertions(+), 4 deletions(-)

diff --git a/riscv/riscv_platform_impl.h b/riscv/riscv_platform_impl.h
index baae2749..db5ff639 100644
--- a/riscv/riscv_platform_impl.h
+++ b/riscv/riscv_platform_impl.h
@@ -5,6 +5,9 @@
 
 /* Settings of the platform implementation. */
 
+#define DEFAULT_RSTVEC     0x00001000
+#define SAIL_XLEN          64
+
 extern bool rv_enable_dirty_update;
 extern bool rv_enable_misaligned;
 
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index 024bd71e..9a03245f 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -103,7 +103,6 @@ uint64_t load_sail(char *f)
   return entry;
 }
 
-/* for now, override the reset-vector using the elf entry */
 void init_spike(const char *f, uint64_t entry)
 {
 #ifdef SPIKE
@@ -111,19 +110,51 @@ void init_spike(const char *f, uint64_t entry)
   tv_set_verbose(s, 1);
   tv_load_elf(s, f);
   tv_reset(s);
-  tv_set_pc(s, entry);
 #else
   s = NULL;
 #endif
 }
 
+void init_sail_reset_vector(uint64_t entry)
+{
+#define RST_VEC_SIZE 8
+  uint32_t reset_vec[RST_VEC_SIZE] = {
+    0x297,                                      // auipc  t0,0x0
+    0x28593 + (RST_VEC_SIZE * 4 << 20),         // addi   a1, t0, &dtb
+    0xf1402573,                                 // csrr   a0, mhartid
+    SAIL_XLEN == 32 ?
+      0x0182a283u :                             // lw     t0,24(t0)
+      0x0182b283u,                              // ld     t0,24(t0)
+    0x28067,                                    // jr     t0
+    0,
+    (uint32_t) (entry & 0xffffffff),
+    (uint32_t) (entry >> 32)
+  };
+
+  rv_rom_base = DEFAULT_RSTVEC;
+  uint64_t addr = rv_rom_base;
+  for (int i = 0; i < sizeof(reset_vec); i++)
+    write_mem(addr++, (uint64_t)((char *)reset_vec)[i]);
+  /* TODO: write DTB */
+
+  /* zero-fill to page boundary */
+  const int align = 0x1000;
+  uint64_t rom_end = (addr + align -1)/align + align;
+  for (int i = addr; i < rom_end; i++)
+    write_mem(addr++, 0);
+
+  /* set rom size */
+  rv_rom_size = addr - rv_rom_base;
+  /* boot at reset vector */
+  zPC = rv_rom_base;
+}
 
-void init_sail(uint64_t entry)
+void init_sail(uint64_t elf_entry)
 {
   model_init();
   zinit_platform(UNIT);
   zinit_sys(UNIT);
-  zPC = entry;
+  init_sail_reset_vector(elf_entry);
 }
 
 int init_check(struct tv_spike_t *s)
-- 
cgit v1.2.3


From 0bce4fc40f2473e6f9f59e54b3e5061a4752b2d5 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Fri, 28 Sep 2018 17:26:05 -0700
Subject: RISC-V: Add device tree blob into rom, currently only when linked
 against spike.

---
 riscv/riscv_sim.c | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index 9a03245f..2ac5e800 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -108,6 +108,7 @@ void init_spike(const char *f, uint64_t entry)
 #ifdef SPIKE
   s = tv_init("RV64IMAC");
   tv_set_verbose(s, 1);
+  tv_set_dtb_in_rom(s, 1);
   tv_load_elf(s, f);
   tv_reset(s);
 #else
@@ -135,16 +136,26 @@ void init_sail_reset_vector(uint64_t entry)
   uint64_t addr = rv_rom_base;
   for (int i = 0; i < sizeof(reset_vec); i++)
     write_mem(addr++, (uint64_t)((char *)reset_vec)[i]);
+#ifdef SPIKE
+  const unsigned char *dtb = NULL;
+  int dtb_len;
+  tv_get_dtb(s, &dtb, &dtb_len);
+  fprintf(stderr, "Got %d bytes of dtb at %p\n", dtb_len, dtb);
+  for (int i = 0; i < dtb_len; i++)
+    write_mem(addr++, dtb[i]);
+#else
+  fprintf(stdout, "Running without rom device tree.\n");
   /* TODO: write DTB */
+#endif
 
   /* zero-fill to page boundary */
   const int align = 0x1000;
-  uint64_t rom_end = (addr + align -1)/align + align;
+  uint64_t rom_end = (addr + align -1)/align * align;
   for (int i = addr; i < rom_end; i++)
     write_mem(addr++, 0);
 
   /* set rom size */
-  rv_rom_size = addr - rv_rom_base;
+  rv_rom_size = rom_end - rv_rom_base;
   /* boot at reset vector */
   zPC = rv_rom_base;
 }
@@ -311,8 +322,11 @@ int main(int argc, char **argv)
   char *file = process_args(argc, argv);
   uint64_t entry = load_sail(file);
 
-  init_sail(entry);
+  /* initialize spike before sail so that we can access the device-tree blob,
+   * until we roll our own.
+   */
   init_spike(file, entry);
+  init_sail(entry);
 
   if (!init_check(s)) finish(1);
 
-- 
cgit v1.2.3


From 8525e0b26eaec05c2c031279693cd61c544fc12a Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Fri, 28 Sep 2018 18:37:11 -0700
Subject: RISC-V: tick the clock in the C platform.

---
 riscv/riscv_platform_impl.c |  1 +
 riscv/riscv_platform_impl.h |  1 +
 riscv/riscv_sail.h          |  2 ++
 riscv/riscv_sim.c           | 18 ++++++++++++++++--
 4 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/riscv/riscv_platform_impl.c b/riscv/riscv_platform_impl.c
index 1a1d42a7..3135895d 100644
--- a/riscv/riscv_platform_impl.c
+++ b/riscv/riscv_platform_impl.c
@@ -15,3 +15,4 @@ uint64_t rv_clint_base = UINT64_C(0x2000000);
 uint64_t rv_clint_size = UINT64_C(0xc0000);
 
 uint64_t rv_htif_tohost = UINT64_C(0x80001000);
+uint64_t rv_insns_per_tick = UINT64_C(100);
diff --git a/riscv/riscv_platform_impl.h b/riscv/riscv_platform_impl.h
index db5ff639..a3ab79f8 100644
--- a/riscv/riscv_platform_impl.h
+++ b/riscv/riscv_platform_impl.h
@@ -21,3 +21,4 @@ extern uint64_t rv_clint_base;
 extern uint64_t rv_clint_size;
 
 extern uint64_t rv_htif_tohost;
+extern uint64_t rv_insns_per_tick;
diff --git a/riscv/riscv_sail.h b/riscv/riscv_sail.h
index 596a8263..17afedbd 100644
--- a/riscv/riscv_sail.h
+++ b/riscv/riscv_sail.h
@@ -12,6 +12,8 @@ void model_fini(void);
 unit zinit_platform(unit);
 unit zinit_sys(unit);
 bool zstep(sail_int);
+unit ztick_clock(unit);
+unit ztick_platform(unit);
 
 extern bool zhtif_done;
 extern mach_bits zhtif_exit_code;
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index 2ac5e800..9e99136d 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -111,6 +111,8 @@ void init_spike(const char *f, uint64_t entry)
   tv_set_dtb_in_rom(s, 1);
   tv_load_elf(s, f);
   tv_reset(s);
+  /* sync the insns per tick */
+  rv_insns_per_tick = tv_get_insns_per_tick(s);
 #else
   s = NULL;
 #endif
@@ -261,6 +263,7 @@ void run_sail(void)
 
   /* initialize the step number */
   mach_int step_no = 0;
+  int insn_cnt = 0;
 
   while (!zhtif_done) {
     { /* run a Sail step */
@@ -271,7 +274,10 @@ void run_sail(void)
       if (have_exception) goto step_exception;
       flush_logs();
     }
-    if (stepped) step_no++;
+    if (stepped) {
+      step_no++;
+      insn_cnt++;
+    }
 
 #ifdef SPIKE
     { /* run a Spike step */
@@ -303,7 +309,15 @@ void run_sail(void)
     }
 #endif
 
-    /* TODO: update time */
+    if (insn_cnt == rv_insns_per_tick) {
+      insn_cnt = 0;
+      ztick_clock(UNIT);
+      ztick_platform(UNIT);
+#ifdef SPIKE
+      tv_tick_clock(s);
+      tv_step_io(s);
+#endif
+    }
   }
 
  dump_state:
-- 
cgit v1.2.3


From 2a511449bcd694a5a8e2d16fb65262c914861ba3 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Tue, 2 Oct 2018 12:02:00 -0700
Subject: RISC-V: implement terminal output for C platform.

---
 riscv/riscv_platform.c      |  7 +++++--
 riscv/riscv_platform_impl.c | 10 ++++++++++
 riscv/riscv_platform_impl.h |  3 +++
 riscv/riscv_sim.c           | 39 ++++++++++++++++++++++++++++++++++-----
 4 files changed, 52 insertions(+), 7 deletions(-)

diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index fa3b49aa..5eeb0eb7 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -48,8 +48,11 @@ unit cancel_reservation(unit u)
   return UNIT;
 }
 
-unit plat_term_write(mach_bits c)
-{ return UNIT; }
+unit plat_term_write(mach_bits s)
+{ char c = s & 0xff;
+  plat_term_write_impl(c);
+  return UNIT;
+}
 
 void plat_insns_per_tick(sail_int *rop, unit u)
 { }
diff --git a/riscv/riscv_platform_impl.c b/riscv/riscv_platform_impl.c
index 3135895d..d8d52da0 100644
--- a/riscv/riscv_platform_impl.c
+++ b/riscv/riscv_platform_impl.c
@@ -1,4 +1,6 @@
 #include "riscv_platform_impl.h"
+#include <unistd.h>
+#include <stdio.h>
 
 /* Settings of the platform implementation, with common defaults. */
 
@@ -16,3 +18,11 @@ uint64_t rv_clint_size = UINT64_C(0xc0000);
 
 uint64_t rv_htif_tohost = UINT64_C(0x80001000);
 uint64_t rv_insns_per_tick = UINT64_C(100);
+
+int term_fd = 1; // set during startup
+void plat_term_write_impl(char c)
+{
+  if (write(term_fd, &c, sizeof(c)) < 0) {
+    fprintf(stderr, "Unable to write to terminal!\n");
+  }
+}
diff --git a/riscv/riscv_platform_impl.h b/riscv/riscv_platform_impl.h
index a3ab79f8..562f8554 100644
--- a/riscv/riscv_platform_impl.h
+++ b/riscv/riscv_platform_impl.h
@@ -22,3 +22,6 @@ extern uint64_t rv_clint_size;
 
 extern uint64_t rv_htif_tohost;
 extern uint64_t rv_insns_per_tick;
+
+extern int term_fd;
+void plat_term_write_impl(char c);
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index 9e99136d..fc732e89 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -1,6 +1,11 @@
 #include <getopt.h>
 #include <stdio.h>
 #include <stdlib.h>
+#include <errno.h>
+#include <unistd.h>
+#include <sys/types.h>
+#include <sys/stat.h>
+#include <fcntl.h>
 
 #include "elf.h"
 #include "sail.h"
@@ -34,12 +39,13 @@ struct tv_spike_t;
 
 static bool do_dump_dts = false;
 struct tv_spike_t *s = NULL;
+char *term_log = NULL;
 
 static struct option options[] = {
   {"enable-dirty",      no_argument,       0, 'd'},
   {"enable-misaligned", no_argument,       0, 'm'},
   {"dump-dts",          no_argument,       0, 's'},
-  {"verbosity",         required_argument, 0, 'v'},
+  {"terminal-log",      required_argument, 0, 't'},
   {"help",              no_argument,       0, 'h'},
   {0, 0, 0, 0}
 };
@@ -59,7 +65,7 @@ char *process_args(int argc, char **argv)
 {
   int c, idx = 1;
   while(true) {
-    c = getopt_long(argc, argv, "dmsv:h", options, &idx);
+    c = getopt_long(argc, argv, "dmst:v:h", options, &idx);
     if (c == -1) break;
     switch (c) {
     case 'd':
@@ -71,6 +77,9 @@ char *process_args(int argc, char **argv)
     case 's':
       do_dump_dts = true;
       break;
+    case 't':
+      term_log = strdup(optarg);
+      break;
     case 'h':
       print_usage(argv[0], 0);
       break;
@@ -79,8 +88,8 @@ char *process_args(int argc, char **argv)
       print_usage(argv[0], 1);
     }
   }
-
   if (idx >= argc) print_usage(argv[0], 0);
+  if (term_log == NULL) term_log = strdup("term.log");
   return argv[idx];
 }
 
@@ -146,7 +155,7 @@ void init_sail_reset_vector(uint64_t entry)
   for (int i = 0; i < dtb_len; i++)
     write_mem(addr++, dtb[i]);
 #else
-  fprintf(stdout, "Running without rom device tree.\n");
+  fprintf(stderr, "Running without rom device tree.\n");
   /* TODO: write DTB */
 #endif
 
@@ -327,13 +336,32 @@ void run_sail(void)
   finish(diverged);
 
  step_exception:
-  fprintf(stdout, "Sail exception!");
+  fprintf(stderr, "Sail exception!");
   goto dump_state;
 }
 
+void init_logs()
+{
+#ifdef SPIKE
+  // The Spike interface uses stdout for terminal output, and stderr for logs.
+  // Do the same here.
+  int logfd;
+  if (dup2(1, 2) < 0) {
+    fprintf(stderr, "Unable to dup 1 -> 2: %s\n", strerror(errno));
+    exit(1);
+  }
+  if ((term_fd = open(term_log, O_WRONLY|O_CREAT|O_TRUNC, S_IRUSR|S_IRGRP|S_IROTH|S_IWUSR)) < 0) {
+    fprintf(stderr, "Cannot create terminal log '%s': %s\n", term_log, strerror(errno));
+    exit(1);
+  }
+#endif
+}
+
 int main(int argc, char **argv)
 {
   char *file = process_args(argc, argv);
+  init_logs();
+
   uint64_t entry = load_sail(file);
 
   /* initialize spike before sail so that we can access the device-tree blob,
@@ -345,4 +373,5 @@ int main(int argc, char **argv)
   if (!init_check(s)) finish(1);
 
   run_sail();
+  flush_logs();
 }
-- 
cgit v1.2.3


From 90b1e6717008f66f2bab6b7da844c4919583fe67 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Tue, 2 Oct 2018 12:03:23 -0700
Subject: RISC-V: adjust main loop for the non-spike case.

---
 riscv/riscv_sim.c | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index fc732e89..17e426eb 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -300,23 +300,24 @@ void run_sail(void)
         fprintf(stdout, "Sail done (exit-code %ld), but not Spike!\n", zhtif_exit_code);
         exit(1);
       }
-      /* check exit code */
-      if (zhtif_exit_code == 0)
-        fprintf(stdout, "SUCCESS\n");
-      else
-        fprintf(stdout, "FAILURE: %ld\n", zhtif_exit_code);
     } else {
       if (spike_done) {
         fprintf(stdout, "Spike done, but not Sail!\n");
         exit(1);
       }
-
-      if (!compare_states(s)) {
-        diverged = true;
-        break;
-      }
+    }
+    if (!compare_states(s)) {
+      diverged = true;
+      break;
     }
 #endif
+    if (zhtif_done) {
+      /* check exit code */
+      if (zhtif_exit_code == 0)
+        fprintf(stdout, "SUCCESS\n");
+      else
+        fprintf(stdout, "FAILURE: %ld\n", zhtif_exit_code);
+    }
 
     if (insn_cnt == rv_insns_per_tick) {
       insn_cnt = 0;
-- 
cgit v1.2.3


From 666128be44e51d6b781aedb6fdc97cd90fa59c3c Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Sat, 6 Oct 2018 19:42:22 -0700
Subject: RISC-V: fix: sstatus.SD depends on .XS and .FS.

---
 riscv/riscv_sys.sail | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 59bff606..37c45117 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -375,13 +375,17 @@ function lower_mstatus(m : Mstatus) -> Sstatus = {
 }
 
 function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
-  let m = update_SD(m, s.SD());
   // FIXME: This should be parameterized by a platform setting.  For now, match spike.
   // let m = update_UXL(m, s.UXL());
   let m = update_MXR(m, s.MXR());
   let m = update_SUM(m, s.SUM());
+
+  // FIXME: Should XS and FS check whether X and F|D are supported in misa?
   let m = update_XS(m, s.XS());
   let m = update_FS(m, s.FS());
+  let m = update_SD(m, extStatus_of_bits(m.FS()) == Dirty
+                     | extStatus_of_bits(m.XS()) == Dirty);
+
   let m = update_SPP(m, s.SPP());
   let m = update_SPIE(m, s.SPIE());
   let m = update_UPIE(m, s.UPIE());
-- 
cgit v1.2.3


From e3490924e6bce23d3d4b236fdc61c7345a17e814 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Mon, 8 Oct 2018 08:43:31 -0700
Subject: RISC-V: various fixes - add mstatus to cross-check - fix typo in
 assembly mapping for lr/sc

---
 riscv/riscv.sail   | 4 ++--
 riscv/riscv_sail.h | 1 +
 riscv/riscv_sim.c  | 1 +
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 2cad614e..71ad0137 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -851,7 +851,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
        }
 
 mapping clause assembly = LOADRES(aq, rl, rs1, size, rd)
-                      <-> "lr." ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
+                      <-> "lr" ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1)
 
 /* ****************************************************************** */
 union clause ast = STORECON : (bool, bool, regbits, regbits, word_width, regbits)
@@ -916,7 +916,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
   }
 }
 
-mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd) <-> "sc." ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
+mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd) <-> "sc" ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 /* ****************************************************************** */
 union clause ast = AMO : (amoop, bool, bool, regbits, regbits, word_width, regbits)
diff --git a/riscv/riscv_sail.h b/riscv/riscv_sail.h
index 17afedbd..f2569b3b 100644
--- a/riscv/riscv_sail.h
+++ b/riscv/riscv_sail.h
@@ -31,6 +31,7 @@ extern mach_bits
   zx16, zx17, zx18, zx19, zx20, zx21, zx22, zx23,
   zx24, zx25, zx26, zx27, zx28, zx29, zx30, zx31;
 
+extern mach_bits zmstatus;
 extern mach_bits zmepc, zmtval;
 extern mach_bits zsepc, zstval;
 
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index 17e426eb..79c353f9 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -247,6 +247,7 @@ int compare_states(struct tv_spike_t *s)
   passed &= tv_check_csr(s, CSR_MCAUSE, zmcause.zMcause_chunk_0);
   passed &= tv_check_csr(s, CSR_MEPC, zmepc);
   passed &= tv_check_csr(s, CSR_MTVAL, zmtval);
+  passed &= tv_check_csr(s, CSR_MSTATUS, zmstatus);
 
   passed &= tv_check_csr(s, CSR_SCAUSE, zscause.zMcause_chunk_0);
   passed &= tv_check_csr(s, CSR_SEPC, zsepc);
-- 
cgit v1.2.3


From d43b475507ed9144b26be124376c3e656005a416 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Mon, 8 Oct 2018 09:35:11 -0700
Subject: RISC-V: Add a platform knob to control mtval contents on illegal
 instruction faults.

---
 riscv/platform.ml                 |  2 ++
 riscv/platform_main.ml            |  3 +++
 riscv/riscv_extras.lem            |  4 ++++
 riscv/riscv_extras_sequential.lem |  4 ++++
 riscv/riscv_platform.c            |  3 +++
 riscv/riscv_platform.h            |  1 +
 riscv/riscv_platform.sail         | 16 ++++++++++++++++
 riscv/riscv_platform_impl.c       |  5 +++--
 riscv/riscv_platform_impl.h       |  1 +
 riscv/riscv_sim.c                 | 11 ++++++-----
 riscv/riscv_step.sail             |  6 ++++--
 riscv/riscv_sys.sail              | 12 ------------
 riscv/riscv_types.sail            |  7 +++++--
 13 files changed, 52 insertions(+), 23 deletions(-)

diff --git a/riscv/platform.ml b/riscv/platform.ml
index 092df80f..06486ca2 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -56,6 +56,7 @@ module Elf = Elf_loader;;
 
 let config_enable_dirty_update = ref false
 let config_enable_misaligned_access = ref false
+let config_mtval_has_illegal_inst_bits = ref false
 
 (* Mapping to Sail externs *)
 
@@ -82,6 +83,7 @@ let make_rom start_pc =
 
 let enable_dirty_update () = !config_enable_dirty_update
 let enable_misaligned_access () = !config_enable_misaligned_access
+let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits
 
 let rom_base () = bits_of_int64 P.rom_base
 let rom_size () = bits_of_int   !rom_size_ref
diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml
index e204daee..b33247f1 100644
--- a/riscv/platform_main.ml
+++ b/riscv/platform_main.ml
@@ -73,6 +73,9 @@ let options = Arg.align ([("-dump-dts",
                           ("-enable-misaligned-access",
                            Arg.Set P.config_enable_misaligned_access,
                            " enable misaligned accesses without M-mode traps");
+                          ("-mtval-has-illegal-inst-bits",
+                           Arg.Set P.config_mtval_has_illegal_inst_bits,
+                           " mtval stores instruction bits on an illegal instruction exception");
                           ("-with-dtc",
                            Arg.String PI.set_dtc,
                            " full path to dtc to use")
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index a6fa1298..7028d5b8 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -97,6 +97,10 @@ val plat_enable_misaligned_access : unit -> bool
 let plat_enable_misaligned_access () = false
 declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
 
+val plat_mtval_has_illegal_inst_bits : unit -> bool
+let plat_mtval_has_illegal_inst_bits () = false
+declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
+
 val plat_insns_per_tick : unit -> integer
 let plat_insns_per_tick () = 1
 declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem
index a6fa1298..7028d5b8 100644
--- a/riscv/riscv_extras_sequential.lem
+++ b/riscv/riscv_extras_sequential.lem
@@ -97,6 +97,10 @@ val plat_enable_misaligned_access : unit -> bool
 let plat_enable_misaligned_access () = false
 declare ocaml target_rep function plat_enable_misaligned_access = `Platform.enable_misaligned_access`
 
+val plat_mtval_has_illegal_inst_bits : unit -> bool
+let plat_mtval_has_illegal_inst_bits () = false
+declare ocaml target_rep function plat_mtval_has_illegal_inst_bits = `Platform.mtval_has_illegal_inst_bits`
+
 val plat_insns_per_tick : unit -> integer
 let plat_insns_per_tick () = 1
 declare ocaml target_rep function plat_insns_per_tick = `Platform.insns_per_tick`
diff --git a/riscv/riscv_platform.c b/riscv/riscv_platform.c
index 5eeb0eb7..f0aff76a 100644
--- a/riscv/riscv_platform.c
+++ b/riscv/riscv_platform.c
@@ -14,6 +14,9 @@ bool plat_enable_dirty_update(unit u)
 bool plat_enable_misaligned_access(unit u)
 { return rv_enable_misaligned; }
 
+bool plat_mtval_has_illegal_inst_bits(unit u)
+{ return rv_mtval_has_illegal_inst_bits; }
+
 mach_bits plat_ram_base(unit u)
 { return rv_ram_base; }
 
diff --git a/riscv/riscv_platform.h b/riscv/riscv_platform.h
index 4401ad49..93782660 100644
--- a/riscv/riscv_platform.h
+++ b/riscv/riscv_platform.h
@@ -3,6 +3,7 @@
 
 bool plat_enable_dirty_update(unit);
 bool plat_enable_misaligned_access(unit);
+bool plat_mtval_has_illegal_inst_bits(unit);
 
 mach_bits plat_ram_base(unit);
 mach_bits plat_ram_size(unit);
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index c4af9c79..3020d23d 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -22,6 +22,11 @@ val plat_enable_misaligned_access = {ocaml: "Platform.enable_misaligned_access",
                                      c: "plat_enable_misaligned_access",
                                      lem: "plat_enable_misaligned_access"} : unit -> bool
 
+/* whether mtval stores the bits of a faulting instruction on illegal instruction exceptions */
+val plat_mtval_has_illegal_inst_bits = {ocaml: "Platform.mtval_has_illegal_inst_bits",
+                                        c: "plat_mtval_has_illegal_inst_bits",
+                                        lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool
+
 /* ROM holding reset vector and device-tree DTB */
 val plat_rom_base   = {ocaml: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits
 val plat_rom_size   = {ocaml: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits
@@ -265,3 +270,14 @@ function tick_platform() -> unit = {
   cancel_reservation();
   htif_tick();
 }
+
+/* Platform-specific handling of instruction faults */
+
+function handle_illegal() -> unit = {
+  let info = if plat_mtval_has_illegal_inst_bits ()
+             then Some(instbits)
+             else None();
+  let t : sync_exception = struct { trap    = E_Illegal_Instr,
+                                    excinfo = info };
+  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
+}
diff --git a/riscv/riscv_platform_impl.c b/riscv/riscv_platform_impl.c
index d8d52da0..04a661c0 100644
--- a/riscv/riscv_platform_impl.c
+++ b/riscv/riscv_platform_impl.c
@@ -4,8 +4,9 @@
 
 /* Settings of the platform implementation, with common defaults. */
 
-bool rv_enable_dirty_update = false;
-bool rv_enable_misaligned   = false;
+bool rv_enable_dirty_update         = false;
+bool rv_enable_misaligned           = false;
+bool rv_mtval_has_illegal_inst_bits = false;
 
 uint64_t rv_ram_base = UINT64_C(0x80000000);
 uint64_t rv_ram_size = UINT64_C(0x80000000);
diff --git a/riscv/riscv_platform_impl.h b/riscv/riscv_platform_impl.h
index 562f8554..85e25c95 100644
--- a/riscv/riscv_platform_impl.h
+++ b/riscv/riscv_platform_impl.h
@@ -10,6 +10,7 @@
 
 extern bool rv_enable_dirty_update;
 extern bool rv_enable_misaligned;
+extern bool rv_mtval_has_illegal_inst_bits;
 
 extern uint64_t rv_ram_base;
 extern uint64_t rv_ram_size;
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index 79c353f9..9db1ea59 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -42,11 +42,12 @@ struct tv_spike_t *s = NULL;
 char *term_log = NULL;
 
 static struct option options[] = {
-  {"enable-dirty",      no_argument,       0, 'd'},
-  {"enable-misaligned", no_argument,       0, 'm'},
-  {"dump-dts",          no_argument,       0, 's'},
-  {"terminal-log",      required_argument, 0, 't'},
-  {"help",              no_argument,       0, 'h'},
+  {"enable-dirty",                no_argument,       0, 'd'},
+  {"enable-misaligned",           no_argument,       0, 'm'},
+  {"mtval-has-illegal-inst-bits", no_argument,       0, 'i'},
+  {"dump-dts",                    no_argument,       0, 's'},
+  {"terminal-log",                required_argument, 0, 't'},
+  {"help",                        no_argument,       0, 'h'},
   {0, 0, 0, 0}
 };
 
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index f9675115..218be598 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -63,7 +63,8 @@ function step(step_no) = {
             match decodeCompressed(h) {
               None() => {
                 print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") <no-decode>");
-                handle_decode_exception(EXTZ(h));
+                instbits = EXTZ(h);
+                handle_illegal();
                 (false, true)
               },
               Some(ast) => {
@@ -77,7 +78,8 @@ function step(step_no) = {
             match decode(w) {
               None() => {
                 print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") <no-decode>");
-                handle_decode_exception(EXTZ(w));
+                instbits = EXTZ(w);
+                handle_illegal();
                 (false, true)
               },
               Some(ast) => {
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 37c45117..9c49d9e5 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -976,21 +976,9 @@ function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
   nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
 }
 
-function handle_decode_exception(instbits : xlenbits) -> unit = {
-  let t : sync_exception = struct { trap    = E_Illegal_Instr,
-                                    excinfo = Some(instbits) };
-  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
-}
-
 function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
   nextPC = handle_trap(del_priv, true, i, PC, None())
 
-function handle_illegal() -> unit = {
-  let t : sync_exception = struct { trap    = E_Illegal_Instr,
-                                    excinfo = None() };
-  nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC)
-}
-
 /* state state initialization */
 
 function init_sys() -> unit = {
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index d269356c..4cbc6f87 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -34,8 +34,11 @@ let sp   : regbits = 0b00010  /* x2, stack pointer  */
 
 /* program counter */
 
-register PC     : xlenbits
-register nextPC : xlenbits
+register PC       : xlenbits
+register nextPC   : xlenbits
+
+/* internal state to hold instruction bits for faulting instructions */
+register instbits : xlenbits
 
 /* register file and accessors */
 
-- 
cgit v1.2.3


From 1f0716a98c3758675ab18e76d69ffac1e8d6a694 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Mon, 8 Oct 2018 12:20:33 -0700
Subject: RISC-V: add cli option to dump the platform device-tree.

---
 riscv/riscv_sim.c | 42 +++++++++++++++++++++++++++++++++++-------
 1 file changed, 35 insertions(+), 7 deletions(-)

diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index 9db1ea59..305c61f8 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -62,6 +62,24 @@ static void print_usage(const char *argv0, int ec)
   exit(ec);
 }
 
+static void dump_dts(void)
+{
+#ifdef SPIKE
+  size_t dts_len = 0;
+  struct tv_spike_t *s = tv_init("RV64IMAC", 0);
+  tv_get_dts(s, NULL, &dts_len);
+  if (dts_len > 0) {
+    unsigned char *dts = (unsigned char *)malloc(dts_len + 1);
+    dts[dts_len] = '\0';
+    tv_get_dts(s, dts, &dts_len);
+    fprintf(stdout, "%s\n", dts);
+  }
+#else
+  fprintf(stdout, "Spike linkage is currently needed to generate DTS.\n");
+#endif
+  exit(0);
+}
+
 char *process_args(int argc, char **argv)
 {
   int c, idx = 1;
@@ -89,6 +107,7 @@ char *process_args(int argc, char **argv)
       print_usage(argv[0], 1);
     }
   }
+  if (do_dump_dts) dump_dts();
   if (idx >= argc) print_usage(argv[0], 0);
   if (term_log == NULL) term_log = strdup("term.log");
   return argv[idx];
@@ -116,7 +135,7 @@ uint64_t load_sail(char *f)
 void init_spike(const char *f, uint64_t entry)
 {
 #ifdef SPIKE
-  s = tv_init("RV64IMAC");
+  s = tv_init("RV64IMAC", 1);
   tv_set_verbose(s, 1);
   tv_set_dtb_in_rom(s, 1);
   tv_load_elf(s, f);
@@ -149,12 +168,21 @@ void init_sail_reset_vector(uint64_t entry)
   for (int i = 0; i < sizeof(reset_vec); i++)
     write_mem(addr++, (uint64_t)((char *)reset_vec)[i]);
 #ifdef SPIKE
-  const unsigned char *dtb = NULL;
-  int dtb_len;
-  tv_get_dtb(s, &dtb, &dtb_len);
-  fprintf(stderr, "Got %d bytes of dtb at %p\n", dtb_len, dtb);
-  for (int i = 0; i < dtb_len; i++)
-    write_mem(addr++, dtb[i]);
+  unsigned char *dtb = NULL;
+  size_t dtb_len = 0;
+  tv_get_dtb(s, NULL, &dtb_len);
+  if (dtb_len > 0) {
+    dtb = (unsigned char *)malloc(dtb_len + 1);
+    dtb[dtb_len] = '\0';
+    if (!tv_get_dtb(s, dtb, &dtb_len)) {
+      fprintf(stderr, "Got %ld bytes of dtb at %p\n", dtb_len, dtb);
+      for (size_t i = 0; i < dtb_len; i++)
+        write_mem(addr++, dtb[i]);
+    } else {
+      fprintf(stderr, "Error getting DTB!\n");
+      exit(1);
+    }
+  }
 #else
   fprintf(stderr, "Running without rom device tree.\n");
   /* TODO: write DTB */
-- 
cgit v1.2.3


From 5be50269f940be8cc155d30843abfcc657ced54c Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Wed, 10 Oct 2018 12:36:49 -0700
Subject: RISC-V: Allow the C platform to get the DTB from a file, so that OS
 boot is possible without linking to Spike. When linked with Spike, ensure
 that the DTBs being used are identical.

---
 riscv/riscv_sim.c | 122 ++++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 100 insertions(+), 22 deletions(-)

diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index 305c61f8..276c7b1b 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -5,6 +5,7 @@
 #include <unistd.h>
 #include <sys/types.h>
 #include <sys/stat.h>
+#include <sys/mman.h>
 #include <fcntl.h>
 
 #include "elf.h"
@@ -14,6 +15,7 @@
 #include "riscv_platform_impl.h"
 #include "riscv_sail.h"
 
+//#define SPIKE 1
 #ifdef SPIKE
 #include "tv_spike_intf.h"
 #else
@@ -40,12 +42,19 @@ struct tv_spike_t;
 static bool do_dump_dts = false;
 struct tv_spike_t *s = NULL;
 char *term_log = NULL;
+char *dtb_file = NULL;
+unsigned char *dtb = NULL;
+size_t dtb_len = 0;
+
+unsigned char *spike_dtb = NULL;
+size_t spike_dtb_len = 0;
 
 static struct option options[] = {
   {"enable-dirty",                no_argument,       0, 'd'},
   {"enable-misaligned",           no_argument,       0, 'm'},
   {"mtval-has-illegal-inst-bits", no_argument,       0, 'i'},
   {"dump-dts",                    no_argument,       0, 's'},
+  {"device-tree-blob",            required_argument, 0, 'b'},
   {"terminal-log",                required_argument, 0, 't'},
   {"help",                        no_argument,       0, 'h'},
   {0, 0, 0, 0}
@@ -80,11 +89,41 @@ static void dump_dts(void)
   exit(0);
 }
 
+static void read_dtb(const char *path)
+{
+  int fd = open(path, O_RDONLY);
+  if (fd < 0) {
+    fprintf(stderr, "Unable to read DTB file %s: %s\n", path, strerror(errno));
+    exit(1);
+  }
+  struct stat st;
+  if (fstat(fd, &st) < 0) {
+    fprintf(stderr, "Unable to stat DTB file %s: %s\n", path, strerror(errno));
+    exit(1);
+  }
+  char *m = (char *)mmap(NULL, st.st_size, PROT_READ, MAP_PRIVATE, fd, 0);
+  if (m == MAP_FAILED) {
+    fprintf(stderr, "Unable to map DTB file %s: %s\n", path, strerror(errno));
+    exit(1);
+  }
+  dtb = (unsigned char *)malloc(st.st_size);
+  if (dtb == NULL) {
+    fprintf(stderr, "Cannot allocate DTB from file %s!\n", path);
+    exit(1);
+  }
+  memcpy(dtb, m, st.st_size);
+  dtb_len = st.st_size;
+  munmap(m, st.st_size);
+  close(fd);
+
+  fprintf(stdout, "Read %ld bytes of DTB from %s.\n", dtb_len, path);
+}
+
 char *process_args(int argc, char **argv)
 {
   int c, idx = 1;
   while(true) {
-    c = getopt_long(argc, argv, "dmst:v:h", options, &idx);
+    c = getopt_long(argc, argv, "dmsb:t:v:h", options, &idx);
     if (c == -1) break;
     switch (c) {
     case 'd':
@@ -93,9 +132,14 @@ char *process_args(int argc, char **argv)
     case 'm':
       rv_enable_misaligned = true;
       break;
+    case 'i':
+      rv_mtval_has_illegal_inst_bits = true;
     case 's':
       do_dump_dts = true;
       break;
+    case 'b':
+      dtb_file = strdup(optarg);
+      break;
     case 't':
       term_log = strdup(optarg);
       break;
@@ -110,7 +154,10 @@ char *process_args(int argc, char **argv)
   if (do_dump_dts) dump_dts();
   if (idx >= argc) print_usage(argv[0], 0);
   if (term_log == NULL) term_log = strdup("term.log");
-  return argv[idx];
+  if (dtb_file) read_dtb(dtb_file);
+
+  fprintf(stdout, "Running file %s.\n", argv[optind]);
+  return argv[optind];
 }
 
 uint64_t load_sail(char *f)
@@ -135,18 +182,43 @@ uint64_t load_sail(char *f)
 void init_spike(const char *f, uint64_t entry)
 {
 #ifdef SPIKE
+  /* The initialization order below matters. */
   s = tv_init("RV64IMAC", 1);
   tv_set_verbose(s, 1);
   tv_set_dtb_in_rom(s, 1);
   tv_load_elf(s, f);
   tv_reset(s);
+
   /* sync the insns per tick */
   rv_insns_per_tick = tv_get_insns_per_tick(s);
+
+  /* get DTB from spike */
+  tv_get_dtb(s, NULL, &spike_dtb_len);
+  if (spike_dtb_len > 0) {
+    spike_dtb = (unsigned char *)malloc(spike_dtb_len + 1);
+    dtb[spike_dtb_len] = '\0';
+    if (!tv_get_dtb(s, spike_dtb, &spike_dtb_len)) {
+      fprintf(stderr, "Got %ld bytes of dtb at %p\n", spike_dtb_len, spike_dtb);
+    } else {
+      fprintf(stderr, "Error getting DTB from Spike.\n");
+      exit(1);
+    }
+  } else {
+    fprintf(stderr, "No DTB available from Spike.\n");
+  }
 #else
   s = NULL;
 #endif
 }
 
+void tick_spike()
+{
+#ifdef SPIKE
+  tv_tick_clock(s);
+  tv_step_io(s);
+#endif
+}
+
 void init_sail_reset_vector(uint64_t entry)
 {
 #define RST_VEC_SIZE 8
@@ -167,25 +239,33 @@ void init_sail_reset_vector(uint64_t entry)
   uint64_t addr = rv_rom_base;
   for (int i = 0; i < sizeof(reset_vec); i++)
     write_mem(addr++, (uint64_t)((char *)reset_vec)[i]);
+
+  if (dtb && dtb_len) {
+    for (size_t i = 0; i < dtb_len; i++)
+      write_mem(addr++, dtb[i]);
+  }
+
 #ifdef SPIKE
-  unsigned char *dtb = NULL;
-  size_t dtb_len = 0;
-  tv_get_dtb(s, NULL, &dtb_len);
-  if (dtb_len > 0) {
-    dtb = (unsigned char *)malloc(dtb_len + 1);
-    dtb[dtb_len] = '\0';
-    if (!tv_get_dtb(s, dtb, &dtb_len)) {
-      fprintf(stderr, "Got %ld bytes of dtb at %p\n", dtb_len, dtb);
+  if (dtb && dtb_len) {
+    // Ensure that Spike's DTB matches the one provided.
+    bool matched = dtb_len == spike_dtb_len;
+    if (matched) {
       for (size_t i = 0; i < dtb_len; i++)
-        write_mem(addr++, dtb[i]);
-    } else {
-      fprintf(stderr, "Error getting DTB!\n");
+        matched = matched && (dtb[i] == spike_dtb[i]);
+    }
+    if (!matched) {
+      fprintf(stderr, "Provided DTB does not match Spike's!\n");
       exit(1);
     }
+  } else {
+    if (spike_dtb_len > 0) {
+      // Use the DTB from Spike.
+      for (size_t i = 0; i < spike_dtb_len; i++)
+        write_mem(addr++, spike_dtb[i]);
+    } else {
+      fprintf(stderr, "Running without rom device tree.\n");
+    }
   }
-#else
-  fprintf(stderr, "Running without rom device tree.\n");
-  /* TODO: write DTB */
 #endif
 
   /* zero-fill to page boundary */
@@ -353,10 +433,8 @@ void run_sail(void)
       insn_cnt = 0;
       ztick_clock(UNIT);
       ztick_platform(UNIT);
-#ifdef SPIKE
-      tv_tick_clock(s);
-      tv_step_io(s);
-#endif
+
+      tick_spike();
     }
   }
 
@@ -376,16 +454,16 @@ void init_logs()
 #ifdef SPIKE
   // The Spike interface uses stdout for terminal output, and stderr for logs.
   // Do the same here.
-  int logfd;
   if (dup2(1, 2) < 0) {
     fprintf(stderr, "Unable to dup 1 -> 2: %s\n", strerror(errno));
     exit(1);
   }
+#endif
+
   if ((term_fd = open(term_log, O_WRONLY|O_CREAT|O_TRUNC, S_IRUSR|S_IRGRP|S_IROTH|S_IWUSR)) < 0) {
     fprintf(stderr, "Cannot create terminal log '%s': %s\n", term_log, strerror(errno));
     exit(1);
   }
-#endif
 }
 
 int main(int argc, char **argv)
-- 
cgit v1.2.3


From 578877f6080d4026ce863c863e3db7bcb230e28b Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Tue, 23 Oct 2018 13:07:47 -0700
Subject: RISC-V: Initial splitting of instructions across multiple files.

---
 riscv/Makefile               |  4 +++-
 riscv/riscv.sail             | 37 -------------------------------------
 riscv/riscv_insts_begin.sail | 19 +++++++++++++++++++
 riscv/riscv_insts_end.sail   | 15 +++++++++++++++
 4 files changed, 37 insertions(+), 38 deletions(-)
 create mode 100644 riscv/riscv_insts_begin.sail
 create mode 100644 riscv/riscv_insts_end.sail

diff --git a/riscv/Makefile b/riscv/Makefile
index 72abc5da..f4a7d8b5 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,4 +1,6 @@
-SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail riscv.sail riscv_step.sail riscv_analysis.sail
+SAIL_INSTS = riscv.sail
+SAIL_INST_SRCS = riscv_insts_begin.sail $(SAIL_INSTS) riscv_insts_end.sail
+SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail $(SAIL_INST_SRCS) riscv_step.sail riscv_analysis.sail
 PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
 SAIL_DIR ?= $(realpath ..)
 SAIL ?= $(SAIL_DIR)/sail
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 71ad0137..c0c1d6e2 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -1,29 +1,3 @@
-/* Instruction definitions.
- *
- * This includes decoding, execution, and assembly parsing and printing.
- */
-
-scattered union ast
-
-val decode : bits(32) -> option(ast) effect pure
-
-val decodeCompressed : bits(16) -> option(ast) effect pure
-
-val cast print_insn : ast -> string
-
-/* returns whether an instruction was retired, used for computing minstret */
-val execute : ast -> bool effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
-scattered function execute
-
-val assembly : ast <-> string
-scattered mapping assembly
-
-val encdec : ast <-> bits(32)
-scattered mapping encdec
-
-val encdec_compressed : ast <-> bits(16)
-scattered mapping encdec_compressed
-
 /* ****************************************************************** */
 union clause ast = UTYPE : (bits(20), regbits, uop)
 
@@ -1585,14 +1559,3 @@ function clause execute C_ILLEGAL(s) = { handle_illegal(); false }
 mapping clause assembly = C_ILLEGAL(s) <-> "c.illegal" ^ spc() ^ hex_bits_16(s)
 
 /* ****************************************************************** */
-
-
-end ast
-end execute
-end assembly
-end encdec
-end encdec_compressed
-
-function decode bv = Some(encdec(bv))
-function decodeCompressed bv = Some(encdec_compressed(bv))
-function print_insn insn = assembly(insn)
\ No newline at end of file
diff --git a/riscv/riscv_insts_begin.sail b/riscv/riscv_insts_begin.sail
new file mode 100644
index 00000000..56fd8b43
--- /dev/null
+++ b/riscv/riscv_insts_begin.sail
@@ -0,0 +1,19 @@
+/* Instruction definitions.
+ *
+ * This includes decoding, execution, and assembly parsing and printing.
+ */
+
+scattered union ast
+
+/* returns whether an instruction was retired, used for computing minstret */
+val execute : ast -> bool effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
+scattered function execute
+
+val assembly : ast <-> string
+scattered mapping assembly
+
+val encdec : ast <-> bits(32)
+scattered mapping encdec
+
+val encdec_compressed : ast <-> bits(16)
+scattered mapping encdec_compressed
diff --git a/riscv/riscv_insts_end.sail b/riscv/riscv_insts_end.sail
new file mode 100644
index 00000000..144f06e3
--- /dev/null
+++ b/riscv/riscv_insts_end.sail
@@ -0,0 +1,15 @@
+/* End definitions */
+end ast
+end execute
+end assembly
+end encdec
+end encdec_compressed
+
+val cast print_insn : ast -> string
+function print_insn insn = assembly(insn)
+
+val decode : bits(32) -> option(ast) effect pure
+function decode bv = Some(encdec(bv))
+
+val decodeCompressed : bits(16) -> option(ast) effect pure
+function decodeCompressed bv = Some(encdec_compressed(bv))
-- 
cgit v1.2.3


From 852929bb8b47993bcb642ada41802383a308c9c2 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Tue, 23 Oct 2018 14:00:31 -0700
Subject: RISC-V: separate jalr execute clause for seq model and rmem.

---
 riscv/Makefile             | 15 ++++++++++++---
 riscv/riscv.sail           | 18 ++----------------
 riscv/riscv_jalr_rmem.sail |  9 +++++++++
 riscv/riscv_jalr_seq.sail  | 14 ++++++++++++++
 4 files changed, 37 insertions(+), 19 deletions(-)
 create mode 100644 riscv/riscv_jalr_rmem.sail
 create mode 100644 riscv/riscv_jalr_seq.sail

diff --git a/riscv/Makefile b/riscv/Makefile
index f4a7d8b5..e6bbbd5c 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,6 +1,15 @@
-SAIL_INSTS = riscv.sail
-SAIL_INST_SRCS = riscv_insts_begin.sail $(SAIL_INSTS) riscv_insts_end.sail
-SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail $(SAIL_INST_SRCS) riscv_step.sail riscv_analysis.sail
+SAIL_SEQ_INST  = riscv.sail riscv_jalr_seq.sail
+SAIL_RMEM_INST = riscv.sail riscv_jalr_rmem.sail
+
+SAIL_SEQ_INST_SRCS  = riscv_insts_begin.sail $(SAIL_SEQ_INST) riscv_insts_end.sail
+SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.sail
+
+# non-instruction sources
+SAIL_OTHER_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail
+
+SAIL_SRCS      = $(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS)  riscv_step.sail riscv_analysis.sail
+SAIL_RMEM_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_RMEM_INST_SRCS) riscv_step.sail riscv_analysis.sail
+
 PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml
 SAIL_DIR ?= $(realpath ..)
 SAIL ?= $(SAIL_DIR)/sail
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index c0c1d6e2..47d714f5 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -61,25 +61,11 @@ union clause ast = RISCV_JALR : (bits(12), regbits, regbits)
 
 mapping clause encdec = RISCV_JALR(imm, rs1, rd) <-> imm @ rs1 @ 0b000 @ rd @ 0b1100111
 
-function clause execute (RISCV_JALR(imm, rs1, rd)) = {
-  /* write rd before anything else to prevent unintended strength */
-  X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
-  let newPC : xlenbits = X(rs1) + EXTS(imm);
-/*  RMEM FIXME: For the sequential model, the above definition doesn't work directly
-    if rs1 = rd.  We would effectively have to keep a regfile for reads and another for
-    writes, and swap on instruction fetch.  This could perhaps be optimized in
-    some manner, but for now, we just reorder the previous two lines to improve simulator
-    performance in the sequential model, as below:
-  let newPC : xlenbits = X(rs1) + EXTS(imm);
-  X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
-*/
-  nextPC = newPC[63..1] @ 0b0;
-  true
-}
-
 mapping clause assembly = RISCV_JALR(imm, rs1, rd)
                       <-> "jalr" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
 
+/* see riscv_jalr_seq.sail or riscv_jalr_rmem.sail for the execute clause. */
+
 /* ****************************************************************** */
 union clause ast = BTYPE : (bits(13), regbits, regbits, bop)
 
diff --git a/riscv/riscv_jalr_rmem.sail b/riscv/riscv_jalr_rmem.sail
new file mode 100644
index 00000000..3e5eec9a
--- /dev/null
+++ b/riscv/riscv_jalr_rmem.sail
@@ -0,0 +1,9 @@
+/* The definition for the memory model. */
+
+function clause execute (RISCV_JALR(imm, rs1, rd)) = {
+  /* write rd before anything else to prevent unintended strength */
+  X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */
+  let newPC : xlenbits = X(rs1) + EXTS(imm);
+  nextPC = newPC[63..1] @ 0b0;
+  true
+}
diff --git a/riscv/riscv_jalr_seq.sail b/riscv/riscv_jalr_seq.sail
new file mode 100644
index 00000000..b38563ef
--- /dev/null
+++ b/riscv/riscv_jalr_seq.sail
@@ -0,0 +1,14 @@
+/* The definition for the sequential model. */
+
+function clause execute (RISCV_JALR(imm, rs1, rd)) = {
+/* For the sequential model, the memory-model definition doesn't work directly
+   if rs1 = rd.  We would effectively have to keep a regfile for reads and another for
+   writes, and swap on instruction completion.  This could perhaps be optimized in
+   some manner, but for now, we just keep a reordered definition to improve simulator
+   performance.
+*/
+  let newPC : xlenbits = X(rs1) + EXTS(imm);
+  X(rd) = nextPC;
+  nextPC = newPC[63..1] @ 0b0;
+  true
+}
-- 
cgit v1.2.3


From 1e7b116842ea0e0ad76a70e2736398ef2211dde9 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Tue, 23 Oct 2018 15:17:22 -0700
Subject: RISC-V: use stderr for terminal output in OCaml backend.

Also add a brief README for booting Linux on the C and OCaml backends.
---
 riscv/README           | 23 +++++++++++++++++++++++
 riscv/platform_impl.ml |  2 +-
 2 files changed, 24 insertions(+), 1 deletion(-)
 create mode 100644 riscv/README

diff --git a/riscv/README b/riscv/README
new file mode 100644
index 00000000..b925821e
--- /dev/null
+++ b/riscv/README
@@ -0,0 +1,23 @@
+Booting Linux with the C backend:
+---------------------------------
+
+The C model needs an ELF-version of the BBL (Berkeley-Boot-Loader) that contains
+the Linux kernel as an embedded payload.  It also needs a DTB (device-tree blob)
+file describing the platform.  Once those are available, the model should be run
+as:
+
+$ ./riscv_sim -b spike.dtb bbl > execution-trace.log 2>&1 &
+$ tail -f term.log
+
+The term.log file contains the console boot messages.
+
+
+Booting Linux with the OCaml backend:
+-------------------------------------
+
+The OCaml model only needs the ELF-version of the BBL, since it can generate its
+own DTB.
+
+$ ./platform bbl > execution-trace.log
+
+The console output is sent to stderr.
diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml
index e593dce9..c5cc3fff 100644
--- a/riscv/platform_impl.ml
+++ b/riscv/platform_impl.ml
@@ -159,7 +159,7 @@ let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *)
 (* Terminal I/O *)
 
 let term_write char =
-  ignore (Unix.write_substring Unix.stdout (String.make 1 char) 0 1)
+  ignore (Unix.write_substring Unix.stderr (String.make 1 char) 0 1)
 
 let rec term_read () =
   let buf = Bytes.make 1 '\000' in
-- 
cgit v1.2.3


From 8ae06c742324160e2677f233a8e509eaa46b54c3 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Tue, 23 Oct 2018 16:05:47 -0700
Subject: RISC-V: switch c tests to use the C platform simulator; update
 .gitignore.

---
 .gitignore                  | 2 ++
 test/riscv/run_tests.sh     | 5 ++---
 test/riscv/tests/.gitignore | 1 +
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/.gitignore b/.gitignore
index 6e5f1362..3ad05e9d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -91,7 +91,9 @@ lib/hol/sail-heap
 /riscv/riscv
 /riscv/platform
 /riscv/riscv.c
+/riscv/riscv_model.c
 /riscv/riscv_c
+/riscv/riscv_sim
 
 /x86/x86.lem
 /x86/x86.ml
diff --git a/test/riscv/run_tests.sh b/test/riscv/run_tests.sh
index 512feabf..319504ad 100755
--- a/test/riscv/run_tests.sh
+++ b/test/riscv/run_tests.sh
@@ -67,7 +67,7 @@ for test in $DIR/tests/*.elf; do
     fi
 done
 
-if make -C $SAILDIR/riscv riscv_c;
+if make -C $SAILDIR/riscv riscv_sim;
 then
     green "Building RISCV specification to C" "ok"
 else
@@ -75,8 +75,7 @@ else
 fi
 
 for test in $DIR/tests/*.elf; do
-    $SAILDIR/sail -elf $test -o ${test%.elf}.bin 2> /dev/null;
-    if timeout 5 $SAILDIR/riscv/riscv_c --binary=0x1000,reset_vec.bin --image=${test%.elf}.bin > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout
+    if timeout 5 $SAILDIR/riscv/riscv_sim $test > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout
     then
 	green "$(basename $test)" "ok"
     else
diff --git a/test/riscv/tests/.gitignore b/test/riscv/tests/.gitignore
index f47cb204..72a5e441 100644
--- a/test/riscv/tests/.gitignore
+++ b/test/riscv/tests/.gitignore
@@ -1 +1,2 @@
 *.out
+*.cout
-- 
cgit v1.2.3


From 5471af45fd04169eb184371dcd8f791e507eab6f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 24 Oct 2018 17:25:47 +0100
Subject: Add constraint synonyms

Currently not enabled by default, the flag -Xconstraint_synonyms
enables them

For generating constraints in ASL parser, we want to be able to give
names to the constraints that we attach to certain variables. It's
slightly awkward right now when constraints get long complicated
because the entire constraint always has to be typed out in full
whenever it appears, and there's no way to abstract away from that.

This adds constraint synonyms, which work much like type synonyms
except for constraints, e.g.

constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256

these constraints can then be used instead of the full constraint, e.g.

val f : forall 'n, where Size('n). int('n) -> unit

Unfortunatly we need to have a keyword to 'call' the constraint
synonym otherwise the grammer stops being LR(1). This could be
resolved by parsing all constraints into Parse_ast.atyp and then
de-sugaring them into constraints, which is what happens for
n-expressions already, but that would require quite a bit of work on
the parser.

To avoid this forcing changes to any other parts of Sail, the intended
invariant is that all constraints appearing anywhere in a type-checked
AST have no constraint synonyms, so they don't have to worry about
matching on NC_app, or calling Env.expand_typquant_synonyms (which
isn't even exported for this reason).
---
 editors/sail2-mode.el                         |   2 +-
 language/sail.ott                             |  26 +++--
 src/ast_util.ml                               |  27 ++++-
 src/ast_util.mli                              |   2 +
 src/initial_check.ml                          |   8 ++
 src/lexer.mll                                 |   2 +
 src/parse_ast.ml                              |   2 +
 src/parser.mly                                |   6 +-
 src/pretty_print_sail.ml                      |   5 +-
 src/sail.ml                                   |   3 +
 src/type_check.ml                             | 156 ++++++++++++++++++--------
 src/type_check.mli                            |   4 +
 src/util.ml                                   |   1 +
 src/util.mli                                  |   1 +
 test/typecheck/pass/constraint_sym.sail       |   7 ++
 test/typecheck/pass/constraint_sym/v1.expect  |   5 +
 test/typecheck/pass/constraint_sym/v1.sail    |   7 ++
 test/typecheck/pass/constraint_sym/v2.expect  |   5 +
 test/typecheck/pass/constraint_sym/v2.sail    |   7 ++
 test/typecheck/pass/constraint_sym/v3.expect  |   5 +
 test/typecheck/pass/constraint_sym/v3.sail    |   7 ++
 test/typecheck/pass/constraint_sym/v4.expect  |   5 +
 test/typecheck/pass/constraint_sym/v4.sail    |   6 +
 test/typecheck/pass/global_type_var/v3.expect |   2 +-
 24 files changed, 234 insertions(+), 67 deletions(-)
 create mode 100644 test/typecheck/pass/constraint_sym.sail
 create mode 100644 test/typecheck/pass/constraint_sym/v1.expect
 create mode 100644 test/typecheck/pass/constraint_sym/v1.sail
 create mode 100644 test/typecheck/pass/constraint_sym/v2.expect
 create mode 100644 test/typecheck/pass/constraint_sym/v2.sail
 create mode 100644 test/typecheck/pass/constraint_sym/v3.expect
 create mode 100644 test/typecheck/pass/constraint_sym/v3.sail
 create mode 100644 test/typecheck/pass/constraint_sym/v4.expect
 create mode 100644 test/typecheck/pass/constraint_sym/v4.sail

diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index 05d3eb60..de8c3d11 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -9,7 +9,7 @@
     "overload" "cast" "sizeof" "constraint" "default" "assert" "newtype" "from"
     "pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to"
     "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield"
-    "mapping"))
+    "mapping" "where"))
 
 (defconst sail2-kinds
   '("Int" "Type" "Order" "inc" "dec"
diff --git a/language/sail.ott b/language/sail.ott
index 2edffcbe..59d51d68 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -293,6 +293,7 @@ n_constraint :: 'NC_' ::=
   | kid 'IN' { num1 , ... , numn }              :: :: set
   | n_constraint \/ n_constraint'               :: :: or
   | n_constraint /\ n_constraint'               :: :: and
+  | id ( nexp1 , ... , nexpn )                  :: :: app
   | true                                        :: :: true
   | false                                       :: :: false
 
@@ -1012,29 +1013,30 @@ prec :: '' ::=
 def :: 'DEF_' ::=
   {{ com top-level definition }}
   {{ auxparam 'a }}
-  | kind_def                                         :: :: kind
+  | kind_def                                           :: :: kind
     {{ com definition of named kind identifiers }}
-  | type_def                                         :: :: type
+  | type_def                                           :: :: type
     {{ com type definition }}
-  | fundef                                           :: :: fundef
+  | fundef                                             :: :: fundef
     {{ com function definition }}
-  | mapdef                                           :: :: mapdef
+  | mapdef                                             :: :: mapdef
     {{ com mapping definition }}
-  | letbind                                          :: :: val
+  | letbind                                            :: :: val
     {{ com value definition }}
-  | val_spec                                         :: :: spec
+  | val_spec                                           :: :: spec
     {{ com top-level type constraint }}
-  | fix prec num id                                  :: :: fixity
+  | fix prec num id                                    :: :: fixity
     {{ com fixity declaration }}
-  |  overload id [ id1 ; ... ; idn ]                 :: :: overload
+  |  overload id [ id1 ; ... ; idn ]                   :: :: overload
     {{ com operator overload specification }}
-  | default_spec                                     :: :: default
+  | default_spec                                       :: :: default
     {{ com default kind and type assumptions }}
-  | scattered_def                                    :: :: scattered
+  | scattered_def                                      :: :: scattered
     {{ com scattered function and type definition }}
-  | dec_spec                                         :: :: reg_dec
+  | dec_spec                                           :: :: reg_dec
     {{ com register declaration }}
-  | fundef1 .. fundefn                               :: I :: internal_mutrec
+  | constraint id ( kid1 , ... , kidn ) = n_constraint :: :: constraint
+  | fundef1 .. fundefn                                 :: I :: internal_mutrec
     {{ com internal representation of mutually recursive functions }}
 
 defs :: '' ::=
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 1d0689e4..9966742e 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -329,7 +329,7 @@ let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2))
 let nc_true = mk_nc NC_true
 let nc_false = mk_nc NC_false
 
-let rec nc_negate (NC_aux (nc, _)) =
+let rec nc_negate (NC_aux (nc, l)) =
   match nc with
   | NC_bounded_ge (n1, n2) -> nc_lt n1 n2
   | NC_bounded_le (n1, n2) -> nc_gt n1 n2
@@ -343,6 +343,8 @@ let rec nc_negate (NC_aux (nc, _)) =
   | NC_set (kid, [int]) -> nc_neq (nvar kid) (nconstant int)
   | NC_set (kid, int :: ints) ->
      mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints)))))
+  | NC_app _ ->
+     raise (Reporting_basic.err_unreachable l __POS__ "tried to negate constraint with unexpanded synonym")
 
 let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown)
 
@@ -379,6 +381,10 @@ let quant_split typq =
   let qis = quant_items typq in
   List.concat (List.map qi_kopt qis), List.concat (List.map qi_nc qis)
 
+let quant_map_items f = function
+  | TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_no_forall, l)
+  | TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (List.map f qis), l)
+
 let unaux_nexp (Nexp_aux (nexp, _)) = nexp
 let unaux_order (Ord_aux (ord, _)) = ord
 let unaux_typ (Typ_aux (typ, _)) = typ
@@ -523,8 +529,8 @@ let def_loc = function
   | DEF_scattered (SD_aux (_, (l, _)))
   | DEF_reg_dec (DEC_aux (_, (l, _)))
   | DEF_fixity (_, _, Id_aux (_, l))
-  | DEF_overload (Id_aux (_, l), _) ->
-    l
+  | DEF_overload (Id_aux (_, l), _) -> l
+  | DEF_constraint (Id_aux (_, l), _, _) -> l
   | DEF_internal_mutrec _ -> Parse_ast.Unknown
 
 let string_of_id = function
@@ -638,12 +644,17 @@ and string_of_n_constraint = function
      "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
   | NC_aux (NC_set (kid, ns), _) ->
      string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
+  | NC_aux (NC_app (id, nexps), _) ->
+     "where " ^ string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_nexp nexps ^ ")"
   | NC_aux (NC_true, _) -> "true"
   | NC_aux (NC_false, _) -> "false"
 
+let string_of_kinded_id = function
+  | KOpt_aux (KOpt_none kid, _) -> string_of_kid kid
+  | KOpt_aux (KOpt_kind (k, kid), _) -> "(" ^ string_of_kid kid ^ " : " ^ string_of_kind k ^ ")"
+
 let string_of_quant_item_aux = function
-  | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid
-  | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "(" ^ string_of_kid kid ^ " :: " ^ string_of_kind k ^ ")"
+  | QI_id kopt -> string_of_kinded_id kopt
   | QI_const constr -> string_of_n_constraint constr
 
 let string_of_quant_item = function
@@ -884,6 +895,8 @@ module NC = struct
     | NC_or (nc1,nc2), NC_or (nc3,nc4)
     | NC_and (nc1,nc2), NC_and (nc3,nc4)
       -> lex_ord compare compare nc1 nc3 nc2 nc4
+    | NC_app (id1, nexps1), NC_app (id2, nexps2)
+      -> lex_ord (Id.compare) (Util.compare_list Nexp.compare) id1 id2 nexps1 nexps2
     | NC_true, NC_true
     | NC_false, NC_false
       -> 0
@@ -894,6 +907,7 @@ module NC = struct
     | NC_set _, _ -> -1        | _, NC_set _ -> 1
     | NC_or _, _ -> -1         | _, NC_or _ -> 1
     | NC_and _, _ -> -1        | _, NC_and _ -> 1
+    | NC_app _, _ -> -1        | _, NC_app _ -> 1
     | NC_true, _ -> -1         | _, NC_true -> 1
 end
 
@@ -1079,6 +1093,8 @@ let rec tyvars_of_nc (NC_aux (nc, _)) =
   | NC_or (nc1, nc2)
   | NC_and (nc1, nc2) ->
      KidSet.union (tyvars_of_nc nc1) (tyvars_of_nc nc2)
+  | NC_app (id, nexps) ->
+     List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps)
   | NC_true
   | NC_false -> KidSet.empty
 
@@ -1338,6 +1354,7 @@ let rec locate_nc l (NC_aux (nc_aux, _)) =
     | NC_set (kid, nums) -> NC_set (locate_kid l kid, nums)
     | NC_or (nc1, nc2) -> NC_or (locate_nc l nc1, locate_nc l nc2)
     | NC_and (nc1, nc2) -> NC_and (locate_nc l nc1, locate_nc l nc2)
+    | NC_app (id, nexps) -> NC_app (id, List.map (locate_nexp l) nexps)
     | NC_true -> NC_true
     | NC_false -> NC_false
   in
diff --git a/src/ast_util.mli b/src/ast_util.mli
index bbe9463e..ea287190 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -172,6 +172,7 @@ val nc_negate : n_constraint -> n_constraint
 val quant_items : typquant -> quant_item list
 val quant_kopts : typquant -> kinded_id list
 val quant_split : typquant -> kinded_id list * n_constraint list
+val quant_map_items : (quant_item -> quant_item) -> typquant -> typquant
 
 (* Functions to map over the annotations in sub-expressions *)
 val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
@@ -209,6 +210,7 @@ val string_of_typ : typ -> string
 val string_of_typ_arg : typ_arg -> string
 val string_of_typ_pat : typ_pat -> string
 val string_of_n_constraint : n_constraint -> string
+val string_of_kinded_id : kinded_id -> string
 val string_of_quant_item : quant_item -> string
 val string_of_typquant : typquant -> string
 val string_of_typschm : typschm -> string
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4e6e941d..36513ba1 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -370,6 +370,9 @@ and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint)
                 NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
              | Parse_ast.NC_and (nc1, nc2) ->
                 NC_and (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
+             | Parse_ast.NC_app (id, typs) ->
+                let nexps = List.map (to_ast_nexp k_env) typs in
+                NC_app (to_ast_id id, nexps)
              | Parse_ast.NC_true -> NC_true
              | Parse_ast.NC_false -> NC_false
     ), l)
@@ -907,6 +910,11 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
   | Parse_ast.DEF_reg_dec(dec) ->
      let d = to_ast_dec envs dec in
      ((Finished(DEF_reg_dec(d))),envs),partial_defs
+  | Parse_ast.DEF_constraint (id, kids, nc) ->
+     let id = to_ast_id id in
+     let kids = List.map to_ast_var kids in
+     let nc = to_ast_nexp_constraint k_env nc in
+     ((Finished (DEF_constraint (id, kids, nc))), envs), partial_defs
   | Parse_ast.DEF_pragma (_, _, l) ->
      typ_error l "Encountered preprocessor directive in initial check" None None None
   | Parse_ast.DEF_internal_mutrec _ ->
diff --git a/src/lexer.mll b/src/lexer.mll
index cc49073c..cbefa601 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -163,6 +163,8 @@ let kw_table =
      ("do",                      (fun _ -> Do));
      ("mutual",                  (fun _ -> Mutual));
      ("bitfield",                (fun _ -> Bitfield));
+     ("tuple",                   (fun _ -> Tuple));
+     ("where",                   (fun _ -> Where));
 
      ("barr",                    (fun x -> Barr));
      ("depend",                  (fun x -> Depend));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index a4052d82..3317c196 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -176,6 +176,7 @@ n_constraint_aux =  (* constraint over kind $_$ *)
  | NC_set of kid * (Big_int.num) list
  | NC_or of n_constraint * n_constraint
  | NC_and of n_constraint * n_constraint
+ | NC_app of id * atyp list
  | NC_true
  | NC_false
 
@@ -566,6 +567,7 @@ def =  (* Top-level definition *)
  | DEF_scattered of scattered_def (* scattered definition *)
  | DEF_reg_dec of dec_spec (* register declaration *)
  | DEF_pragma of string * string * l
+ | DEF_constraint of id * kid list * n_constraint
  | DEF_internal_mutrec of fundef list
 
 
diff --git a/src/parser.mly b/src/parser.mly
index b9aae275..070dee50 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -175,7 +175,7 @@ let rec desugar_rchain chain s e =
 
 /*Terminals with no content*/
 
-%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
+%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Tuple 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
@@ -331,6 +331,8 @@ nc_and:
     { $1 }
 
 atomic_nc:
+  | Where id Lparen typ_list Rparen
+    { mk_nc (NC_app ($2, $4)) $startpos $endpos }
   | True
     { mk_nc NC_true $startpos $endpos }
   | False
@@ -1402,6 +1404,8 @@ def:
     { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) }
   | default_def
     { DEF_default $1 }
+  | Constraint id Lparen kid_list Rparen Eq nc
+    { DEF_constraint ($2, $4, $7) }
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
   | Pragma
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 08ede660..0b0a8305 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -123,6 +123,7 @@ let doc_nc =
     | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
     | NC_set (kid, ints) ->
        separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
+    | NC_app (id, nexps) -> string "where" ^^ space ^^ doc_id id ^^ parens (separate_map (comma ^^ space) doc_nexp nexps)
     | _ -> parens (nc0 nc)
   and nc0 (NC_aux (nc_aux, _) as nc) =
     match nc_aux with
@@ -134,7 +135,7 @@ let doc_nc =
     | _ -> atomic_nc nc
   in
   nc0
-  
+
 let rec doc_typ (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
@@ -586,6 +587,8 @@ let rec doc_def def = group (match def with
   | DEF_fixity (prec, n, id) ->
      fixities := Bindings.add id (prec, Big_int.to_int n) !fixities;
      separate space [doc_prec prec; doc_int n; doc_id id]
+  | DEF_constraint (id, kids, nc) ->
+     separate space [string "constraint"; doc_id id; parens (separate_map (comma ^^ space) doc_kid kids); equals; doc_nc nc]
   | DEF_overload (id, ids) ->
      separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
   ) ^^ hardline
diff --git a/src/sail.ml b/src/sail.ml
index 9526d6fe..c1c965fe 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -237,6 +237,9 @@ let options = Arg.align ([
   ( "-dmagic_hash",
     Arg.Set Initial_check.opt_magic_hash,
     " (debug) allow special character # in identifiers");
+  ( "-Xconstraint_synonyms",
+    Arg.Set Type_check.opt_constraint_synonyms,
+    " (extension) allow constraint synonyms");
   ( "-v",
     Arg.Set opt_print_version,
     " print version");
diff --git a/src/type_check.ml b/src/type_check.ml
index e1232046..cf1d8ef9 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -69,6 +69,10 @@ let opt_no_effects = ref false
    assignments in l-expressions *)
 let opt_no_lexp_bounds_check = ref false
 
+(* opt_constraint_synonyms allows constraint synonyms as toplevel
+   definitions *)
+let opt_constraint_synonyms = ref false
+
 let depth = ref 0
 
 let rec indent n = match n with
@@ -163,6 +167,7 @@ and strip_n_constraint_aux = function
   | NC_set (kid, nums) -> NC_set (strip_kid kid, nums)
   | NC_or (nc1, nc2) -> NC_or (strip_n_constraint nc1, strip_n_constraint nc2)
   | NC_and (nc1, nc2) -> NC_and (strip_n_constraint nc1, strip_n_constraint nc2)
+  | NC_app (id, nexps) -> NC_app (strip_id id, List.map strip_nexp nexps)
   | NC_true -> NC_true
   | NC_false -> NC_false
 and strip_n_constraint = function
@@ -245,6 +250,7 @@ and nc_subst_nexp_aux l sv subst = function
      else set_nc
   | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
   | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
+  | NC_app (id, nexps) -> NC_app (id, List.map (nexp_subst sv subst) nexps)
   | NC_false -> NC_false
   | NC_true -> NC_true
 
@@ -336,6 +342,8 @@ let typquant_subst_kid_aux sv subst = function
 
 let typquant_subst_kid sv subst (TypQ_aux (typq, l)) = TypQ_aux (typquant_subst_kid_aux sv subst typq, l)
 
+let adding = Util.("Adding " |> darkgray |> clear)
+
 (**************************************************************************)
 (* 2. Environment                                                         *)
 (**************************************************************************)
@@ -378,6 +386,7 @@ module Env : sig
   val add_ret_typ : typ -> t -> t
   val add_typ_synonym : id -> (t -> typ_arg list -> typ) -> t -> t
   val get_typ_synonym : id -> t -> t -> typ_arg list -> typ
+  val add_constraint_synonym : id -> kid list -> n_constraint -> t -> t
   val add_num_def : id -> nexp -> t -> t
   val get_num_def : id -> t -> nexp
   val add_overloads : id -> id list -> t -> t
@@ -400,7 +409,11 @@ module Env : sig
   val polymorphic_undefineds : t -> bool
   val lookup_id : ?raw:bool -> id -> t -> typ lvar
   val fresh_kid : ?kid:kid -> t -> kid
+
   val expand_synonyms : t -> typ -> typ
+  val expand_constraint_synonyms : t -> n_constraint -> n_constraint
+  val expand_typquant_synonyms : t -> typquant -> typquant
+
   val canonicalize : t -> typ -> typ
   val base_typ_of : t -> typ -> typ
   val add_smt_op : id -> string -> t -> t
@@ -448,6 +461,7 @@ end = struct
       accessors : (typquant * typ) Bindings.t;
       externs : (string -> string option) Bindings.t;
       smt_ops : string Bindings.t;
+      constraint_synonyms : (kid list * n_constraint) Bindings.t;
       casts : id list;
       allow_casts : bool;
       allow_bindings : bool;
@@ -477,6 +491,7 @@ end = struct
       accessors = Bindings.empty;
       externs = Bindings.empty;
       smt_ops = Bindings.empty;
+      constraint_synonyms = Bindings.empty;
       casts = [];
       allow_bindings = true;
       allow_casts = true;
@@ -495,11 +510,11 @@ end = struct
 
   let get_typ_var kid env =
     try snd (KBindings.find kid env.typ_vars) with
-    | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid)
+    | Not_found -> typ_error (kid_loc kid) ("No type variable " ^ string_of_kid kid)
 
   let get_typ_var_loc kid env =
     try fst (KBindings.find kid env.typ_vars) with
-    | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid)
+    | Not_found -> typ_error (kid_loc kid) ("No type variable " ^ string_of_kid kid)
 
   let get_typ_vars env = KBindings.map snd env.typ_vars
   let get_typ_var_locs env = KBindings.map fst env.typ_vars
@@ -545,12 +560,12 @@ end = struct
     | Not_found -> []
 
   let add_overloads id ids env =
-    typ_print (lazy ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]"));
+    typ_print (lazy (adding ^ "overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]"));
     let existing = try Bindings.find id env.overloads with Not_found -> [] in
     { env with overloads = Bindings.add id (existing @ ids) env.overloads }
 
   let add_smt_op id str env =
-    typ_print (lazy ("Adding smt binding " ^ string_of_id id ^ " to " ^ str));
+    typ_print (lazy (adding ^ "smt binding " ^ string_of_id id ^ " to " ^ str));
     { env with smt_ops = Bindings.add id str env.smt_ops }
 
   let get_smt_op (Id_aux (_, l) as id) env =
@@ -597,8 +612,28 @@ end = struct
     then ()
     else typ_error (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
 
+  let rec expand_constraint_synonyms env (NC_aux (nc_aux, l) as nc) =
+    let expand = expand_constraint_synonyms env in
+    match nc_aux with
+    | NC_app (id, nexps) ->
+       begin
+         try
+           let kids, nc = Bindings.find id env.constraint_synonyms in
+           let nc = List.fold_left2 (fun nc kid nexp -> nc_subst_nexp kid (unaux_nexp nexp) nc) nc kids nexps in
+           expand nc
+         with Not_found -> typ_error l ("Could not expand constraint synonym in " ^ string_of_n_constraint nc)
+       end
+    | NC_and (nc1, nc2) -> NC_aux (NC_and (expand nc1, expand nc2), l)
+    | NC_or (nc1, nc2) -> NC_aux (NC_or (expand nc1, expand nc2), l)
+    | NC_true | NC_false | NC_set _ | NC_equal _ | NC_not_equal _ | NC_bounded_le _ | NC_bounded_ge _  -> nc
+
+  let expand_quant_item_synonyms env = function
+    | QI_aux (QI_id kopt, l) -> QI_aux (QI_id kopt, l)
+    | QI_aux (QI_const nc, l) -> QI_aux (QI_const (expand_constraint_synonyms env nc), l)
+
+  let expand_typquant_synonyms env = quant_map_items (expand_quant_item_synonyms env)
+
   let rec expand_synonyms env (Typ_aux (typ, l) as t) =
-    (* typ_debug (lazy ("Expanding synonyms for " ^ string_of_typ t)); *)
     match typ with
     | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l)
     | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l)
@@ -644,7 +679,7 @@ end = struct
        let kids = List.map rename_kid kids in
        let nc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid "syn#" kid)) nc) nc !rebindings in
        let typ = List.fold_left (fun typ kid -> typ_subst_nexp kid (Nexp_var (prepend_kid "syn#" kid)) typ) typ !rebindings in
-       typ_print (lazy ("Synonym existential: {" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}"));
+       typ_debug (lazy ("Synonym existential: {" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}"));
        let env = { env with constraints = nc :: env.constraints } in
        Typ_aux (Typ_exist (kids, nc, expand_synonyms env typ), l)
     | Typ_var v -> Typ_aux (Typ_var v, l)
@@ -718,7 +753,7 @@ end = struct
   (* Check if a type, order, n-expression or constraint is
      well-formed. Throws a type error if the type is badly formed. *)
   let rec wf_typ ?exs:(exs=KidSet.empty) env typ =
-    typ_debug (lazy ("Well-formed " ^ string_of_typ typ));
+    typ_debug (lazy ("well-formed " ^ string_of_typ typ));
     let (Typ_aux (typ_aux, l)) = expand_synonyms env typ in
     match typ_aux with
     | Typ_id id when bound_typ_id env id ->
@@ -755,7 +790,8 @@ end = struct
     | Typ_arg_nexp nexp -> wf_nexp ~exs:exs env nexp
     | Typ_arg_typ typ -> wf_typ ~exs:exs env typ
     | Typ_arg_order ord -> wf_order env ord
-  and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l)) =
+  and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) =
+    typ_debug (lazy ("well-formed nexp " ^ string_of_nexp nexp));
     match nexp_aux with
     | Nexp_id _ -> ()
     | Nexp_var kid when KidSet.mem kid exs -> ()
@@ -765,7 +801,7 @@ end = struct
          | BK_int -> ()
          | kind -> typ_error l ("Constraint is badly formed, "
                                 ^ string_of_kid kid ^ " has kind "
-                                ^ string_of_base_kind_aux kind ^ " but should have kind Nat")
+                                ^ string_of_base_kind_aux kind ^ " but should have kind Int")
        end
     | Nexp_constant _ -> ()
     | Nexp_app (id, nexps) ->
@@ -787,15 +823,28 @@ end = struct
                                 ^ string_of_base_kind_aux kind ^ " but should have kind Order")
        end
     | Ord_inc | Ord_dec -> ()
-  and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc, _)) =
-    match nc with
+  and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc_aux, l) as nc) =
+    typ_debug (lazy ("well-formed constraint " ^ string_of_n_constraint nc));
+    match nc_aux with
     | NC_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
     | NC_not_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
     | NC_bounded_ge (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
     | NC_bounded_le (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
-    | NC_set (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *)
+    | NC_set (kid, _) when KidSet.mem kid exs -> ()
+    | NC_set (kid, _) -> begin
+        match get_typ_var kid env with
+        | BK_int -> ()
+        | kind -> typ_error l ("Set constraint is badly formed, "
+                               ^ string_of_kid kid ^ " has kind "
+                               ^ string_of_base_kind_aux kind ^ " but should have kind Int")
+      end
     | NC_or (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
     | NC_and (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
+    | NC_app (id, nexps) ->
+       if not (Bindings.mem id env.constraint_synonyms) then
+         typ_error l ("Constraint synonym " ^ string_of_id id ^ " is not defined")
+       else ();
+       List.iter (wf_nexp ~exs:exs env) nexps
     | NC_true | NC_false -> ()
 
   let counter = ref 0
@@ -834,7 +883,8 @@ end = struct
   let rec update_val_spec id (typq, typ) env =
     begin
       let typ = expand_synonyms env typ in
-      typ_print (lazy ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind (typq, typ)));
+      let typq = expand_typquant_synonyms env typq in
+      typ_print (lazy (adding ^ "val spec " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
       let env = match typ with
         | Typ_aux (Typ_bidir (typ1, typ2), _) -> add_mapping id (typq, typ1, typ2) env
         | _ -> env
@@ -854,7 +904,7 @@ end = struct
         env
   and add_mapping id (typq, typ1, typ2) env =
     begin
-      typ_print (lazy ("Adding mapping " ^ string_of_id id));
+      typ_print (lazy (adding ^ "mapping " ^ string_of_id id));
       let forwards_id = mk_id (string_of_id id ^ "_forwards") in
       let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in
       let backwards_id = mk_id (string_of_id id ^ "_backwards") in
@@ -912,7 +962,7 @@ end = struct
     then typ_error (id_loc id) ("Cannot create enum " ^ string_of_id id ^ ", type name is already bound")
     else
       begin
-        typ_print (lazy ("Adding enum " ^ string_of_id id));
+        typ_print (lazy (adding ^ "enum " ^ string_of_id id));
         { env with enums = Bindings.add id (IdSet.of_list ids) env.enums }
       end
 
@@ -930,7 +980,7 @@ end = struct
     then typ_error (id_loc id) ("Cannot create record " ^ string_of_id id ^ ", type name is already bound")
     else
       begin
-        typ_print (lazy ("Adding record " ^ string_of_id id));
+        typ_print (lazy (adding ^ "record " ^ string_of_id id));
         let rec record_typ_args = function
           | [] -> []
           | ((QI_aux (QI_id kopt, _)) :: qis) when is_nat_kopt kopt ->
@@ -947,7 +997,7 @@ end = struct
         in
         let fold_accessors accs (typ, fid) =
           let acc_typ = mk_typ (Typ_fn ([rectyp], typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
-          typ_print (lazy (indent 1 ^ "Adding accessor " ^ string_of_id id ^ "." ^ string_of_id fid ^ " :: " ^ string_of_bind (typq, acc_typ)));
+          typ_print (lazy (indent 1 ^ adding ^ "accessor " ^ string_of_id id ^ "." ^ string_of_id fid ^ " :: " ^ string_of_bind (typq, acc_typ)));
           Bindings.add (field_name id fid) (typq, acc_typ) accs
         in
         { env with records = Bindings.add id (typq, fields) env.records;
@@ -987,19 +1037,19 @@ end = struct
       if Bindings.mem id env.top_val_specs then
         typ_error (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name")
       else ();
-      typ_print (lazy ("Adding local binding " ^ string_of_id id ^ " :: " ^ string_of_mtyp mtyp));
+      typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp));
       { env with locals = Bindings.add id mtyp env.locals }
     end
 
   let add_variant id variant env =
     begin
-      typ_print (lazy ("Adding variant " ^ string_of_id id));
+      typ_print (lazy (adding ^ "variant " ^ string_of_id id));
       { env with variants = Bindings.add id variant env.variants }
     end
 
   let add_union_id id bind env =
     begin
-      typ_print (lazy ("Adding union identifier binding " ^ string_of_id id ^ " :: " ^ string_of_bind bind));
+      typ_print (lazy (adding ^ "union identifier " ^ string_of_id id ^ " : " ^ string_of_bind bind));
       { env with union_ids = Bindings.add id bind env.union_ids }
     end
 
@@ -1008,7 +1058,7 @@ end = struct
     | Not_found -> fun typ -> typ
 
   let add_flow id f env =
-    typ_print (lazy ("Adding flow constraints for " ^ string_of_id id));
+    typ_print (lazy (adding ^ "flow constraints for " ^ string_of_id id));
     { env with flow = Bindings.add id (fun typ -> f (get_flow id env typ)) env.flow }
 
   let remove_flow id env =
@@ -1046,7 +1096,7 @@ end = struct
     then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound")
     else
       begin
-        typ_print (lazy ("Adding register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ));
+        typ_print (lazy (adding ^ "register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ));
         { env with registers = Bindings.add id (reff, weff, typ) env.registers }
       end
 
@@ -1072,10 +1122,10 @@ end = struct
 
   let add_typ_var l kid k env =
     if KBindings.mem kid env.typ_vars
-    then typ_error (kid_loc kid) ("Kind identifier " ^ string_of_kid kid ^ " is already bound")
+    then typ_error (kid_loc kid) ("type variable " ^ string_of_kid kid ^ " is already bound")
     else
       begin
-        typ_print (lazy ("Adding kind identifier " ^ string_of_kid kid ^ " :: " ^ string_of_base_kind_aux k));
+        typ_print (lazy (adding ^ "type variable " ^ string_of_kid kid ^ " : " ^ string_of_base_kind_aux k));
         { env with typ_vars = KBindings.add kid (l, k) env.typ_vars }
       end
 
@@ -1084,7 +1134,7 @@ end = struct
     then typ_error (id_loc id) ("Num identifier " ^ string_of_id id ^ " is already bound")
     else
       begin
-        typ_print (lazy ("Adding Num identifier " ^ string_of_id id ^ " :: " ^ string_of_nexp nexp));
+        typ_print (lazy (adding ^ "Num identifier " ^ string_of_id id ^ " : " ^ string_of_nexp nexp));
         { env with num_defs = Bindings.add id nexp env.num_defs }
       end
 
@@ -1099,7 +1149,8 @@ end = struct
     match nc_aux with
     | NC_true -> env
     | _ ->
-       typ_print (lazy ("Adding constraint " ^ string_of_n_constraint constr));
+       let constr = expand_constraint_synonyms env constr in
+       typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr));
        { env with constraints = constr :: env.constraints }
 
   let get_ret_typ env = env.ret_typ
@@ -1114,7 +1165,7 @@ end = struct
   let no_bindings env = { env with allow_bindings = false }
 
   let add_cast cast env =
-    typ_print (lazy ("Adding cast " ^ string_of_id cast));
+    typ_print (lazy (adding ^ "cast " ^ string_of_id cast));
     { env with casts = cast :: env.casts }
 
   let add_typ_synonym id synonym env =
@@ -1122,12 +1173,22 @@ end = struct
     then typ_error (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists")
     else
       begin
-        typ_print (lazy ("Adding type synonym " ^ string_of_id id));
+        typ_print (lazy (adding ^ "type synonym " ^ string_of_id id));
         { env with typ_synonyms = Bindings.add id synonym env.typ_synonyms }
       end
 
   let get_typ_synonym id env = Bindings.find id env.typ_synonyms
 
+  let add_constraint_synonym id kids nc env =
+    if Bindings.mem id env.constraint_synonyms
+    then typ_error (id_loc id) ("Constraint synonym " ^ string_of_id id ^ " already exists")
+    else
+      begin
+        typ_print (lazy (adding ^ "constraint synonym " ^ string_of_id id));
+        wf_constraint ~exs:(KidSet.of_list kids) env nc;
+        { env with constraint_synonyms = Bindings.add id (kids, nc) env.constraint_synonyms }
+      end
+
   let get_default_order env =
     match env.default_order with
     | None -> typ_error Parse_ast.Unknown ("No default order has been set")
@@ -1186,6 +1247,10 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t =
   | TypQ_aux (TypQ_no_forall, _) -> env
   | TypQ_aux (TypQ_tq quants, _) -> List.fold_left add_quant_item env quants
 
+let expand_bind_synonyms l env (typq, typ) =
+  Env.expand_typquant_synonyms env typq, Env.expand_synonyms (add_typquant l typq env) typ
+
+
 (* Create vectors with the default order from the environment *)
 
 let default_order_error_string =
@@ -1356,6 +1421,7 @@ let rec nc_constraint env var_of (NC_aux (nc, l)) =
                     (List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant i)) ints)
   | NC_or (nc1, nc2) -> Constraint.disj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2)
   | NC_and (nc1, nc2) -> Constraint.conj (nc_constraint env var_of nc1) (nc_constraint env var_of nc2)
+  | NC_app (id, nexps) -> raise (Reporting_basic.err_unreachable l __POS__ "constraint synonym reached smt generation")
   | NC_false -> Constraint.literal false
   | NC_true -> Constraint.literal true
 
@@ -2034,7 +2100,6 @@ let rec instantiate_quants quants kid uvar = match quants with
           if is_typ_kid kid kinded_id
           then instantiate_quants quants kid uvar
           else quant :: instantiate_quants quants kid uvar
-       | _ -> typ_error Parse_ast.Unknown "Cannot instantiate quantifier"
      end
   | ((QI_aux (QI_const nc, l)) :: quants) ->
      begin
@@ -2307,7 +2372,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
             let checked_msg = crule check_exp env assert_msg string_typ in
             let env = match assert_constraint env true constr_exp with
               | Some nc ->
-                 typ_print (lazy ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert"));
+                 typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint nc ^ " for assert"));
                  Env.add_constraint nc env
               | None -> env
             in
@@ -2739,7 +2804,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
        let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with
          | Typ_tup typs -> typs
          | _ -> [typ]
-       in       
+       in
        match Env.expand_synonyms env ctor_typ with
        | Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _) ->
           begin
@@ -4382,31 +4447,26 @@ let check_mapdef env (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _)) as md
    context. We have to destructure the various kinds of val specs, but
    the difference is irrelevant for the typechecker. *)
 let check_val_spec env (VS_aux (vs, (l, _))) =
-  let annotate vs typ eff = DEF_spec (VS_aux (vs, (l, Some ((env,typ,eff), None)))) in
-  let (id, quants, typ, env) = match vs with
-    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _) as typschm, id, ext_opt, is_cast) ->
-       typ_debug (lazy ("VS typschm: " ^ string_of_id id ^ ", " ^ string_of_typschm typschm));
+  let annotate vs typ eff = DEF_spec (VS_aux (vs, (l, Some ((env, typ, eff), None)))) in
+  let vs, id, typq, typ, env = match vs with
+    | VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l) as typschm, id, ext_opt, is_cast) ->
+       typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm));
        let env = match (ext_opt "smt", ext_opt "#") with
          | Some op, None -> Env.add_smt_op id op env
          | _, _ -> env
        in
-       Env.wf_typ (add_typquant l quants env) typ;
-       typ_debug (lazy "CHECKED WELL-FORMED VAL SPEC");
-       let env =
-       (* match ext_opt with
-         | None -> env
-         | Some ext -> *)
-         Env.add_extern id ext_opt env
-       in
+       let env = Env.add_extern id ext_opt env in
        let env = if is_cast then Env.add_cast id env else env in
-       (id, quants, typ, env)
+       let typq, typ = expand_bind_synonyms ts_l env (typq, typ) in
+       let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in
+       (vs, id, typq, typ, env)
   in
   let eff =
     match typ with
-    | Typ_aux (Typ_fn (_,_,eff),_) -> eff
+    | Typ_aux (Typ_fn (_, _, eff), _) -> eff
     | _ -> no_effect
   in
-  [annotate vs typ eff], Env.add_val_spec id (quants, Env.expand_synonyms (add_typquant l quants env) typ) env
+  [annotate vs typ eff], Env.add_val_spec id (typq, typ) env
 
 let check_default env (DT_aux (ds, l)) =
   match ds with
@@ -4521,6 +4581,10 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t =
   | DEF_fixity (prec, n, op) -> [DEF_fixity (prec, n, op)], env
   | DEF_fundef fdef -> check_fundef env fdef
   | DEF_mapdef mdef -> check_mapdef env mdef
+  | DEF_constraint (id, kids, nc) when !opt_constraint_synonyms ->
+     [], Env.add_constraint_synonym id kids nc env
+  | DEF_constraint (id, _, _) ->
+     typ_error (id_loc id) "Use -Xconstraint_synonyms to enable constraint synonyms"
   | DEF_internal_mutrec fdefs ->
      let defs = List.concat (List.map (fun fdef -> fst (check_fundef env fdef)) fdefs) in
      let split_fundef (defs, fdefs) def = match def with
diff --git a/src/type_check.mli b/src/type_check.mli
index 4fe6711c..8d2b02a9 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -67,6 +67,10 @@ val opt_no_effects : bool ref
    assignments in l-expressions. *)
 val opt_no_lexp_bounds_check : bool ref
 
+(** [opt_constraint_synonyms] allows constraint synonyms as toplevel
+   definitions *)
+val opt_constraint_synonyms : bool ref
+
 (** {2 Type errors} *)
 
 type type_error =
diff --git a/src/util.ml b/src/util.ml
index b54c13d4..e0366fe7 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -408,6 +408,7 @@ let termcode n =
 
 let bold str = termcode 1 ^ str
 
+let darkgray str = termcode 90 ^ str
 let red str = termcode 91 ^ str
 let green str = termcode 92 ^ str
 let yellow str = termcode 93 ^ str
diff --git a/src/util.mli b/src/util.mli
index bb7aa70d..eb4b4bd2 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -239,6 +239,7 @@ val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list)
 (* Terminal color codes *)
 val termcode : int -> string
 val bold : string -> string
+val darkgray : string -> string
 val green : string -> string
 val red : string -> string
 val red_bg : string -> string
diff --git a/test/typecheck/pass/constraint_sym.sail b/test/typecheck/pass/constraint_sym.sail
new file mode 100644
index 00000000..6d212e40
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v1.expect b/test/typecheck/pass/constraint_sym/v1.expect
new file mode 100644
index 00000000..71fd6f30
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v1.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v1.sail", line 3, character 23 to line 3, character 24
+
+constraint Size('n) = 'm in {32, 64}
+
+No type variable 'm
diff --git a/test/typecheck/pass/constraint_sym/v1.sail b/test/typecheck/pass/constraint_sym/v1.sail
new file mode 100644
index 00000000..4421ee77
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v1.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'm in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v2.expect b/test/typecheck/pass/constraint_sym/v2.expect
new file mode 100644
index 00000000..58a0f416
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v2.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v2.sail", line 7, character 22 to line 7, character 34
+
+val foo : forall 'n, where Siz('n). int('n) -> unit
+
+Constraint synonym Siz is not defined
diff --git a/test/typecheck/pass/constraint_sym/v2.sail b/test/typecheck/pass/constraint_sym/v2.sail
new file mode 100644
index 00000000..1d98e3e4
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v2.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Siz('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v3.expect b/test/typecheck/pass/constraint_sym/v3.expect
new file mode 100644
index 00000000..ab4526dc
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v3.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v3.sail", line 7, character 42 to line 7, character 43
+
+val foo : forall ('n : Type), where Size('n). int('n) -> unit
+
+Constraint is badly formed, 'n has kind Type but should have kind Int
diff --git a/test/typecheck/pass/constraint_sym/v3.sail b/test/typecheck/pass/constraint_sym/v3.sail
new file mode 100644
index 00000000..886acbe4
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v3.sail
@@ -0,0 +1,7 @@
+$option -Xconstraint_synonyms
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall ('n : Type), where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/constraint_sym/v4.expect b/test/typecheck/pass/constraint_sym/v4.expect
new file mode 100644
index 00000000..c8374baf
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v4.expect
@@ -0,0 +1,5 @@
+Type error at file "constraint_sym/v4.sail", line 2, character 12 to line 2, character 15
+
+constraint Size('n) = 'n in {32, 64}
+
+Use -Xconstraint_synonyms to enable constraint synonyms
diff --git a/test/typecheck/pass/constraint_sym/v4.sail b/test/typecheck/pass/constraint_sym/v4.sail
new file mode 100644
index 00000000..96bf5e82
--- /dev/null
+++ b/test/typecheck/pass/constraint_sym/v4.sail
@@ -0,0 +1,6 @@
+
+constraint Size('n) = 'n in {32, 64}
+
+constraint Nat('n) = 'n >= 0
+
+val foo : forall 'n, where Size('n). int('n) -> unit
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index 8014f88a..c7e06dc7 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -2,4 +2,4 @@ Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, ch
 
 val test : forall 'size. atom('size) -> unit
 
-Kind identifier 'size is already bound
+type variable 'size is already bound
-- 
cgit v1.2.3