From faec5d87b9d9690b1c95928d2d932d5d51d94cd4 Mon Sep 17 00:00:00 2001
From: emersion
Date: Wed, 9 May 2018 12:30:32 +0100
Subject: Fix Byte_sequence errors due to linksem update

---
 src/elf_loader.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index 89987647..02ff072b 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -65,9 +65,9 @@ let rec break n = function
   | (_ :: _ as xs) -> [Lem_list.take n xs] @ break n (Lem_list.drop n xs)
 
 let print_segment seg =
-  let (Byte_sequence.Sequence bs) = seg.Elf_interpreted_segment.elf64_segment_body in
+  let bs = seg.Elf_interpreted_segment.elf64_segment_body in
   prerr_endline "0011 2233 4455 6677 8899 aabb ccdd eeff 0123456789abcdef";
-  List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 bs)
+  List.iter (fun bs -> prerr_endline (hex_line bs)) (break 16 (Byte_sequence.char_list_of_byte_sequence bs))
 
 let read name =
   let info = Sail_interface.populate_and_obtain_global_symbol_init_info name in
@@ -112,7 +112,7 @@ let write_file chan paddr i byte =
 
 let load_segment ?writer:(writer=write_sail_lib) seg =
   let open Elf_interpreted_segment in
-  let (Byte_sequence.Sequence bs) = seg.elf64_segment_body in
+  let bs = seg.elf64_segment_body in
   let paddr = seg.elf64_segment_paddr in
   let base = seg.elf64_segment_base in
   let offset = seg.elf64_segment_offset in
@@ -121,7 +121,7 @@ let load_segment ?writer:(writer=write_sail_lib) seg =
   prerr_endline ("Segment base address: " ^ Big_int.to_string base);
   prerr_endline ("Segment physical address: " ^ Big_int.to_string paddr);
   print_segment seg;
-  List.iteri (writer paddr) (List.map int_of_char bs)
+  List.iteri (writer paddr) (List.map int_of_char (Byte_sequence.char_list_of_byte_sequence bs))
 
 let load_elf ?writer:(writer=write_sail_lib) name =
   let segments, e_entry, symbol_map = read name in
-- 
cgit v1.2.3


From 9fea45722d58132cc484d9421fb3407286dc4f01 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 4 May 2018 16:18:01 +0100
Subject: Generate initial register state record

Filled with default values (e.g., 0) and used to initialise the state monad.
There is already code to generate a Sail function "initialize_registers", but
this is monadic itself, so it cannot be used to initialise the monad.
---
 src/state.ml       | 131 +++++++++++++++++++++++++++++++++++++++++++----------
 src/type_check.mli |   3 ++
 2 files changed, 111 insertions(+), 23 deletions(-)

(limited to 'src')

diff --git a/src/state.ml b/src/state.ml
index 49fa5a99..5a360456 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -60,6 +60,11 @@ open Pretty_print_sail
 
 let defs_of_string = ast_of_def_string Ast_util.inc_ord
 
+let is_defined defs name = IdSet.mem (mk_id name) (ids_of_defs (Defs defs))
+
+let has_default_order defs =
+  List.exists (function DEF_default (DT_aux (DT_order _, _)) -> true | _ -> false) defs
+
 let find_registers defs =
   List.fold_left
     (fun acc def ->
@@ -77,18 +82,100 @@ let generate_regstate = function
   | [] -> ["type regstate = unit"]
   | registers ->
      let reg (typ, id) = Printf.sprintf "%s : %s" (string_of_id id) (to_string (doc_typ typ)) in
-     let initreg (_, id) = Printf.sprintf "%s = undefined" (string_of_id id) in
-     let regstate =
-       "struct regstate = { " ^
-       (String.concat ", " (List.map reg registers)) ^
-       " }"
-     in
-     let initstate =
-       "let initial_regstate : regstate = struct { " ^
-       (String.concat ", " (List.map initreg registers)) ^
-       " }"
-     in
-     regstate :: (if !Initial_check.opt_undefined_gen then [initstate] else [])
+     ["struct regstate = { " ^ (String.concat ", " (List.map reg registers)) ^ " }"]
+
+let generate_initial_regstate defs =
+  let registers = find_registers defs in
+  if registers = [] then [] else
+  try
+    (* Recursively choose a default value for every type in the spec.
+       vals, constructed below, maps user-defined types to default values. *)
+    let rec lookup_init_val vals (Typ_aux (typ_aux, _) as typ) =
+      match typ_aux with
+      | Typ_id id ->
+         if string_of_id id = "bool" then "false" else
+         if string_of_id id = "bit" then "bitzero" else
+         if string_of_id id = "int" then "0" else
+         if string_of_id id = "nat" then "0" else
+         if string_of_id id = "real" then "0" else
+         if string_of_id id = "string" then "\"\"" else
+         if string_of_id id = "unit" then "()" else
+         Bindings.find id vals []
+      | Typ_app (id, _) when string_of_id id = "list" -> "[||]"
+      | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _)]) when string_of_id id = "atom" ->
+         string_of_nexp nexp
+      | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp, _); _]) when string_of_id id = "range" ->
+         string_of_nexp nexp
+      | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_constant len, _)), _); _ ;
+                      Typ_arg_aux (Typ_arg_typ etyp, _)])
+        when string_of_id id = "vector" ->
+         (* Output a list of initial values of the vector elements, or a
+            literal binary zero value if this is a bitvector and the
+            environment has a default indexing order (required by the
+            typechecker for binary and hex literals) *)
+         let literal_bitvec = is_bit_typ etyp && has_default_order defs in
+         let init_elem = if literal_bitvec then "0" else lookup_init_val vals etyp in
+         let rec elems len =
+           if (Nat_big_num.less_equal len Nat_big_num.zero) then [] else
+           init_elem :: elems (Nat_big_num.pred len)
+         in
+         if literal_bitvec then "0b" ^ (String.concat "" (elems len)) else
+         "[" ^ (String.concat ", " (elems len)) ^ "]"
+      | Typ_app (id, args) -> Bindings.find id vals args
+      | Typ_tup typs ->
+         "(" ^ (String.concat ", " (List.map (lookup_init_val vals) typs)) ^ ")"
+      | Typ_exist (_, _, typ) -> lookup_init_val vals typ
+      | _ -> raise Not_found
+    in
+    (* Helper functions to instantiate type arguments *)
+    let typ_subst_targ kid (Typ_arg_aux (arg, _)) typ = match arg with
+      | Typ_arg_nexp (Nexp_aux (nexp, _)) -> typ_subst_nexp kid nexp typ
+      | Typ_arg_typ (Typ_aux (typ', _)) -> typ_subst_typ kid typ' typ
+      | Typ_arg_order (Ord_aux (ord, _)) -> typ_subst_order kid ord typ
+    in
+    let typ_subst_quant_item typ (QI_aux (qi, _)) arg = match qi with
+      | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) ->
+         typ_subst_targ kid arg typ
+      | _ -> typ
+    in
+    let typ_subst_typquant tq args typ =
+      List.fold_left2 typ_subst_quant_item typ (quant_items tq) args
+    in
+    let add_typ_init_val vals = function
+      | TD_enum (id, _, id1 :: _, _) ->
+         (* Choose the first value of an enumeration type as default *)
+         Bindings.add id (fun _ -> string_of_id id1) vals
+      | TD_variant (id, _, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) ->
+         (* Choose the first variant of a union type as default *)
+         let init_val args =
+           let typ1 = typ_subst_typquant tq args typ1 in
+           string_of_id id1 ^ " (" ^ lookup_init_val vals typ1 ^ ")"
+         in
+         Bindings.add id init_val vals
+      | TD_abbrev (id, _, TypSchm_aux (TypSchm_ts (tq, typ), _)) ->
+         let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in
+         Bindings.add id init_val vals
+      | TD_record (id, _, tq, fields, _) ->
+         let init_val args =
+           let init_field (typ, id) =
+             let typ = typ_subst_typquant tq args typ in
+             string_of_id id ^ " = " ^ lookup_init_val vals typ
+           in
+           "struct { " ^ (String.concat ", " (List.map init_field fields)) ^ " }"
+         in
+         Bindings.add id init_val vals
+      | TD_bitfield (id, typ, _) ->
+         Bindings.add id (fun _ -> lookup_init_val vals typ) vals
+      | _ -> vals
+    in
+    let init_vals = List.fold_left (fun vals def -> match def with
+      | DEF_type (TD_aux (td, _)) -> add_typ_init_val vals td
+      | _ -> vals) Bindings.empty defs
+    in
+    let init_reg (typ, id) = string_of_id id ^ " = " ^ lookup_init_val init_vals typ in
+    ["let initial_regstate : regstate = struct { " ^ (String.concat ", " (List.map init_reg registers)) ^ " }"]
+  with
+  | _ -> [] (* Do not generate an initial register state if anything goes wrong *)
 
 let rec regval_constr_id mwords (Typ_aux (t, l) as typ) = match t with
   | Typ_id id -> id
@@ -135,9 +222,8 @@ let generate_regval_typ typs =
   (String.concat ", " (builtins :: List.map constr (Bindings.bindings typs))) ^
   " }"]
 
-let add_regval_conv id typ defs =
+let add_regval_conv id typ (Defs defs) =
   let id = string_of_id id in
-  let is_defined name = IdSet.mem (mk_id name) (ids_of_defs defs) in
   let typ_str = to_string (doc_typ typ) in
   (* Create a function that converts from regval to the target type. *)
   let from_name = id ^ "_of_regval" in
@@ -146,14 +232,14 @@ let add_regval_conv id typ defs =
     Printf.sprintf "function %s Regval_%s(v) = Some(v)" from_name id;
     Printf.sprintf "and %s _ = None()" from_name
     ] in
-  let from_defs = if is_defined from_name then [] else [from_val; from_function] in
+  let from_defs = if is_defined defs from_name then [] else [from_val; from_function] in
   (* Create a function that converts from target type to regval. *)
   let to_name = "regval_of_" ^ id in
   let to_val = Printf.sprintf "val %s : %s -> register_value" to_name typ_str in
   let to_function = Printf.sprintf "function %s v = Regval_%s(v)" to_name id in
-  let to_defs = if is_defined to_name then [] else [to_val; to_function] in
+  let to_defs = if is_defined defs to_name then [] else [to_val; to_function] in
   let cdefs = concat_ast (List.map defs_of_string (from_defs @ to_defs)) in
-  append_ast defs cdefs
+  append_ast (Defs defs) cdefs
 
 let rec regval_convs_lem mwords (Typ_aux (t, _) as typ) = match t with
   | Typ_app _ when is_vector_typ typ && not (mwords && is_bitvector_typ typ) ->
@@ -393,17 +479,16 @@ let generate_regstate_defs mwords defs =
   let gen_undef = !Initial_check.opt_undefined_gen in
   Initial_check.opt_undefined_gen := false;
   let registers = find_registers defs in
-  let def_ids = ids_of_defs (Defs defs) in
-  let has_def name = IdSet.mem (mk_id name) def_ids in
   let regtyps = register_base_types mwords (List.map fst registers) in
   let option_typ =
-    if has_def "option" then [] else
+    if is_defined defs "option" then [] else
       ["union option ('a : Type) = {None : unit, Some : 'a}"]
   in
-  let regval_typ = if has_def "register_value" then [] else generate_regval_typ regtyps in
-  let regstate_typ = if has_def "regstate" then [] else generate_regstate registers in
+  let regval_typ = if is_defined defs "register_value" then [] else generate_regval_typ regtyps in
+  let regstate_typ = if is_defined defs "regstate" then [] else generate_regstate registers in
+  let initregstate = if is_defined defs "initial_regstate" then [] else generate_initial_regstate defs in
   let defs =
-    option_typ @ regval_typ @ regstate_typ
+    option_typ @ regval_typ @ regstate_typ @ initregstate
     |> List.map defs_of_string
     |> concat_ast
     |> Bindings.fold add_regval_conv regtyps
diff --git a/src/type_check.mli b/src/type_check.mli
index ed240839..a5d38363 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -283,6 +283,9 @@ val string_of_uvar : uvar -> string
 
 val subst_unifiers : uvar KBindings.t -> typ -> typ
 
+val typ_subst_nexp : kid -> nexp_aux -> typ -> typ
+val typ_subst_typ : kid -> typ_aux -> typ -> typ
+val typ_subst_order : kid -> order_aux -> typ -> typ
 val typ_subst_kid : kid -> kid -> typ -> typ
 
 val unify : l -> Env.t -> typ -> typ -> uvar KBindings.t * kid list * n_constraint option
-- 
cgit v1.2.3


From c3f3642dfa5647685ae3dea86beeef8abc27f026 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 4 May 2018 17:44:07 +0100
Subject: Support short-circuiting of Boolean expressions in Lem

---
 src/gen_lib/prompt.lem  |  6 +++++
 src/pretty_print_lem.ml | 63 +++++++++++++++++++++++--------------------------
 src/rewrites.ml         | 10 +++++++-
 3 files changed, 45 insertions(+), 34 deletions(-)

(limited to 'src')

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index de683047..830f2350 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -38,6 +38,12 @@ end
 
 declare {isabelle} termination_argument foreachM = automatic
 
+val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
+let and_boolM l r = l >>= (fun l -> if l then r else return false)
+
+val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
+let or_boolM l r = l >>= (fun l -> if l then return true else r)
+
 val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e
 let bool_of_bitU_fail = function
   | B0 -> return false
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f58c3fa6..f6b2fa87 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -551,10 +551,11 @@ let doc_exp_lem, doc_let_lem =
     let expY = top_exp ctxt true in
     let expN = top_exp ctxt false in
     let expV = top_exp ctxt in
+    let wrap_parens doc = if aexp_needed then parens (doc) else doc in
     let liftR doc =
       if ctxt.early_ret && effectful (effect_of full_exp)
-      then separate space [string "liftR"; parens (doc)]
-      else doc in
+      then wrap_parens (separate space [string "liftR"; parens (doc)])
+      else wrap_parens doc in
     match e with
     | E_assign((LEXP_aux(le_act,tannot) as le), e) ->
        (* can only be register writes *)
@@ -619,20 +620,21 @@ let doc_exp_lem, doc_let_lem =
       raise (Reporting_basic.err_unreachable l
         "E_vector_append should have been rewritten before pretty-printing")
     | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
-    | E_if(c,t,e) ->
-       let epp = if_exp ctxt false c t e in
-       if aexp_needed then parens (align epp) else epp
+    | E_if(c,t,e) -> wrap_parens (align (if_exp ctxt false c t e))
     | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
        raise (report l "E_for should have been rewritten before pretty-printing")
     | E_loop _ ->
        raise (report l "E_loop should have been rewritten before pretty-printing")
     | E_let(leb,e) ->
-       let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
-       if aexp_needed then parens epp else epp
+       wrap_parens (let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e)
     | E_app(f,args) ->
        begin match f with
-       (* temporary hack to make the loop body a function of the temporary variables *)
        | Id_aux (Id "None", _) as none -> doc_id_lem_ctor none
+       | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _)
+         when effectful (effect_of full_exp) ->
+          let call = doc_id_lem (append_id f "M") in
+          wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args)))
+       (* temporary hack to make the loop body a function of the temporary variables *)
        | Id_aux (Id "foreach", _) ->
           begin
             match args with
@@ -743,7 +745,7 @@ let doc_exp_lem, doc_let_lem =
                | _ ->
                   doc_id_lem_ctor f ^^ space ^^ 
                     parens (separate_map comma (expV false) args) in
-             if aexp_needed then parens (align epp) else epp
+             wrap_parens (align epp)
           | _ ->
              let call, is_extern = match annot with
                | Some (env, _, _) when Env.is_extern f env "lem" ->
@@ -796,8 +798,7 @@ let doc_exp_lem, doc_let_lem =
        else if is_ctor env id then doc_id_lem_ctor id
        else doc_id_lem id
     | E_lit lit -> doc_lit_lem lit
-    | E_cast(typ,e) ->
-       expV aexp_needed e
+    | E_cast(typ,e) -> expV aexp_needed e
     | E_tuple exps ->
        parens (align (group (separate_map (comma ^^ break 1) expN exps)))
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
@@ -807,10 +808,9 @@ let doc_exp_lem, doc_let_lem =
            (* when Env.is_record tid env -> *)
            tid
          | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
-       let epp = anglebars (space ^^ (align (separate_map
-                                          (semi_sp ^^ break 1)
-                                          (doc_fexp ctxt recordtyp) fexps)) ^^ space) in
-       if aexp_needed then parens epp else epp
+       wrap_parens (anglebars (space ^^ (align (separate_map
+                                        (semi_sp ^^ break 1)
+                                        (doc_fexp ctxt recordtyp) fexps)) ^^ space))
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
        let recordtyp = match annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
@@ -829,7 +829,7 @@ let doc_exp_lem, doc_let_lem =
        let start = match nexp_simp start with
          | Nexp_aux (Nexp_constant i, _) -> Big_int.to_string i
          | _ -> if dir then "0" else string_of_int (List.length exps) in
-       let expspp =
+       (* let expspp =
          match exps with
          | [] -> empty
          | e :: es ->
@@ -840,7 +840,8 @@ let doc_exp_lem, doc_let_lem =
                      expN e),
                   if count = 20 then 0 else count + 1)
                 (expN e,0) es in
-            align (group expspp) in
+            align (group expspp) in *)
+       let expspp = align (group (flow_map (semi ^^ break 0) expN exps)) in
        let epp = brackets expspp in
        let (epp,aexp_needed) =
          if is_bit_typ etyp && !opt_mwords then
@@ -858,28 +859,24 @@ let doc_exp_lem, doc_let_lem =
        brackets (separate_map semi (expN) exps)
     | E_case(e,pexps) ->
        let only_integers e = expY e in
-       let epp =
-         group ((separate space [string "match"; only_integers e; string "with"]) ^/^
-                  (separate_map (break 1) (doc_case ctxt) pexps) ^/^
-                    (string "end")) in
-       if aexp_needed then parens (align epp) else align epp
+       wrap_parens
+         (group ((separate space [string "match"; only_integers e; string "with"]) ^/^
+                 (separate_map (break 1) (doc_case ctxt) pexps) ^/^
+                 (string "end")))
     | E_try (e, pexps) ->
        if effectful (effect_of e) then
          let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in
-         let epp =
-           group ((separate space [string try_catch; expY e; string "(function "]) ^/^
-                    (separate_map (break 1) (doc_case ctxt) pexps) ^/^
-                      (string "end)")) in
-         if aexp_needed then parens (align epp) else align epp
+         wrap_parens
+           (group ((separate space [string try_catch; expY e; string "(function "]) ^/^
+                   (separate_map (break 1) (doc_case ctxt) pexps) ^/^
+                   (string "end)")))
        else
          raise (Reporting_basic.err_todo l "Warning: try-block around pure expression")
     | E_throw e ->
-       let epp = liftR (separate space [string "throw"; expY e]) in
-       if aexp_needed then parens (align epp) else align epp
+       align (liftR (separate space [string "throw"; expY e]))
     | E_exit e -> liftR (separate space [string "exit"; expY e])
     | E_assert (e1,e2) ->
-       let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in
-       if aexp_needed then parens (align epp) else align epp
+       align (liftR (separate space [string "assert_exp"; expY e1; expY e2]))
     | E_app_infix (e1,id,e2) ->
        raise (Reporting_basic.err_unreachable l
          "E_app_infix should have been rewritten before pretty-printing")
@@ -905,9 +902,9 @@ let doc_exp_lem, doc_let_lem =
          in
          infix 0 1 middle (expV b e1) (expN e2)
        in
-       if aexp_needed then parens (align epp) else epp
+       wrap_parens (align epp)
     | E_internal_return (e1) ->
-       separate space [string "return"; expY e1]
+       wrap_parens (align (separate space [string "return"; expY e1]))
     | E_sizeof nexp ->
       (match nexp_simp nexp with
         | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem (L_aux (L_num i, l))
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 582901dc..e779b059 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2581,6 +2581,14 @@ let rewrite_defs_letbind_effects =
     | E_cast (typ,exp') ->
        n_exp_name exp' (fun exp' ->
        k (rewrap (E_cast (typ,exp'))))
+    | E_app (op_bool, [l; r])
+      when string_of_id op_bool = "and_bool" || string_of_id op_bool = "or_bool" ->
+       (* Leave effectful operands of Boolean "and"/"or" in place to allow
+          short-circuiting. *)
+       let newreturn = effectful l || effectful r in
+       let l = n_exp_term newreturn l in
+       let r = n_exp_term newreturn r in
+       k (rewrap (E_app (op_bool, [l; r])))
     | E_app (id,exps) ->
        n_exp_nameL exps (fun exps ->
        k (rewrap (E_app (id,exps))))
@@ -2967,7 +2975,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          (* after rewrite_defs_letbind_effects c has no variable updates *)
          let env = env_of_annot annot in
          let typ = typ_of e1 in
-         let eff = union_eff_exps [e1;e2] in
+         let eff = union_eff_exps [c;e1;e2] in
          let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in
          Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
     | E_case (e1,ps) ->
-- 
cgit v1.2.3


From c6710bb09c1d492b4434f0b3b375750275b4d4b5 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 4 May 2018 17:46:10 +0100
Subject: Run ARM built-in tests for Lem backend (via OCaml)

---
 src/gen_lib/sail_operators.lem          | 12 ++++++++++++
 src/gen_lib/sail_operators_bitlists.lem | 17 +++++++++++++++++
 src/gen_lib/sail_operators_mwords.lem   | 17 +++++++++++++++++
 3 files changed, 46 insertions(+)

(limited to 'src')

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index d4275c87..78aab65e 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -223,3 +223,15 @@ let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedInteger
 
 val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
 let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r)
+
+val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
+let get_slice_int_bv len n lo =
+  let hi = lo + len - 1 in
+  let bs = bools_of_int (hi + 1) n in
+  of_bools (subrange_list false bs hi lo)
+
+val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer
+let set_slice_int_bv len n lo v =
+  let hi = lo + len - 1 in
+  let bs = bits_of_int (hi + 1) n in
+  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v)))
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index b0a29b5e..fed293b4 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -35,6 +35,9 @@ let zero_extend bits len = extz_bits len bits
 val sign_extend : list bitU -> integer -> list bitU
 let sign_extend bits len = exts_bits len bits
 
+val zeros : integer -> list bitU
+let zeros len = repeat [B0] len
+
 val vector_truncate : list bitU -> integer -> list bitU
 let vector_truncate bs len = extz_bv len bs
 
@@ -289,6 +292,20 @@ let duplicate_oracle b n =
 val reverse_endianness : list bitU -> list bitU
 let reverse_endianness v = reverse_endianness_list v
 
+val get_slice_int : integer -> integer -> integer -> list bitU
+let get_slice_int = get_slice_int_bv
+
+val set_slice_int : integer -> integer -> integer -> list bitU -> integer
+let set_slice_int = set_slice_int_bv
+
+val slice : list bitU -> integer -> integer -> list bitU
+let slice v lo len =
+  subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+  update_subrange_vec_dec out (n + slice_len - 1) n v
+
 val eq_vec    : list bitU -> list bitU -> bool
 val neq_vec   : list bitU -> list bitU -> bool
 val ult_vec   : list bitU -> list bitU -> bool
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 8bcc0319..077dfb02 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -76,6 +76,9 @@ let zero_extend w _ = Machine_word.zeroExtend w
 val sign_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
 let sign_extend w _ = Machine_word.signExtend w
 
+val zeros : forall 'a. Size 'a => integer -> mword 'a
+let zeros _ = Machine_word.wordFromNatural 0
+
 val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
 let vector_truncate w _ = Machine_word.zeroExtend w
 
@@ -310,6 +313,20 @@ let duplicate        b n = maybe_failwith (duplicate_maybe b n)
 val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
 let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v))
 
+val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
+let get_slice_int = get_slice_int_bv
+
+val set_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer
+let set_slice_int = set_slice_int_bv
+
+val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
+let slice v lo len =
+  subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : forall 'a 'b. Size 'a, Size 'b => integer -> integer -> mword 'a -> integer -> mword 'b -> mword 'a
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+  update_subrange_vec_dec out (n + slice_len - 1) n v
+
 val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-- 
cgit v1.2.3


From b6b46102fc49eae53c27d5d6540d41981c75da0c Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 8 May 2018 18:13:03 +0100
Subject: Add more annotations for loop bounds in Lem rewriting

Typechecking for-loops failed after the Lem rewriting passes in some cases: if
the lower bound for the loop may be greater than the upper bound, the loop
variable's type might be empty, and it cannot be initialised.  This patch adds
a guard "lower <= upper" around the loop body, and removes it again during
pretty-printing.
---
 src/pretty_print_lem.ml | 14 ++++++++------
 src/rewrites.ml         | 43 +++++++++++++++++++++++++++++++++++--------
 2 files changed, 43 insertions(+), 14 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f6b2fa87..c181249d 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -640,12 +640,14 @@ let doc_exp_lem, doc_let_lem =
             match args with
             | [exp1; exp2; exp3; ord_exp; vartuple; body] ->
                let loopvar, body = match body with
