Merge branch 'sail2' into rmem_interpreter

1 files changed, 876 insertions, 0 deletions

diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
new file mode 100644
index 00000000..33b67008
--- /dev/null
+++ b/src/constant_propagation.ml
@@ -0,0 +1,876 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Spec_analysis
+open Type_check
+
+(* COULD DO: dead code is only eliminated at if expressions, but we could
+   also cut out impossible case branches and code after assertions. *)
+
+(* Constant propogation.
+   Takes maps of immutable/mutable variables to subsitute.
+   The substs argument also contains the current type-level kid refinements
+   so that we can check for dead code.
+   Extremely conservative about evaluation order of assignments in
+   subexpressions, dropping assignments rather than committing to
+   any particular order *)
+
+
+let kbindings_from_list = List.fold_left (fun s (v,i) -> KBindings.add v i s) KBindings.empty
+let bindings_from_list = List.fold_left (fun s (v,i) -> Bindings.add v i s) Bindings.empty
+(* union was introduced in 4.03.0, a bit too recently *)
+let bindings_union s1 s2 =
+  Bindings.merge (fun _ x y -> match x,y with
+  |  _, (Some x) -> Some x
+  |  (Some x), _ -> Some x
+  |  _,  _ -> None) s1 s2
+let kbindings_union s1 s2 =
+  KBindings.merge (fun _ x y -> match x,y with
+  |  _, (Some x) -> Some x
+  |  (Some x), _ -> Some x
+  |  _,  _ -> None) s1 s2
+
+let rec list_extract f = function
+  | [] -> None
+  | h::t -> match f h with None -> list_extract f t | Some v -> Some v
+
+
+
+let is_pure e =
+  match e with
+  | Effect_aux (Effect_set [],_) -> true
+  | _ -> false
+
+let remove_bound (substs,ksubsts) pat =
+  let bound = bindings_from_pat pat in
+  List.fold_left (fun sub v -> Bindings.remove v sub) substs bound, ksubsts
+
+let rec is_value (E_aux (e,(l,annot))) =
+  let is_constructor id =
+    match destruct_tannot annot with
+    | None ->
+       (Reporting.print_err l "Monomorphisation"
+          ("Missing type information for identifier " ^ string_of_id id);
+        false) (* Be conservative if we have no info *)
+    | Some (env,_,_) ->
+       Env.is_union_constructor id env ||
+         (match Env.lookup_id id env with
+         | Enum _ -> true
+         | Unbound | Local _ | Register _ -> false)
+  in
+  match e with
+  | E_id id -> is_constructor id
+  | E_lit _ -> true
+  | E_tuple es -> List.for_all is_value es
+  | E_app (id,es) -> is_constructor id && List.for_all is_value es
+  (* We add casts to undefined to keep the type information in the AST *)
+  | E_cast (typ,E_aux (E_lit (L_aux (L_undef,_)),_)) -> true
+(* TODO: more? *)
+  | _ -> false
+
+let isubst_minus_set subst set =
+  IdSet.fold Bindings.remove set subst
+
+let threaded_map f state l =
+  let l',state' =
+    List.fold_left (fun (tl,state) element -> let (el',state') = f state element in (el'::tl,state'))
+      ([],state) l
+  in List.rev l',state'
+
+
+(* Attempt simple pattern matches *)
+let lit_match = function
+  | (L_zero | L_false), (L_zero | L_false) -> true
+  | (L_one  | L_true ), (L_one  | L_true ) -> true
+  | L_num i1, L_num i2 -> Big_int.equal i1 i2
+  | l1,l2 -> l1 = l2
+
+(* There's no undefined nexp, so replace undefined sizes with a plausible size.
+   32 is used as a sensible default. *)
+
+let fabricate_nexp_exist env l typ kids nc typ' =
+  match kids,nc,Env.expand_synonyms env typ' with
+  | ([kid],NC_aux (NC_set (kid',i::_),_),
+     Typ_aux (Typ_app (Id_aux (Id "atom",_),
+                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_))
+      when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 ->
+     Nexp_aux (Nexp_constant i,Unknown)
+  | ([kid],NC_aux (NC_true,_),
+     Typ_aux (Typ_app (Id_aux (Id "atom",_),
+                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_))
+      when Kid.compare kid kid'' = 0 ->
+     nint 32
+  | ([kid],NC_aux (NC_set (kid',i::_),_),
+     Typ_aux (Typ_app (Id_aux (Id "range",_),
+                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_);
+                        A_aux (A_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
+      when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 &&
+        Kid.compare kid kid''' = 0 ->
+     Nexp_aux (Nexp_constant i,Unknown)
+  | ([kid],NC_aux (NC_true,_),
+     Typ_aux (Typ_app (Id_aux (Id "range",_),
+                       [A_aux (A_nexp (Nexp_aux (Nexp_var kid'',_)),_);
+                        A_aux (A_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_))
+      when Kid.compare kid kid'' = 0 &&
+        Kid.compare kid kid''' = 0 ->
+     nint 32
+  | ([], _, typ) -> nint 32
+  | (kids, nc, typ) ->
+     raise (Reporting.err_general l
+              ("Undefined value at unsupported type " ^ string_of_typ typ ^ " with " ^ Util.string_of_list ", " string_of_kid kids))
+
+let fabricate_nexp l tannot =
+  match destruct_tannot tannot with
+  | None -> nint 32
+  | Some (env,typ,_) ->
+     match Type_check.destruct_exist (Type_check.Env.expand_synonyms env typ) with
+     | None -> nint 32
+     (* TODO: check this *)
+     | Some (kopts,nc,typ') -> fabricate_nexp_exist env l typ (List.map kopt_kid kopts) nc typ'
+
+let atom_typ_kid kid = function
+  | Typ_aux (Typ_app (Id_aux (Id "atom",_),
+                      [A_aux (A_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_) ->
+     Kid.compare kid kid' = 0
+  | _ -> false
+
+(* We reduce casts in a few cases, in particular to ensure that where the
+   type checker has added a ({'n, true. atom('n)}) ex_int(...) cast we can
+   fill in the 'n.  For undefined we fabricate a suitable value for 'n. *)
+
+let reduce_cast typ exp l annot =
+  let env = env_of_annot (l,annot) in
+  let typ' = Env.base_typ_of env typ in
+  match exp, destruct_exist (Env.expand_synonyms env typ') with
+  | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' ->
+     let nc_env = Env.add_typ_var l kopt env in
+     let nc_env = Env.add_constraint (nc_eq (nvar (kopt_kid kopt)) (nconstant n)) nc_env in
+     if prove __POS__ nc_env nc
+     then exp
+     else raise (Reporting.err_unreachable l __POS__
+                   ("Constant propagation error: literal " ^ Big_int.to_string n ^
+                       " does not satisfy constraint " ^ string_of_n_constraint nc))
+  | E_aux (E_lit (L_aux (L_undef,_)),_), Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' ->
+     let nexp = fabricate_nexp_exist env Unknown typ [kopt_kid kopt] nc typ'' in
+     let newtyp = subst_kids_typ (KBindings.singleton (kopt_kid kopt) nexp) typ'' in
+     E_aux (E_cast (newtyp, exp), (Generated l,replace_typ newtyp annot))
+  | E_aux (E_cast (_,
+                   (E_aux (E_lit (L_aux (L_undef,_)),_) as exp)),_),
+     Some ([kopt],nc,typ'') when atom_typ_kid (kopt_kid kopt) typ'' ->
+     let nexp = fabricate_nexp_exist env Unknown typ [kopt_kid kopt] nc typ'' in
+     let newtyp = subst_kids_typ (KBindings.singleton (kopt_kid kopt) nexp) typ'' in
+     E_aux (E_cast (newtyp, exp), (Generated l,replace_typ newtyp annot))
+  | _ -> E_aux (E_cast (typ,exp),(l,annot))
+
+(* Used for constant propagation in pattern matches *)
+type 'a matchresult =
+  | DoesMatch of 'a
+  | DoesNotMatch
+  | GiveUp
+
+(* Remove top-level casts from an expression.  Useful when we need to look at
+   subexpressions to reduce something, but could break type-checking if we used
+   it everywhere. *)
+let rec drop_casts = function
+  | E_aux (E_cast (_,e),_) -> drop_casts e
+  | exp -> exp
+
+let int_of_str_lit = function
+  | L_hex hex -> Big_int.of_string ("0x" ^ hex)
+  | L_bin bin -> Big_int.of_string ("0b" ^ bin)
+  | _ -> assert false
+
+let bits_of_lit = function
+  | L_bin bin -> bin
+  | L_hex hex -> hex_to_bin hex
+  | _ -> assert false
+
+let slice_lit (L_aux (lit,ll)) i len (Ord_aux (ord,_)) =
+  let i = Big_int.to_int i in
+  let len = Big_int.to_int len in
+  let bin = bits_of_lit lit in
+  match match ord with
+  | Ord_inc -> Some i
+  | Ord_dec -> Some (String.length bin - i - len)
+  | Ord_var _ -> None
+  with
+  | None -> None
+  | Some i ->
+     Some (L_aux (L_bin (String.sub bin i len),Generated ll))
+
+let concat_vec lit1 lit2 =
+  let bits1 = bits_of_lit lit1 in
+  let bits2 = bits_of_lit lit2 in
+  L_bin (bits1 ^ bits2)
+
+let lit_eq (L_aux (l1,_)) (L_aux (l2,_)) =
+  match l1,l2 with
+  | (L_zero|L_false), (L_zero|L_false)
+  | (L_one |L_true ), (L_one |L_true)
+    -> Some true
+  | (L_hex _| L_bin _), (L_hex _|L_bin _)
+    -> Some (Big_int.equal (int_of_str_lit l1) (int_of_str_lit l2))
+  | L_undef, _ | _, L_undef -> None
+  | L_num i1, L_num i2 -> Some (Big_int.equal i1 i2)
+  | _ -> Some (l1 = l2)
+
+let try_app (l,ann) (id,args) =
+  let new_l = Parse_ast.Generated l in
+  let env = env_of_annot (l,ann) in
+  let get_overloads f = List.map string_of_id
+    (Env.get_overloads (Id_aux (Id f, Parse_ast.Unknown)) env @
+    Env.get_overloads (Id_aux (DeIid f, Parse_ast.Unknown)) env) in
+  let is_id f = List.mem (string_of_id id) (f :: get_overloads f) in
+  if is_id "==" || is_id "!=" then
+    match args with
+    | [E_aux (E_lit l1,_); E_aux (E_lit l2,_)] ->
+       let lit b = if b then L_true else L_false in
+       let lit b = lit (if is_id "==" then b else not b) in
+       (match lit_eq l1 l2 with
+       | None -> None
+       | Some b -> Some (E_aux (E_lit (L_aux (lit b,new_l)),(l,ann))))
+    | _ -> None
+  else if is_id "cast_bit_bool" then
+    match args with
+    | [E_aux (E_lit L_aux (L_zero,_),_)] -> Some (E_aux (E_lit (L_aux (L_false,new_l)),(l,ann)))
+    | [E_aux (E_lit L_aux (L_one ,_),_)] -> Some (E_aux (E_lit (L_aux (L_true ,new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "UInt" || is_id "unsigned" then
+    match args with
+    | [E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit,_), _)] ->
+       Some (E_aux (E_lit (L_aux (L_num (int_of_str_lit lit),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "slice" then
+    match args with
+    | [E_aux (E_lit (L_aux ((L_hex _| L_bin _),_) as lit), annot);
+       E_aux (E_lit L_aux (L_num i,_), _);
+       E_aux (E_lit L_aux (L_num len,_), _)] ->
+       (match Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) with
+       | Typ_aux (Typ_app (_,[_;A_aux (A_order ord,_);_]),_) ->
+          (match slice_lit lit i len ord with
+          | Some lit' -> Some (E_aux (E_lit lit',(l,ann)))
+          | None -> None)
+       | _ -> None)
+    | _ -> None
+  else if is_id "bitvector_concat" then
+    match args with
+    | [E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit1,_), _);
+       E_aux (E_lit L_aux ((L_hex _| L_bin _) as lit2,_), _)] ->
+       Some (E_aux (E_lit (L_aux (concat_vec lit1 lit2,new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "shl_int" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (Big_int.shift_left i (Big_int.to_int j)),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "mult_atom" || is_id "mult_int" || is_id "mult_range" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (Big_int.mul i j),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "quotient_nat" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (Big_int.div i j),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "add_atom" || is_id "add_int" || is_id "add_range" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_); E_aux (E_lit L_aux (L_num j,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (Big_int.add i j),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "negate_range" then
+    match args with
+    | [E_aux (E_lit L_aux (L_num i,_),_)] ->
+       Some (E_aux (E_lit (L_aux (L_num (Big_int.negate i),new_l)),(l,ann)))
+    | _ -> None
+  else if is_id "ex_int" then
+    match args with
+    | [E_aux (E_lit lit,(l,_))] -> Some (E_aux (E_lit lit,(l,ann)))
+    | [E_aux (E_cast (_,(E_aux (E_lit (L_aux (L_undef,_)),_) as e)),(l,_))] ->
+       Some (reduce_cast (typ_of_annot (l,ann)) e l ann)
+    | _ -> None
+  else if is_id "vector_access" || is_id "bitvector_access" then
+    match args with
+    | [E_aux (E_lit L_aux ((L_hex _ | L_bin _) as lit,_),_);
+       E_aux (E_lit L_aux (L_num i,_),_)] ->
+       let v = int_of_str_lit lit in
+       let b = Big_int.bitwise_and (Big_int.shift_right v (Big_int.to_int i)) (Big_int.of_int 1) in
+       let lit' = if Big_int.equal b (Big_int.of_int 1) then L_one else L_zero in
+       Some (E_aux (E_lit (L_aux (lit',new_l)),(l,ann)))
+    | _ -> None
+  else None
+
+
+let construct_lit_vector args =
+  let rec aux l = function
+    | [] -> Some (L_aux (L_bin (String.concat "" (List.rev l)),Unknown))
+    | E_aux (E_lit (L_aux ((L_zero | L_one) as lit,_)),_)::t ->
+       aux ((if lit = L_zero then "0" else "1")::l) t
+    | _ -> None
+  in aux [] args
+
+(* Add a cast to undefined so that it retains its type, otherwise it can't be
+   substituted safely *)
+let keep_undef_typ value =
+  match value with
+  | E_aux (E_lit (L_aux (L_undef,lann)),eann) ->
+     E_aux (E_cast (typ_of_annot eann,value),(Generated Unknown,snd eann))
+  | _ -> value
+
+(* Check whether the current environment with the given kid assignments is
+   inconsistent (and hence whether the code is dead) *)
+let is_env_inconsistent env ksubsts =
+  let env = KBindings.fold (fun k nexp env ->
+    Env.add_constraint (nc_eq (nvar k) nexp) env) ksubsts env in
+  prove __POS__ env nc_false
+
+
+let const_props defs ref_vars =
+  let rec const_prop_exp substs assigns ((E_aux (e,(l,annot))) as exp) =
+    (* Functions to treat lists and tuples of subexpressions as possibly
+       non-deterministic: that is, we stop making any assumptions about
+       variables that are assigned to in any of the subexpressions *)
+    let non_det_exp_list es =
+      let assigned_in =
+        List.fold_left (fun vs exp -> IdSet.union vs (assigned_vars exp))
+          IdSet.empty es in
+      let assigns = isubst_minus_set assigns assigned_in in
+      let es' = List.map (fun e -> fst (const_prop_exp substs assigns e)) es in
+      es',assigns
+    in
+    let non_det_exp_2 e1 e2 =
+       let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in
+       let assigns = isubst_minus_set assigns assigned_in_e12 in
+       let e1',_ = const_prop_exp substs assigns e1 in
+       let e2',_ = const_prop_exp substs assigns e2 in
+       e1',e2',assigns
+    in
+    let non_det_exp_3 e1 e2 e3 =
+       let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in
+       let assigned_in_e123 = IdSet.union assigned_in_e12 (assigned_vars e3) in
+       let assigns = isubst_minus_set assigns assigned_in_e123 in
+       let e1',_ = const_prop_exp substs assigns e1 in
+       let e2',_ = const_prop_exp substs assigns e2 in
+       let e3',_ = const_prop_exp substs assigns e3 in
+       e1',e2',e3',assigns
+    in
+    let non_det_exp_4 e1 e2 e3 e4 =
+       let assigned_in_e12 = IdSet.union (assigned_vars e1) (assigned_vars e2) in
+       let assigned_in_e123 = IdSet.union assigned_in_e12 (assigned_vars e3) in
+       let assigned_in_e1234 = IdSet.union assigned_in_e123 (assigned_vars e4) in
+       let assigns = isubst_minus_set assigns assigned_in_e1234 in
+       let e1',_ = const_prop_exp substs assigns e1 in
+       let e2',_ = const_prop_exp substs assigns e2 in
+       let e3',_ = const_prop_exp substs assigns e3 in
+       let e4',_ = const_prop_exp substs assigns e4 in
+       e1',e2',e3',e4',assigns
+    in
+    let re e assigns = E_aux (e,(l,annot)),assigns in
+    match e with
+      (* TODO: are there more circumstances in which we should get rid of these? *)
+    | E_block [e] -> const_prop_exp substs assigns e
+    | E_block es ->
+       let es',assigns = threaded_map (const_prop_exp substs) assigns es in
+       re (E_block es') assigns
+    | E_nondet es ->
+       let es',assigns = non_det_exp_list es in
+       re (E_nondet es') assigns
+    | E_id id ->
+       let env = Type_check.env_of_annot (l, annot) in
+       (try
+         match Env.lookup_id id env with
+         | Local (Immutable,_) -> Bindings.find id (fst substs)
+         | Local (Mutable,_)   -> Bindings.find id assigns
+         | _ -> exp
+       with Not_found -> exp),assigns
+    | E_lit _
+    | E_sizeof _
+    | E_constraint _
+      -> exp,assigns
+    | E_cast (t,e') ->
+       let e'',assigns = const_prop_exp substs assigns e' in
+       if is_value e''
+       then reduce_cast t e'' l annot, assigns
+       else re (E_cast (t, e'')) assigns
+    | E_app (id,es) ->
+       let es',assigns = non_det_exp_list es in
+       let env = Type_check.env_of_annot (l, annot) in
+       (match try_app (l,annot) (id,es') with
+       | None ->
+          (match const_prop_try_fn l env (id,es') with
+          | None -> re (E_app (id,es')) assigns
+          | Some r -> r,assigns)
+       | Some r -> r,assigns)
+    | E_tuple es ->
+       let es',assigns = non_det_exp_list es in
+       re (E_tuple es') assigns
+    | E_if (e1,e2,e3) ->
+       let e1',assigns = const_prop_exp substs assigns e1 in
+       let e1_no_casts = drop_casts e1' in
+       (match e1_no_casts with
+       | E_aux (E_lit (L_aux ((L_true|L_false) as lit ,_)),_) ->
+          (match lit with
+          | L_true -> const_prop_exp substs assigns e2
+          |  _     -> const_prop_exp substs assigns e3)
+       | _ ->
+          (* If the guard is an equality check, propagate the value. *)
+          let env1 = env_of e1_no_casts in
+          let is_equal id =
+            List.exists (fun id' -> Id.compare id id' == 0)
+              (Env.get_overloads (Id_aux (DeIid "==", Parse_ast.Unknown))
+                 env1)
+          in
+          let substs_true =
+            match e1_no_casts with
+            | E_aux (E_app (id, [E_aux (E_id var,_); vl]),_)
+            | E_aux (E_app (id, [vl; E_aux (E_id var,_)]),_)
+                when is_equal id ->
+               if is_value vl then
+                 (match Env.lookup_id var env1 with
+                 | Local (Immutable,_) -> Bindings.add var vl (fst substs),snd substs
+                 | _ -> substs)
+               else substs
+            | _ -> substs
+          in
+          (* Discard impossible branches *)
+          if is_env_inconsistent (env_of e2) (snd substs) then
+            const_prop_exp substs assigns e3
+          else if is_env_inconsistent (env_of e3) (snd substs) then
+            const_prop_exp substs_true assigns e2
+          else
+            let e2',assigns2 = const_prop_exp substs_true assigns e2 in
+            let e3',assigns3 = const_prop_exp substs assigns e3 in
+            let assigns = isubst_minus_set assigns (assigned_vars e2) in
+            let assigns = isubst_minus_set assigns (assigned_vars e3) in
+            re (E_if (e1',e2',e3')) assigns)
+    | E_for (id,e1,e2,e3,ord,e4) ->
+       (* Treat e1, e2 and e3 (from, to and by) as a non-det tuple *)
+       let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in
+       let assigns = isubst_minus_set assigns (assigned_vars e4) in
+       let e4',_ = const_prop_exp (Bindings.remove id (fst substs),snd substs) assigns e4 in
+       re (E_for (id,e1',e2',e3',ord,e4')) assigns
+    | E_loop (loop,e1,e2) ->
+       let assigns = isubst_minus_set assigns (IdSet.union (assigned_vars e1) (assigned_vars e2)) in
+       let e1',_ = const_prop_exp substs assigns e1 in
+       let e2',_ = const_prop_exp substs assigns e2 in
+       re (E_loop (loop,e1',e2')) assigns
+    | E_vector es ->
+       let es',assigns = non_det_exp_list es in
+       begin
+         match construct_lit_vector es' with
+         | None -> re (E_vector es') assigns
+         | Some lit -> re (E_lit lit) assigns
+       end
+    | E_vector_access (e1,e2) ->
+       let e1',e2',assigns = non_det_exp_2 e1 e2 in
+       re (E_vector_access (e1',e2')) assigns
+    | E_vector_subrange (e1,e2,e3) ->
+       let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in
+       re (E_vector_subrange (e1',e2',e3')) assigns
+    | E_vector_update (e1,e2,e3) ->
+       let e1',e2',e3',assigns = non_det_exp_3 e1 e2 e3 in
+       re (E_vector_update (e1',e2',e3')) assigns
+    | E_vector_update_subrange (e1,e2,e3,e4) ->
+       let e1',e2',e3',e4',assigns = non_det_exp_4 e1 e2 e3 e4 in
+       re (E_vector_update_subrange (e1',e2',e3',e4')) assigns
+    | E_vector_append (e1,e2) ->
+       let e1',e2',assigns = non_det_exp_2 e1 e2 in
+       re (E_vector_append (e1',e2')) assigns
+    | E_list es ->
+       let es',assigns = non_det_exp_list es in
+       re (E_list es') assigns
+    | E_cons (e1,e2) ->
+       let e1',e2',assigns = non_det_exp_2 e1 e2 in
+       re (E_cons (e1',e2')) assigns
+    | E_record fes ->
+       let assigned_in_fes = assigned_vars_in_fexps fes in
+       let assigns = isubst_minus_set assigns assigned_in_fes in
+       re (E_record (const_prop_fexps substs assigns fes)) assigns
+    | E_record_update (e,fes) ->
+       let assigned_in = IdSet.union (assigned_vars_in_fexps fes) (assigned_vars e) in
+       let assigns = isubst_minus_set assigns assigned_in in
+       let e',_ = const_prop_exp substs assigns e in
+       re (E_record_update (e', const_prop_fexps substs assigns fes)) assigns
+    | E_field (e,id) ->
+       let e',assigns = const_prop_exp substs assigns e in
+       re (E_field (e',id)) assigns
+    | E_case (e,cases) ->
+       let e',assigns = const_prop_exp substs assigns e in
+       (match can_match e' cases substs assigns with
+       | None ->
+          let assigned_in =
+            List.fold_left (fun vs pe -> IdSet.union vs (assigned_vars_in_pexp pe))
+              IdSet.empty cases
+          in
+          let assigns' = isubst_minus_set assigns assigned_in in
+          re (E_case (e', List.map (const_prop_pexp substs assigns) cases)) assigns'
+       | Some (E_aux (_,(_,annot')) as exp,newbindings,kbindings) ->
+          let exp = nexp_subst_exp (kbindings_from_list kbindings) exp in
+          let newbindings_env = bindings_from_list newbindings in
+          let substs' = bindings_union (fst substs) newbindings_env, snd substs in
+          const_prop_exp substs' assigns exp)
+    | E_let (lb,e2) ->
+       begin
+         match lb with
+         | LB_aux (LB_val (p,e), annot) ->
+            let e',assigns = const_prop_exp substs assigns e in
+            let substs' = remove_bound substs p in
+            let plain () =
+              let e2',assigns = const_prop_exp substs' assigns e2 in
+              re (E_let (LB_aux (LB_val (p,e'), annot),
+                         e2')) assigns in
+            if is_value e' && not (is_value e) then
+              match can_match e' [Pat_aux (Pat_exp (p,e2),(Unknown,empty_tannot))] substs assigns with
+              | None -> plain ()
+              | Some (e'',bindings,kbindings) ->
+                 let e'' = nexp_subst_exp (kbindings_from_list kbindings) e'' in
+                 let bindings = bindings_from_list bindings in
+                 let substs'' = bindings_union (fst substs') bindings, snd substs' in
+                 const_prop_exp substs'' assigns e''
+            else plain ()
+       end
+    (* TODO maybe - tuple assignments *)
+    | E_assign (le,e) ->
+       let env = Type_check.env_of_annot (l, annot) in
+       let assigned_in = IdSet.union (assigned_vars_in_lexp le) (assigned_vars e) in
+       let assigns = isubst_minus_set assigns assigned_in in
+       let le',idopt = const_prop_lexp substs assigns le in
+       let e',_ = const_prop_exp substs assigns e in
+       let assigns =
+         match idopt with
+         | Some id ->
+            begin
+              match Env.lookup_id id env with
+              | Local (Mutable,_) | Unbound ->
+                 if is_value e' && not (IdSet.mem id ref_vars)
+                 then Bindings.add id (keep_undef_typ e') assigns
+                 else Bindings.remove id assigns
+              | _ -> assigns
+            end
+         | None -> assigns
+       in
+       re (E_assign (le', e')) assigns
+    | E_exit e ->
+       let e',_ = const_prop_exp substs assigns e in
+       re (E_exit e') Bindings.empty
+    | E_ref id -> re (E_ref id) Bindings.empty
+    | E_throw e ->
+       let e',_ = const_prop_exp substs assigns e in
+       re (E_throw e') Bindings.empty
+    | E_try (e,cases) ->
+       (* TODO: try and preserve *any* assignment info *)
+       let e',_ = const_prop_exp substs assigns e in
+       re (E_case (e', List.map (const_prop_pexp substs Bindings.empty) cases)) Bindings.empty
+    | E_return e ->
+       let e',_ = const_prop_exp substs assigns e in
+       re (E_return e') Bindings.empty
+    | E_assert (e1,e2) ->
+       let e1',e2',assigns = non_det_exp_2 e1 e2 in
+       re (E_assert (e1',e2')) assigns
+  
+    | E_app_infix _
+    | E_var _
+    | E_internal_plet _
+    | E_internal_return _
+    | E_internal_value _
+      -> raise (Reporting.err_unreachable l __POS__
+                  ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
+  and const_prop_fexps substs assigns fes =
+    List.map (const_prop_fexp substs assigns) fes
+  and const_prop_fexp substs assigns (FE_aux (FE_Fexp (id,e), annot)) =
+    FE_aux (FE_Fexp (id,fst (const_prop_exp substs assigns e)),annot)
+  and const_prop_pexp substs assigns = function
+    | (Pat_aux (Pat_exp (p,e),l)) ->
+       Pat_aux (Pat_exp (p,fst (const_prop_exp (remove_bound substs p) assigns e)),l)
+    | (Pat_aux (Pat_when (p,e1,e2),l)) ->
+       let substs' = remove_bound substs p in
+       let e1',assigns = const_prop_exp substs' assigns e1 in
+       Pat_aux (Pat_when (p, e1', fst (const_prop_exp substs' assigns e2)),l)
+  and const_prop_lexp substs assigns ((LEXP_aux (e,annot)) as le) =
+    let re e = LEXP_aux (e,annot), None in
+    match e with
+    | LEXP_id id (* shouldn't end up substituting here *)
+    | LEXP_cast (_,id)
+      -> le, Some id
+    | LEXP_memory (id,es) ->
+       re (LEXP_memory (id,List.map (fun e -> fst (const_prop_exp substs assigns e)) es)) (* or here *)
+    | LEXP_tup les -> re (LEXP_tup (List.map (fun le -> fst (const_prop_lexp substs assigns le)) les))
+    | LEXP_vector (le,e) -> re (LEXP_vector (fst (const_prop_lexp substs assigns le), fst (const_prop_exp substs assigns e)))
+    | LEXP_vector_range (le,e1,e2) ->
+       re (LEXP_vector_range (fst (const_prop_lexp substs assigns le),
+                              fst (const_prop_exp substs assigns e1),
+                              fst (const_prop_exp substs assigns e2)))
+    | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map (fun le -> fst (const_prop_lexp substs assigns le)) les))
+    | LEXP_field (le,id) -> re (LEXP_field (fst (const_prop_lexp substs assigns le), id))
+    | LEXP_deref e ->
+       re (LEXP_deref (fst (const_prop_exp substs assigns e)))
+  (* Reduce a function when
+     1. all arguments are values,
+     2. the function is pure,
+     3. the result is a value
+     (and 4. the function is not scattered, but that's not terribly important)
+     to try and keep execution time and the results managable.
+  *)
+  and const_prop_try_fn l env (id,args) =
+    if not (List.for_all is_value args) then
+      None
+    else
+      let (tq,typ) = Env.get_val_spec_orig id env in
+      let eff = match typ with
+        | Typ_aux (Typ_fn (_,_,eff),_) -> Some eff
+        | _ -> None
+      in
+      let Defs ds = defs in
+      match eff, list_extract (function
+      | (DEF_fundef (FD_aux (FD_function (_,_,eff,((FCL_aux (FCL_Funcl (id',_),_))::_ as fcls)),_)))
+        -> if Id.compare id id' = 0 then Some fcls else None
+      | _ -> None) ds with
+      | None,_ | _,None -> None
+      | Some eff,_ when not (is_pure eff) -> None
+      | Some _,Some fcls ->
+         let arg = match args with
+           | [] -> E_aux (E_lit (L_aux (L_unit,Generated l)),(Generated l,empty_tannot))
+           | [e] -> e
+           | _ -> E_aux (E_tuple args,(Generated l,empty_tannot)) in
+         let cases = List.map (function
+           | FCL_aux (FCL_Funcl (_,pexp), ann) -> pexp)
+           fcls in
+         match can_match_with_env env arg cases (Bindings.empty,KBindings.empty) Bindings.empty with
+         | Some (exp,bindings,kbindings) ->
+            let substs = bindings_from_list bindings, kbindings_from_list kbindings in
+            let result,_ = const_prop_exp substs Bindings.empty exp in
+            let result = match result with
+              | E_aux (E_return e,_) -> e
+              | _ -> result
+            in
+            if is_value result then Some result else None
+         | None -> None
+  
+  and can_match_with_env env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns =
+    let rec findpat_generic check_pat description assigns = function
+      | [] -> (Reporting.print_err l "Monomorphisation"
+                 ("Failed to find a case for " ^ description); None)
+      | [Pat_aux (Pat_exp (P_aux (P_wild,_),exp),_)] -> Some (exp,[],[])
+      | (Pat_aux (Pat_exp (P_aux (P_typ (_,p),_),exp),ann))::tl ->
+         findpat_generic check_pat description assigns ((Pat_aux (Pat_exp (p,exp),ann))::tl)
+      | (Pat_aux (Pat_exp (P_aux (P_id id',_),exp),_))::tlx
+          when pat_id_is_variable env id' ->
+         Some (exp, [(id', exp0)], [])
+      | (Pat_aux (Pat_when (P_aux (P_id id',_),guard,exp),_))::tl
+          when pat_id_is_variable env id' -> begin
+            let substs = Bindings.add id' exp0 substs, ksubsts in
+            let (E_aux (guard,_)),assigns = const_prop_exp substs assigns guard in
+            match guard with
+            | E_lit (L_aux (L_true,_)) -> Some (exp,[(id',exp0)],[])
+            | E_lit (L_aux (L_false,_)) -> findpat_generic check_pat description assigns tl
+            | _ -> None
+          end
+      | (Pat_aux (Pat_when (p,guard,exp),_))::tl -> begin
+        match check_pat p with
+        | DoesNotMatch -> findpat_generic check_pat description assigns tl
+        | DoesMatch (vsubst,ksubst) -> begin
+          let guard = nexp_subst_exp (kbindings_from_list ksubst) guard in
+          let substs = bindings_union substs (bindings_from_list vsubst),
+                       kbindings_union ksubsts (kbindings_from_list ksubst) in
+          let (E_aux (guard,_)),assigns = const_prop_exp substs assigns guard in
+          match guard with
+          | E_lit (L_aux (L_true,_)) -> Some (exp,vsubst,ksubst)
+          | E_lit (L_aux (L_false,_)) -> findpat_generic check_pat description assigns tl
+          | _ -> None
+        end
+        | GiveUp -> None
+      end
+      | (Pat_aux (Pat_exp (p,exp),_))::tl ->
+         match check_pat p with
+         | DoesNotMatch -> findpat_generic check_pat description assigns tl
+         | DoesMatch (subst,ksubst) -> Some (exp,subst,ksubst)
+         | GiveUp -> None
+    in
+    match e with
+    | E_id id ->
+       (match Env.lookup_id id env with
+       | Enum _ ->
+          let checkpat = function
+            | P_aux (P_id id',_)
+            | P_aux (P_app (id',[]),_) ->
+               if Id.compare id id' = 0 then DoesMatch ([],[]) else DoesNotMatch
+            | P_aux (_,(l',_)) ->
+               (Reporting.print_err l' "Monomorphisation"
+                  "Unexpected kind of pattern for enumeration"; GiveUp)
+          in findpat_generic checkpat (string_of_id id) assigns cases
+       | _ -> None)
+    | E_lit (L_aux (lit_e, lit_l)) ->
+       let checkpat = function
+         | P_aux (P_lit (L_aux (lit_p, _)),_) ->
+            if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch
+         | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) ->
+            begin
+              match lit_e with
+              | L_num i ->
+                 DoesMatch ([id, E_aux (e,(l,annot))],
+                            [kid,Nexp_aux (Nexp_constant i,Unknown)])
+              (* For undefined we fix the type-level size (because there's no good
+                 way to construct an undefined size), but leave the term as undefined
+                 to make the meaning clear. *)
+              | L_undef ->
+                 let nexp = fabricate_nexp l annot in
+                 let typ = subst_kids_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in
+                 DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,empty_tannot))),(l,empty_tannot))],
+                            [kid,nexp])
+              | _ ->
+                 (Reporting.print_err lit_l "Monomorphisation"
+                    "Unexpected kind of literal for var match"; GiveUp)
+            end
+         | P_aux (_,(l',_)) ->
+            (Reporting.print_err l' "Monomorphisation"
+               "Unexpected kind of pattern for literal"; GiveUp)
+       in findpat_generic checkpat "literal" assigns cases
+    | E_vector es when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es ->
+       let checkpat = function
+         | P_aux (P_vector ps,_) ->
+            let matches = List.map2 (fun e p ->
+              match e, p with
+              | E_aux (E_lit (L_aux (lit,_)),_), P_aux (P_lit (L_aux (lit',_)),_) ->
+                 if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch
+              | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var ->
+                 DoesMatch ([var, e],[])
+              | _ -> GiveUp) es ps in
+            let final = List.fold_left (fun acc m -> match acc, m with
+              | _, GiveUp -> GiveUp
+              | GiveUp, _ -> GiveUp
+              | DoesMatch (sub,ksub), DoesMatch(sub',ksub') -> DoesMatch(sub@sub',ksub@ksub')
+              | _ -> DoesNotMatch) (DoesMatch ([],[])) matches in
+            (match final with
+            | GiveUp ->
+               (Reporting.print_err l "Monomorphisation"
+                  "Unexpected kind of pattern for vector literal"; GiveUp)
+            | _ -> final)
+         | _ ->
+            (Reporting.print_err l "Monomorphisation"
+               "Unexpected kind of pattern for vector literal"; GiveUp)
+       in findpat_generic checkpat "vector literal" assigns cases
+  
+    | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)) ->
+       let checkpat = function
+         | P_aux (P_lit (L_aux (lit_p, _)),_) -> DoesNotMatch
+         | P_aux (P_var (P_aux (P_id id,p_id_annot), TP_aux (TP_var kid, _)),_) ->
+              (* For undefined we fix the type-level size (because there's no good
+                 way to construct an undefined size), but leave the term as undefined
+                 to make the meaning clear. *)
+            let nexp = fabricate_nexp l annot in
+            let kids = equal_kids (env_of_annot p_id_annot) kid in
+            let ksubst = KidSet.fold (fun k b -> KBindings.add k nexp b) kids KBindings.empty in
+            let typ = subst_kids_typ ksubst (typ_of_annot p_id_annot) in
+            DoesMatch ([id, E_aux (E_cast (typ,e_undef),(l,empty_tannot))],
+                       KBindings.bindings ksubst)
+         | P_aux (_,(l',_)) ->
+            (Reporting.print_err l' "Monomorphisation"
+               "Unexpected kind of pattern for literal"; GiveUp)
+       in findpat_generic checkpat "literal" assigns cases
+    | _ -> None
+  
+  and can_match exp =
+    let env = Type_check.env_of exp in
+    can_match_with_env env exp
+
+in (const_prop_exp, const_prop_pexp)
+
+let const_prop d r = fst (const_props d r)
+let const_prop_pexp d r = snd (const_props d r)
+
+let referenced_vars exp =
+  let open Rewriter in
+  fst (fold_exp
+         { (compute_exp_alg IdSet.empty IdSet.union) with
+           e_ref = (fun id -> IdSet.singleton id, E_ref id) } exp)
+
+(* This is intended to remove impossible cases when a type-level constant has
+   been used to fix a property of the architecture.  In particular, the current
+   version of the RISC-V model uses constructs like
+
+   match (width, sizeof(xlen)) {
+     (BYTE, _)    => ...
+     ...
+     (DOUBLE, 64) => ...
+   };
+
+   and the type checker will replace the sizeof with the literal 32 or 64.  This
+   pass will then remove the DOUBLE case.
+
+   It would be nice to have the full constant propagation above do this kind of
+   thing too...
+*)
+
+let remove_impossible_int_cases _ =
+
+  let must_keep_case exp (Pat_aux ((Pat_exp (p,_) | Pat_when (p,_,_)),_)) =
+    let rec aux (E_aux (exp,_)) (P_aux (p,_)) =
+      match exp, p with
+      | E_tuple exps, P_tup ps -> List.for_all2 aux exps ps
+      | E_lit (L_aux (lit,_)), P_lit (L_aux (lit',_)) -> lit_match (lit, lit')
+      | _ -> true
+    in aux exp p
+  in
+  let e_case (exp,cases) =
+    E_case (exp, List.filter (must_keep_case exp) cases)
+  in
+  let e_if (cond, e_then, e_else) =
+    match destruct_atom_bool (env_of cond) (typ_of cond) with
+    | Some nc ->
+       if prove __POS__ (env_of cond) nc then unaux_exp e_then else
+       if prove __POS__ (env_of cond) (nc_not nc) then unaux_exp e_else else
+       E_if (cond, e_then, e_else)
+    | _ -> E_if (cond, e_then, e_else)
+  in
+  let open Rewriter in
+  let rewrite_exp _ = fold_exp { id_exp_alg with e_case = e_case; e_if = e_if } in
+  rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp }