Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2

19 files changed, 202 insertions, 71 deletions

diff --git a/aarch64/main.sail b/aarch64/main.sail
index b48f84d9..eaaf4f7f 100644
--- a/aarch64/main.sail
+++ b/aarch64/main.sail
@@ -1,12 +1,14 @@
-val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+$include <elf.sail>
 
-function fetch_and_execute () = while true do {
-  let instr = aget_Mem(_PC, 4, AccType_IFETCH);
-  decode(instr);
-  if __BranchTaken then __BranchTaken = false else _PC = _PC + 4
-}
+// Simple top level fetch and execute loop.
+val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
 
-val elf_entry = "Elf_loader.elf_entry" : unit -> int
+function fetch_and_execute () =
+  while true do {
+    let instr = aget_Mem(_PC, 4, AccType_IFETCH);
+    decode(instr);
+    if __BranchTaken then __BranchTaken = false else _PC = _PC + 4
+  }
 
 val main : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
 
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index da98b495..ab916e27 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -1,25 +1,12 @@
 default Order dec
 
+$include <smt.sail>
+$include <flow.sail>
+
 type bits ('n : Int) = vector('n, dec, bit)
 
 infix 4 ==
 
-val div = {
-  smt : "div",
-  lem : "integerDiv"
-} : forall 'n 'm. (atom('n), atom('m)) -> atom(div('n, 'm))
-
-val mod = {
-  smt : "mod",
-  lem : "integerMod"
-} : forall 'n 'm. (atom('n), atom('m)) -> atom(mod('n, 'm))
-
-val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool
-
 val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
 
 val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
@@ -86,16 +73,10 @@ val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('
 
 overload append = {bitvector_concat, vector_concat}
 
-val not_bool = "not" : bool -> bool
-
 val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n)
 
 overload ~ = {not_bool, not_vec}
 
-val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-function neq_atom (x, y) = not_bool(eq_atom(x, y))
-
 val neq_int = {lem: "neq"} : (int, int) -> bool
 
 function neq_int (x, y) = not_bool(eq_int(x, y))
@@ -110,8 +91,6 @@ function neq_anything (x, y) = not_bool(x == y)
 
 overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
 