-                 | E_aux (E_let (LB_aux (LB_val (
-                     P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body
-                 | E_aux (E_let (LB_aux (LB_val (
-                     P_aux (P_var (P_aux (P_id id, _), _), _), _), _), body), _) -> id, body
-                 | E_aux (E_let (LB_aux (LB_val (
-                     P_aux (P_id id, _), _), _), body), _) -> id, body
+                 | E_aux (E_let (LB_aux (LB_val (_, _), _),
+                   E_aux (E_let (LB_aux (LB_val (_, _), _),
+                   E_aux (E_if (_,
+                   E_aux (E_let (LB_aux (LB_val (
+                     ((P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _))
+                     | (P_aux (P_var (P_aux (P_id id, _), _), _))
+                     | (P_aux (P_id id, _))), _), _),
+                     body), _), _), _)), _)), _) -> id, body
                  | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
                let step = match ord_exp with
                  | E_aux (E_lit (L_aux (L_false, _)), _) ->
diff --git a/src/rewrites.ml b/src/rewrites.ml
index e779b059..b59a248e 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2924,20 +2924,21 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          |> mk_var_exps_pats pl env
        in
        let exp4 = rewrite_var_updates (add_vars overwrite exp4 vars) in
-       let ord_exp, kids, constr, lower, upper =
-         match destruct_range env (typ_of exp1), destruct_range env (typ_of exp2) with
+       let ord_exp, kids, constr, lower, upper, lower_exp, upper_exp =
+         match destruct_numeric env (typ_of exp1), destruct_numeric env (typ_of exp2) with
            | None, _ | _, None ->
               raise (Reporting_basic.err_unreachable el "Could not determine loop bounds")
-           | Some (kids1, constr1, l1, u1), Some (kids2, constr2, l2, u2) ->
+           | Some (kids1, constr1, n1), Some (kids2, constr2, n2) ->
               let kids = kids1 @ kids2 in
               let constr = nc_and constr1 constr2 in
-              let ord_exp, lower, upper =
+              let ord_exp, lower, upper, lower_exp, upper_exp =
                 if is_order_inc order
-                then (annot_exp (E_lit (mk_lit L_true)) el env bool_typ, l1, u2)
-                else (annot_exp (E_lit (mk_lit L_false)) el env bool_typ, l2, u1)
+                then (annot_exp (E_lit (mk_lit L_true)) el env bool_typ, n1, n2, exp1, exp2)
+                else (annot_exp (E_lit (mk_lit L_false)) el env bool_typ, n2, n1, exp2, exp1)
               in
-              ord_exp, kids, constr, lower, upper
+              ord_exp, kids, constr, lower, upper, lower_exp, upper_exp
        in
+       (* Bind the loop variable in the body, annotated with constraints *)
        let lvar_kid = mk_kid ("loop_" ^ string_of_id id) in
        let lvar_nc = nc_and constr (nc_and (nc_lteq lower (nvar lvar_kid)) (nc_lteq (nvar lvar_kid) upper)) in
        let lvar_typ = mk_typ (Typ_exist (lvar_kid :: kids, lvar_nc, atom_typ (nvar lvar_kid))) in
@@ -2946,7 +2947,33 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
          TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ)) in
        let lb = fix_eff_lb (annot_letbind (lvar_pat, exp1) el env lvar_typ) in
        let body = fix_eff_exp (annot_exp (E_let (lb, exp4)) el env (typ_of exp4)) in
-       let v = fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; body])) el env (typ_of body)) in
+       (* If lower > upper, the loop body never gets executed, and the type
+          checker might not be able to prove that the initial value exp1
+          satisfies the constraints on the loop variable.
+
+          Make this explicit by guarding the loop body with lower <= upper.
+          (for type-checking; the guard is later removed again by the Lem
+          pretty-printer).  This could be implemented with an assertion, but
+          that would force the loop to be effectful, so we use an if-expression
+          instead.  This code assumes that the loop bounds have (possibly
+          existential) atom types, and the loop body has type unit. *)
+       let lower_kid = mk_kid ("loop_" ^ string_of_id id ^ "_lower") in
+       let lower_pat = P_var (annot_pat P_wild el env (typ_of lower_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var lower_kid)]))) in
+       let lb_lower = annot_letbind (lower_pat, lower_exp) el env (typ_of lower_exp) in
+       let upper_kid = mk_kid ("loop_" ^ string_of_id id ^ "_upper") in
+       let upper_pat = P_var (annot_pat P_wild el env (typ_of upper_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var upper_kid)]))) in
+       let lb_upper = annot_letbind (upper_pat, upper_exp) el env (typ_of upper_exp) in
+       let guard = annot_exp (E_constraint (nc_lteq (nvar lower_kid) (nvar upper_kid))) el env bool_typ in
+       let unit_exp = annot_exp (E_lit (mk_lit L_unit)) el env unit_typ in
+       let skip_val = tuple_exp (if overwrite then vars else unit_exp :: vars) in
+       let guarded_body =
+         fix_eff_exp (annot_exp (E_let (lb_lower,
+           fix_eff_exp (annot_exp (E_let (lb_upper,
+             fix_eff_exp (annot_exp (E_if (guard, body, skip_val))
+               el env (typ_of exp4))))
+             el env (typ_of exp4))))
+           el env (typ_of exp4)) in
+       let v = fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body])) el env (typ_of body)) in
        Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats))
      | E_loop(loop,cond,body) ->
         let vars, varpats =
-- 
cgit v1.2.3


From 972d349919fc5ebe911604330ea3c80e70fdcfad Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 8 May 2018 18:48:18 +0100
Subject: Add tests for Isabelle->OCaml generation for CHERI and AArch64

---
 src/gen_lib/state_monad.lem | 13 +++++++++++++
 src/type_check.mli          |  2 ++
 2 files changed, 15 insertions(+)

(limited to 'src')

diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index 8253b800..a2919762 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -265,3 +265,16 @@ let update_reg_field_bit regfield i reg_val bit =
   let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in
   regfield.set_field reg_val new_field_value
 let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)*)
+
+(* TODO Add Show typeclass for value and exception type *)
+val show_result : forall 'a 'e. result 'a 'e -> string
+let show_result = function
+  | Value _ -> "Value ()"
+  | Ex (Failure msg) -> "Failure " ^ msg
+  | Ex (Throw _) -> "Throw"
+end
+
+val prerr_results : forall 'a 'e 's. SetType 's => set (result 'a 'e * 's) -> unit
+let prerr_results rs =
+  let _ = Set.map (fun (r, _) -> let _ = prerr_endline (show_result r) in ()) rs in
+  ()
diff --git a/src/type_check.mli b/src/type_check.mli
index a5d38363..1c0e2f09 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -271,6 +271,8 @@ val destruct_exist : Env.t -> typ -> (kid list * n_constraint * typ) option
 
 val destruct_range : Env.t -> typ -> (kid list * n_constraint * nexp * nexp) option
 
+val destruct_numeric : Env.t -> typ -> (kid list * n_constraint * nexp) option
+
 val destruct_vector : Env.t -> typ -> (nexp * order * typ) option
 
 type uvar =
-- 
cgit v1.2.3


From c498c8a7f8d448dcefd1692e7562878cc6feb62b Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 9 May 2018 16:51:17 +0100
Subject: Fix printing of hex strings in Lem

---
 src/gen_lib/sail_values.lem | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src')

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 2d9eda9c..5c6dc593 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -414,6 +414,7 @@ let rec hexstring_of_bits bs = match bs with
      | (Just n, Just s) -> Just (n :: s)
      | _ -> Nothing
      end
+  | [] -> Just []
   | _ -> Nothing
   end
 declare {isabelle} termination_argument hexstring_of_bits = automatic
-- 
cgit v1.2.3


From 0d56f6be9e2e437c570da05b1c8cdc25eb24912c Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 9 May 2018 16:55:58 +0100
Subject: Fix an issue with C compilation

---
 src/c_backend.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 5cf282f9..23a8c92e 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1927,7 +1927,7 @@ and compile_block ctx = function
      let setup, _, call, cleanup = compile_aexp ctx exp in
      let rest = compile_block ctx exps in
      let gs = gensym () in
-     setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup @ rest
+     iblock (setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup) :: rest
 
 (** Compile a sail type definition into a IR one. Most of the
    actual work of translating the typedefs into C is done by the code
-- 
cgit v1.2.3


From 9efeea3c2179a182feb07c6b4e640674f149331f Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Wed, 2 May 2018 10:31:00 +0100
Subject: Add language=sail option in listings command for latex output. This
 helps with documents containing listings in multiple languages.

---
 src/latex.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index 01cf55b2..f16dddd8 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -134,7 +134,7 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l
       let oc = open_out (Filename.concat dir (cmd ^ "_sail.tex")) in
       output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l));
       close_out oc;
-      string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting{%s/%s_sail.tex}}" dir cmd)
+      string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s_sail.tex}}" dir cmd)
     end
 
 let latex_command_id ?prefix:(prefix="") dir id no_loc annot =
-- 
cgit v1.2.3


From 6846d314b5fdc90d7c3a3ee656ebbf12cbdf7f8d Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 10 May 2018 17:40:48 +0100
Subject: latex: don't include the prefix in the label. This means we have the
 option of omitting valspec in documentation if it is deemed too verbose and
 still have hyperlinks work. The caveat is that it could result in multiply
 defined labels.

---
 src/latex.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index f16dddd8..8688eaa8 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -123,7 +123,7 @@ let commands = ref StringSet.empty
 let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l, _) as annot) =
   let labelling = match label with
     | None -> ""
-    | Some l -> Printf.sprintf "\\label{%s%s}" prefix l
+    | Some l -> Printf.sprintf "\\label{%s}" l
   in
   let cmd = !opt_prefix_latex ^ prefix ^ cmd in
   if StringSet.mem cmd !commands then
-- 
cgit v1.2.3


From 619bd9b568f6f8f5691a66602b7635834d3d13a2 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 11 May 2018 11:31:47 +0100
Subject: Avoid generating latex files that differ only by case because this
 causes confusion on case insensitive file systems (e.g. mac).

---
 src/latex.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index 8688eaa8..3233a4ac 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -126,11 +126,12 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l
     | Some l -> Printf.sprintf "\\label{%s}" l
   in
   let cmd = !opt_prefix_latex ^ prefix ^ cmd in
-  if StringSet.mem cmd !commands then
+  let lcmd = String.lowercase cmd in  (* lowercase to avoid file names differing only by case *)
+  if StringSet.mem lcmd !commands then
     latex_command ~label:label dir (cmd ^ "v") no_loc annot
   else
     begin
-      commands := StringSet.add cmd !commands;
+      commands := StringSet.add lcmd !commands;
       let oc = open_out (Filename.concat dir (cmd ^ "_sail.tex")) in
       output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l));
       close_out oc;
-- 
cgit v1.2.3


From 17c786ea27bf644efdae271b8a93bd5ce1d730e8 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 11 May 2018 11:32:31 +0100
Subject: Remove unneeded _sail suffix from latex files.

---
 src/latex.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/latex.ml b/src/latex.ml
index 3233a4ac..0520d074 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -132,10 +132,10 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l
   else
     begin
       commands := StringSet.add lcmd !commands;
-      let oc = open_out (Filename.concat dir (cmd ^ "_sail.tex")) in
+      let oc = open_out (Filename.concat dir (cmd ^ ".tex")) in
       output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l));
       close_out oc;
-      string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s_sail.tex}}" dir cmd)
+      string (Printf.sprintf "\\newcommand{\\%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting[language=sail]{%s/%s.tex}}" dir cmd)
     end
 
 let latex_command_id ?prefix:(prefix="") dir id no_loc annot =
-- 
cgit v1.2.3


From db3b6d21c18f4ac516c2554db6890274d2b8292c Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 10 May 2018 14:23:49 +0100
Subject: Remove buggy bit list comparison functions from Lem library

Found bugs by running CHERI test suite on Isabelle-exported model:  signed
less-than for bit lists was missing negations for the two's complement, and
unsigned less-than compared the reverse lists.

Since all other backends implement this in Sail, it seems best to just remove
this code.

Also add support for infix operators to Lem backend, by z-encoding their
identifiers like the other backends do.
---
 src/gen_lib/sail_operators.lem          | 30 ------------------------------
 src/gen_lib/sail_operators_bitlists.lem | 16 ----------------
 src/gen_lib/sail_operators_mwords.lem   | 16 ----------------
 src/pretty_print_lem.ml                 | 22 ++++++++--------------
 4 files changed, 8 insertions(+), 76 deletions(-)

(limited to 'src')

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 78aab65e..0c5da675 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -194,36 +194,6 @@ let neq_bv l r = not (eq_bv l r)
 
 let inline neq_mword l r = (l <> r)
 