-val and_bool = "and_bool" : (bool, bool) -> bool
-
 val builtin_and_vec = {ocaml: "and_vec", lem: "Sail_operators.and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -120,8 +99,6 @@ function and_vec (xs, ys) = builtin_and_vec(xs, ys)
 
 overload operator & = {and_bool, and_vec}
 
-val or_bool = "or_bool" : (bool, bool) -> bool
-
 val builtin_or_vec = {ocaml: "or_vec", lem: "Sail_operators.or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -263,7 +240,7 @@ val abs_int = "abs_int" : int -> int
 
 val abs_real = "abs_real" : real -> real
 
-overload abs = {abs_int, abs_real}
+overload abs = {abs, abs_int, abs_real}
 
 val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat
 
diff --git a/lib/_tags b/lib/_tags
index b1a8186f..916a546b 100644
--- a/lib/_tags
+++ b/lib/_tags
@@ -1,2 +1,2 @@
-<*.m{l,li}>: package(lem), package(linksem), package(zarith), package(uint)
-<main.native>: package(lem), package(linksem), package(zarith), package(uint)
\ No newline at end of file
+<*.m{l,li}>: package(lem), package(linksem), package(zarith)
+<main.native>: package(lem), package(linksem), package(zarith)
\ No newline at end of file
diff --git a/lib/elf.sail b/lib/elf.sail
new file mode 100644
index 00000000..f158fbad
--- /dev/null
+++ b/lib/elf.sail
@@ -0,0 +1,8 @@
+$ifndef _ELF
+$define _ELF
+
+val elf_entry = "Elf_loader.elf_entry" : unit -> int
+
+val elf_tohost = "Elf_loader.elf_tohost" : unit -> int
+
+$endif
diff --git a/lib/flow.sail b/lib/flow.sail
new file mode 100644
index 00000000..cb7b1b99
--- /dev/null
+++ b/lib/flow.sail
@@ -0,0 +1,42 @@
+$ifndef _FLOW
+$define _FLOW
+
+val not_bool = "not" : bool -> bool
+val and_bool = "and_bool" : (bool, bool) -> bool
+val or_bool = "or_bool" : (bool, bool) -> bool
+
+val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+function neq_atom (x, y) = not_bool(eq_atom(x, y))
+
+val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lt_atom = "lt"     : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gt_atom = "gt"     : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+val lt_range_atom = "lt"     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val lteq_range_atom = "lteq" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val gt_range_atom = "gt"     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val gteq_range_atom = "gteq" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val lt_atom_range = "lt"     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+val lteq_atom_range = "lteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+val gt_atom_range = "gt"     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+val gteq_atom_range = "gteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+
+$ifdef TEST
+
+val __flow_test : forall 'n 'm. (atom('n), atom('m)) -> unit
+
+function __flow_test (x, y) = {
+  if lteq_atom(x, y) then {
+    _prove(constraint('n <= 'm))
+  } else {
+    _prove(constraint('n > 'm))
+  }
+}
+
+$endif
+
+$endif
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index fd1d1b23..a69dc379 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -122,3 +122,10 @@ function UInt_slice(xs,i,l) = {
   let xs = (xs & slice_mask(i,l)) >> i in
   UInt(xs)
 }
+
+val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure
+
+function zext_ones(m) = {
+  let v : bits('n) = extsv(0b1) in
+  v >> ('n - m)
+}
diff --git a/lib/smt.sail b/lib/smt.sail
new file mode 100644
index 00000000..702b82c6
--- /dev/null
+++ b/lib/smt.sail
@@ -0,0 +1,30 @@
+$ifndef _SMT
+$define _SMT
+
+// see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
+
+val div = {
+  smt: "div",
+  ocaml: "quotient",
+  lem: "integerDiv"
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
+
+val mod = {
+  smt: "mod",
+  ocaml: "modulus",
+  lem: "integerMod"
+} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
+
+val abs = {
+  smt : "abs",
+  ocaml: "abs_int",
+  lem: "abs_int"
+} : forall 'n. atom('n) -> {'o, 'o = abs('n). atom('o)}
+
+$ifdef TEST
+
+let __smt_x : atom(div(4, 2)) = div(8, 4)
+
+$endif
+
+$endif
diff --git a/riscv/Makefile b/riscv/Makefile
new file mode 100644
index 00000000..fabaaafc
--- /dev/null
+++ b/riscv/Makefile
@@ -0,0 +1,24 @@
+SAIL_SRCS = prelude.sail riscv_types.sail riscv.sail
+SAIL_DIR ?= $(realpath ..)
+
+export SAIL_DIR
+
+all: riscv Riscv_embed_sequential.thy
+
+riscv: $(SAIL_SRCS) main.sail
+	$(SAIL_DIR)/sail -ocaml -o riscv $^
+
+Riscv_embed_sequential.thy: riscv_embed_sequential.lem riscv_extras_embed_sequential.lem
+	lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
+		riscv_extras_embed_sequential.lem \
+		riscv_embed_types_sequential.lem \
+		riscv_embed_sequential.lem
+
+riscv_embed_sequential.lem: $(SAIL_SRCS)
+	$(SAIL_DIR)/sail -lem -o riscv -lem_sequential -lem_mwords -lem_lib Riscv_extras_embed $^
+
+clean:
+	-rm -rf riscv _sbuild
+	-rm -f riscv_embed_sequential.lem riscv_embed_types_sequential.lem
+	-rm -f Riscv_embed_sequential.thy Riscv_embed_types_sequential.thy \
+		Riscv_extras_embed_sequential.thy
diff --git a/src/Makefile b/src/Makefile
index 325cbec6..85c5abba 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -270,4 +270,4 @@ doc:
 	ocamlbuild -use-ocamlfind sail.docdir/index.html
 
 lib:
-	ocamlbuild pretty_print.cmxa pretty_print.cma
+	ocamlbuild -use-ocamlfind pretty_print.cmxa pretty_print.cma
diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index feacdf3d..83c36821 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -118,9 +118,9 @@ let load_segment seg =
 let load_elf name =
   let segments, e_entry, symbol_map = read name in
   opt_elf_entry := e_entry;
-  if List.mem_assoc "tohost" symbol_map then
-    let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in
-    opt_elf_tohost := tohost_addr;
+  (if List.mem_assoc "tohost" symbol_map then
+     let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in
+     opt_elf_tohost := tohost_addr);
   List.iter load_segment segments
 
 (* The sail model can access this by externing a unit -> int function
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 8533827b..bb56c8a9 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -727,7 +727,7 @@ let initial_system_state_of_elf_file name =
            aarch64_register_data_all) *)
         | 8 (* EM_MIPS *) ->
           let startaddr =
-            let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+            let e_entry = Uint64_wrapper.of_bigint e_entry in
             match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
             | Error.Fail s -> failwith "Failed computing entry point"
             | Error.Success s -> s
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 46bc92fb..3d187aa9 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name =
         match Nat_big_num.to_int e_machine with
         | 8 (* EM_MIPS *) ->
           let startaddr =
-            let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+            let e_entry = Uint64_wrapper.of_bigint e_entry in
             match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
             | Error.Fail s -> failwith "Failed computing entry point"
             | Error.Success s -> s
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
index 5e5bee21..6b12ebbb 100644
--- a/src/lem_interp/run_with_elf_cheri128.ml
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name =
         match Nat_big_num.to_int e_machine with
         | 8 (* EM_MIPS *) ->
           let startaddr =
-            let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+            let e_entry = Uint64_wrapper.of_bigint e_entry in
             match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
             | Error.Fail s -> failwith "Failed computing entry point"
             | Error.Success s -> s
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 2e7ad08f..0baaf139 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -899,7 +899,8 @@ let rec freshen_pat_bindings p =
 (* Use the location pairs in choices to reduce case expressions at the first
    location to the given case at the second. *)
 let apply_pat_choices choices =
-  let rewrite_constraint (NC_aux (nc,l) as nconstr) =
+  let rewrite_constraint (NC_aux (nc,l) as nconstr) = E_constraint nconstr (*
+    Not right now - false cases may not type check
     match List.assoc l choices with
     | choice,_ -> begin
        match nc with
@@ -907,7 +908,7 @@ let apply_pat_choices choices =
           E_constraint (NC_aux ((if choice < List.length is then NC_true else NC_false), Generated l))
        | _ -> E_constraint nconstr
     end
-    | exception Not_found -> E_constraint nconstr
+    | exception Not_found -> E_constraint nconstr*)
   in
   let rewrite_case (e,cases) =
     match List.assoc (exp_loc e) choices with
@@ -1504,11 +1505,16 @@ let split_defs continue_anyway splits defs =
            | Some (Some (pats,l)) ->
               Some (List.mapi (fun i p ->
                 match p with
-                | P_aux (P_lit lit,_) when (match lit with L_aux (L_undef,_) -> false | _ -> true) ->
-                   p,[id,E_aux (E_lit lit,(Generated Unknown,None))],[l,(i,[])]
+                | P_aux (P_lit lit,(pl,pannot))
+                    when (match lit with L_aux (L_undef,_) -> false | _ -> true) ->
+                   p,[id,E_aux (E_lit lit,(Generated pl,pannot))],[l,(i,[])]
                 | _ ->
                    let p',subst = freshen_pat_bindings p in
-                   P_aux (P_as (p',id),(l,annot)),[],[l,(i,subst)])
+                   match p' with
+                   | P_aux (P_wild,_) ->
+                      P_aux (P_id id,(l,annot)),[],[l,(i,subst)]
+                   | _ ->
+                      P_aux (P_as (p',id),(l,annot)),[],[l,(i,subst)])
                       pats)
            )
         | P_app (id,ps) ->
@@ -2226,6 +2232,7 @@ let merge rs rs' = {
 }
 
 type env = {
+  top_kids : kid list;
   var_deps : dependencies Bindings.t;
   kid_deps : dependencies KBindings.t
 }
@@ -2248,7 +2255,7 @@ let update_env env deps pat =
   let var_deps = List.fold_left (fun ds v -> Bindings.add v deps ds) env.var_deps bound in
   let kbound = kids_bound_by_pat pat in
   let kid_deps = KidSet.fold (fun v ds -> KBindings.add v deps ds) kbound env.kid_deps in
-  { var_deps = var_deps; kid_deps = kid_deps }
+  { env with var_deps = var_deps; kid_deps = kid_deps }
 
 let assigned_vars_exps es =
   List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp))
@@ -2384,6 +2391,18 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps =
      | None -> None)
   | _ -> None
 
+let simplify_size_nexp env typ_env (Nexp_aux (ne,l) as nexp) =
+  let is_equal kid =
+    prove typ_env (NC_aux (NC_equal (Nexp_aux (Nexp_var kid,Unknown), nexp),Unknown))
+  in
+  match ne with
+  | Nexp_var _
+  | Nexp_constant _ -> nexp
+  | _ ->
+     match List.find is_equal env.top_kids with
+     | kid -> Nexp_aux (Nexp_var kid,Generated l)
+     | exception Not_found -> nexp
+
 (* Takes an environment of dependencies on vars, type vars, and flow control,
    and dependencies on mutable variables.  The latter are quite conservative,
    we currently drop variables assigned inside loops, for example. *)
@@ -2600,6 +2619,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
        let typ = Env.expand_synonyms tenv typ in
        if is_bitvector_typ typ then
          let _,size,_,_ = vector_typ_args_of typ in
+         let size = simplify_size_nexp env tenv size in
          match deps_of_nexp env.kid_deps [] size with
          | Have (args,caller,caller_kids) ->
             { r with
@@ -2664,8 +2684,8 @@ let initial_env fn_id (TypQ_aux (tq,_)) pat set_assertions =
        (match KBindings.find kid set_assertions with
        | (l,is) ->
           let l' = Generated l in
-          let pats = List.map (fun n -> P_aux (P_lit (L_aux (L_num n,l')),(l',None))) is in
-          let pats = pats @ [P_aux (P_wild,(l',None))] in
+          let pats = List.map (fun n -> P_aux (P_lit (L_aux (L_num n,l')),(l',snd annot))) is in
+          let pats = pats @ [P_aux (P_wild,(l',snd annot))] in
           Partial (pats,l)
        | exception Not_found -> Total)
     | _ -> Total
@@ -2736,7 +2756,8 @@ let initial_env fn_id (TypQ_aux (tq,_)) pat set_assertions =
   let _,var_deps,kid_deps = split3 (List.mapi arg pats) in
   let var_deps = List.fold_left dep_bindings_merge Bindings.empty var_deps in
   let kid_deps = List.fold_left dep_kbindings_merge kid_quant_deps kid_deps in
-  { var_deps = var_deps; kid_deps = kid_deps }
+  let top_kids = List.map fst (KBindings.bindings kid_quant_deps) in
+  { top_kids = top_kids; var_deps = var_deps; kid_deps = kid_deps }
 
 (* When there's more than one pick the first *)
 let merge_set_asserts _ x y =
@@ -3059,6 +3080,10 @@ let rewrite_app env typ (id,args) =
         when is_slice slice1 && not (is_constant length1) ->
        E_app (mk_id "zext_slice", [vector1; start1; length1])
 
+    | [E_aux (E_app (ones, [len1]),_);
+       _ (* unnecessary ZeroExtend length *)] ->
+       E_app (mk_id "zext_ones", [len1])
+
     | _ -> E_app (id,args)
 
   else if is_id env (Id "SignExtend") id then
@@ -3099,15 +3124,23 @@ type options = {
   debug_analysis : int;
   rewrites : bool;
   rewrite_size_parameters : bool;
-  all_split_errors : bool
+  all_split_errors : bool;
+  dump_raw: bool
 }
 
+let recheck defs =
+  let w = !Util.opt_warnings in
+  let () = Util.opt_warnings := false in
+  let r = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in
+  let () = Util.opt_warnings := w in
+  r
+
 let monomorphise opts splits env defs =
   let (defs,env) =
     if opts.rewrites then
       let defs = MonoRewrites.mono_rewrite defs in
     (* TODO: is this necessary? *)
-      Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs
+      recheck defs
     else (defs,env)
   in
 (*let _ = Pretty_print.pp_defs stdout defs in*)
@@ -3121,9 +3154,12 @@ let monomorphise opts splits env defs =
   (* TODO: currently doing this because constant propagation leaves numeric literals as
      int, try to avoid this later; also use final env for DEF_spec case above, because the
      type checker doesn't store the env at that point :( *)
-  if opts.rewrite_size_parameters then
-    let (defs,env) = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in
-    let defs = AtomToItself.rewrite_size_parameters env defs in
-    defs
-  else
-    defs
+  let defs = if opts.rewrite_size_parameters then
+      let (defs,env) = recheck defs in
+      let defs = AtomToItself.rewrite_size_parameters env defs in
+      defs
+    else
+      defs
+  in
+  let () = if opts.dump_raw then Pretty_print_sail.pp_defs stdout defs else () in
+  recheck defs
diff --git a/src/monomorphise.mli b/src/monomorphise.mli
index 8e0c1ede..11713511 100644
--- a/src/monomorphise.mli
+++ b/src/monomorphise.mli
@@ -53,7 +53,8 @@ type options = {
   debug_analysis : int;           (* Debug output level for the automatic analysis *)
   rewrites : bool;                (* Experimental rewrites for variable-sized operations *)
   rewrite_size_parameters : bool; (* Make implicit type parameters explicit for (e.g.) lem *)
-  all_split_errors : bool
+  all_split_errors : bool;
+  dump_raw: bool
 }
 
 val monomorphise :
@@ -61,4 +62,4 @@ val monomorphise :
   ((string * int) * string) list -> (* List of splits from the command line *)
   Type_check.Env.t ->
   Type_check.tannot Ast.defs ->
-  Type_check.tannot Ast.defs
+  Type_check.tannot Ast.defs * Type_check.Env.t
diff --git a/src/process_file.ml b/src/process_file.ml
index cb8c8011..1ba8069f 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -196,12 +196,10 @@ let monomorphise_ast locs type_env ast =
     debug_analysis = !opt_dmono_analysis;
     rewrites = !opt_mono_rewrites;
     rewrite_size_parameters = !Pretty_print_lem.opt_mwords;
-    all_split_errors = !opt_dall_split_errors
+    all_split_errors = !opt_dall_split_errors;
+    dump_raw = !opt_ddump_raw_mono_ast
   } in
-  let ast = monomorphise opts locs type_env ast in
-  let () = if !opt_ddump_raw_mono_ast then Pretty_print_sail.pp_defs stdout ast else () in
-  let ienv = Type_check.Env.no_casts Type_check.initial_env in
-  Type_check.check ienv ast
+  monomorphise opts locs type_env ast
 
 let open_output_with_check file_name =
   let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
diff --git a/src/type_check.ml b/src/type_check.ml
index 41438592..a49807ce 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2020,6 +2020,12 @@ let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) -
 let strip_pexp : 'a pexp -> unit pexp = function pexp -> map_pexp_annot (fun (l, _) -> (l, ())) pexp
 let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l, _) -> (l, ())) lexp
 
+let fresh_var =
+  let counter = ref 0 in
+  fun () -> let n = !counter in
+            let () = counter := n+1 in
+            mk_id ("v#" ^ string_of_int n)
+
 let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ_aux, _) as typ) : tannot exp =
   let annot_exp_effect exp typ eff = E_aux (exp, (l, Some (env, typ, eff))) in
   let add_effect exp eff = match exp with
@@ -2470,8 +2476,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
      | exception (Type_error _ as typ_exn) ->
         match pat_aux with
         | P_lit lit ->
-           let guard = mk_exp (E_app_infix (mk_exp (E_id (mk_id "p#")), mk_id "==", mk_exp (E_lit lit))) in
-           let (typed_pat, env, guards) = bind_pat env (mk_pat (P_id (mk_id "p#"))) typ in
+           let var = fresh_var () in
+           let guard = mk_exp (E_app_infix (mk_exp (E_id var), mk_id "==", mk_exp (E_lit lit))) in
+           let (typed_pat, env, guards) = bind_pat env (mk_pat (P_id var)) typ in
            typed_pat, env, guard::guards
         | _ -> raise typ_exn
 
diff --git a/test/lem/run_tests.sh b/test/lem/run_tests.sh
index 5d435950..c53ec189 100755
--- a/test/lem/run_tests.sh
+++ b/test/lem/run_tests.sh
@@ -61,6 +61,6 @@ do
     fi
 done
 
-finish_suite "Expecting pass"
+finish_suite "LEM tests"
 
 printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/riscv/run_tests.sh b/test/riscv/run_tests.sh
index 9f1aa007..32f6f091 100755
--- a/test/riscv/run_tests.sh
+++ b/test/riscv/run_tests.sh
@@ -1,4 +1,3 @@
-
 #!/usr/bin/env bash
 set -e