-val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let ult_bv l r = lexicographicLess (List.reverse (bits_of l)) (List.reverse (bits_of r))
-let ulteq_bv l r = (eq_bv l r) || (ult_bv l r)
-let ugt_bv l r = not (ulteq_bv l r)
-let ugteq_bv l r = (eq_bv l r) || (ugt_bv l r)
-
-val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let slt_bv l r =
-  match (most_significant l, most_significant r) with
-    | (B0, B0) -> ult_bv l r
-    | (B0, B1) -> false
-    | (B1, B0) -> true
-    | (B1, B1) ->
-       let l' = add_one_bit_ignore_overflow (bits_of l) in
-       let r' = add_one_bit_ignore_overflow (bits_of r) in
-       ugt_bv l' r'
-    | (BU, BU) -> ult_bv l r
-    | (BU, _) -> true
-    | (_, BU) -> false
-  end
-let slteq_bv l r = (eq_bv l r) || (slt_bv l r)
-let sgt_bv l r = not (slteq_bv l r)
-let sgteq_bv l r = (eq_bv l r) || (sgt_bv l r)
-
-val ucmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
-let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedIntegerFromWord r)
-
-val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
-let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r)
-
 val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
 let get_slice_int_bv len n lo =
   let hi = lo + len - 1 in
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index fed293b4..19e9b519 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -308,21 +308,5 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
 
 val eq_vec    : list bitU -> list bitU -> bool
 val neq_vec   : list bitU -> list bitU -> bool
-val ult_vec   : list bitU -> list bitU -> bool
-val slt_vec   : list bitU -> list bitU -> bool
-val ugt_vec   : list bitU -> list bitU -> bool
-val sgt_vec   : list bitU -> list bitU -> bool
-val ulteq_vec : list bitU -> list bitU -> bool
-val slteq_vec : list bitU -> list bitU -> bool
-val ugteq_vec : list bitU -> list bitU -> bool
-val sgteq_vec : list bitU -> list bitU -> bool
 let eq_vec    = eq_bv
 let neq_vec   = neq_bv
-let ult_vec   = ult_bv
-let slt_vec   = slt_bv
-let ugt_vec   = ugt_bv
-let sgt_vec   = sgt_bv
-let ulteq_vec = ulteq_bv
-let slteq_vec = slteq_bv
-let ugteq_vec = ugteq_bv
-let sgteq_vec = sgteq_bv
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 077dfb02..22d5b246 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -329,21 +329,5 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
 
 val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val slt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ugt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val sgt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 let inline eq_vec    = eq_mword
 let inline neq_vec   = neq_mword
-let inline ult_vec   = ucmp_mword (<)
-let inline slt_vec   = scmp_mword (<)
-let inline ugt_vec   = ucmp_mword (>)
-let inline sgt_vec   = scmp_mword (>)
-let inline ulteq_vec = ucmp_mword (<=)
-let inline slteq_vec = scmp_mword (<=)
-let inline ugteq_vec = ucmp_mword (>=)
-let inline sgteq_vec = scmp_mword (>=)
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index c181249d..58bbfc4b 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -111,10 +111,7 @@ let rec fix_id remove_tick name = match name with
 let doc_id_lem (Id_aux(i,_)) =
   match i with
   | Id i -> string (fix_id false i)
-  | DeIid x ->
-     (* add an extra space through empty to avoid a closing-comment
-      * token in case of x ending with star. *)
-     parens (separate space [colon; string x; empty])
+  | DeIid x -> string (Util.zencode_string ("op " ^ x))
 
 let doc_id_lem_type (Id_aux(i,_)) =
   match i with
@@ -122,10 +119,7 @@ let doc_id_lem_type (Id_aux(i,_)) =
   | Id("nat") -> string "ii"
   | Id("option") -> string "maybe"
   | Id i -> string (fix_id false i)
-  | DeIid x ->
-     (* add an extra space through empty to avoid a closing-comment
-      * token in case of x ending with star. *)
-     parens (separate space [colon; string x; empty])
+  | DeIid x -> string (Util.zencode_string ("op " ^ x))
 
 let doc_id_lem_ctor (Id_aux(i,_)) =
   match i with
@@ -135,10 +129,11 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
   | Id("Some") -> string "Just"
   | Id("None") -> string "Nothing"
   | Id i -> string (fix_id false (String.capitalize i))
-  | DeIid x ->
-     (* add an extra space through empty to avoid a closing-comment
-      * token in case of x ending with star. *)
-     separate space [colon; string (String.capitalize x); empty]
+  | DeIid x -> string (Util.zencode_string ("op " ^ x))
+
+let deinfix = function
+  | Id_aux (Id v, l) -> Id_aux (DeIid v, l)
+  | Id_aux (DeIid v, l) -> Id_aux (DeIid v, l)
 
 let doc_var_lem kid = string (fix_id true (string_of_kid kid))
 
@@ -880,8 +875,7 @@ let doc_exp_lem, doc_let_lem =
     | E_assert (e1,e2) ->
        align (liftR (separate space [string "assert_exp"; expY e1; expY e2]))
     | E_app_infix (e1,id,e2) ->
-       raise (Reporting_basic.err_unreachable l
-         "E_app_infix should have been rewritten before pretty-printing")
+       expV aexp_needed (E_aux (E_app (deinfix id, [e1; e2]), (l, annot)))
     | E_var(lexp, eq_exp, in_exp) ->
        raise (report l "E_vars should have been removed before pretty-printing")
     | E_internal_plet (pat,e1,e2) ->
-- 
cgit v1.2.3