Various bugfixes and a simple profiling feature for rewrites

11 files changed, 144 insertions, 11 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index e61ec473..db011f14 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -57,13 +57,13 @@ let elsize = shl_int(8, UInt(size))
 ```
 THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}`
 */
-val _shl8 = "shl_int" :
+val _shl8 = {c: "shl_mach_int", _: "shl_int"} :
   forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64}
 
 /*!
 Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}`
 */
-val _shl32 = "shl_int" :
+val _shl32 = {c: "shl_mach_int", _: "shl_int"} :
   forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64}
 
 val _shl_int = "shl_int" : (int, int) -> int
diff --git a/lib/rts.c b/lib/rts.c
index 6bd97934..2f594ff8 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -94,6 +94,10 @@ void write_mem(uint64_t address, uint64_t byte)
   uint64_t mask = address & ~MASK;
   uint64_t offset = address & MASK;
 
+  //if ((byte >= 97 && byte <= 122) || (byte >= 64 && byte <= 90) || (byte >= 48 && byte <= 57) || byte == 10 || byte == 32) {
+  //  fprintf(stderr, "%c", (char) byte);
+  //}
+
   struct block *current = sail_memory;
 
   while (current != NULL) {
diff --git a/lib/sail.c b/lib/sail.c
index 94cd5c2c..fc11a40d 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -291,6 +291,12 @@ void shl_int(sail_int *rop, const sail_int op1, const sail_int op2)
 }
 
 inline
+mach_int shl_mach_int(const mach_int op1, const mach_int op2)
+{
+  return op1 << op2;
+}
+
+inline
 void shr_int(sail_int *rop, const sail_int op1, const sail_int op2)
 {
   mpz_fdiv_q_2exp(*rop, op1, mpz_get_ui(op2));
@@ -446,6 +452,11 @@ void CREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const ui
   mpz_init_set_ui(*rop->bits, op);
 }
 
+mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits op)
+{
+  return mpz_get_ui(*op.bits);
+}
+
 void RECREATE_OF(sail_bits, mach_bits)(sail_bits *rop, const uint64_t op, const uint64_t len, const bool direction)
 {
   rop->len = len;
diff --git a/lib/sail.h b/lib/sail.h
index 4ccd8b93..b3386198 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -131,6 +131,7 @@ bool gteq(const sail_int, const sail_int);
 /*
  * Left and right shift for integers
  */
+mach_int shl_mach_int(const mach_int, const mach_int);
 SAIL_INT_FUNCTION(shl_int, sail_int, const sail_int, const sail_int);
 SAIL_INT_FUNCTION(shr_int, sail_int, const sail_int, const sail_int);
 
@@ -192,6 +193,8 @@ void RECREATE_OF(sail_bits, mach_bits)(sail_bits *,
 				       const mach_bits len,
 				       const bool direction);
 
+mach_bits CREATE_OF(mach_bits, sail_bits)(const sail_bits);
+
 mach_bits CONVERT_OF(mach_bits, sail_bits)(const sail_bits, const bool);
 void CONVERT_OF(sail_bits, mach_bits)(sail_bits *, const mach_bits, const uint64_t, const bool);
 
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 0c4ae87d..97477163 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -306,7 +306,9 @@ let rec c_aval ctx = function
               else
                 v (* id's type went from heap -> stack due to flow typing, so it's really still heap allocated! *)
             with
-              Not_found -> failwith ("could not find " ^ string_of_id id ^ " in local variables")
+              (* Hack: Assuming global letbindings don't change from flow typing... *)
+              Not_found -> AV_C_fragment (F_id id, typ)
+              (* failwith ("could not find " ^ string_of_id id ^ " in local variables") *)
           end
        | Register (_, _, typ) when is_stack_typ ctx typ ->
           AV_C_fragment (F_id id, typ)
@@ -427,9 +429,11 @@ let analyze_primop' ctx id args typ =
      | _ -> no_change
      end
 
+       (*
   | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] when is_stack_typ ctx typ ->
      let len = F_op (f, "-", F_op (t, "-", v_one)) in
      AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ))
+        *)
 
   | "vector_access", [AV_C_fragment (vec, _); AV_C_fragment (n, _)] ->
      AE_val (AV_C_fragment (F_op (v_one, "&", F_op (vec, ">>", n)), typ))
@@ -437,8 +441,10 @@ let analyze_primop' ctx id args typ =
   | "eq_bit", [AV_C_fragment (a, _); AV_C_fragment (b, _)] ->
      AE_val (AV_C_fragment (F_op (a, "==", b), typ))
 
+            (*
   | "slice", [AV_C_fragment (vec, _); AV_C_fragment (start, _); AV_C_fragment (len, _)] ->
      AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", start)), typ))
+             *)
 
   | "undefined_bit", _ ->
      AE_val (AV_C_fragment (F_lit (V_bit Sail2_values.B0), typ))
@@ -2727,7 +2733,7 @@ let codegen_vector ctx (direction, ctyp) =
       ^^ string (Printf.sprintf "  rop->data = malloc(len * sizeof(%s));\n" (sgen_ctyp ctyp))
       ^^ (if not (is_stack_ctyp ctyp) then
             string "  for (int i = 0; i < len; i++) {\n"
-            ^^ string (Printf.sprintf "    CREATE(%s)((rop->data) + i);\n" (sgen_ctyp ctyp))
+            ^^ string (Printf.sprintf "    CREATE(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp))
             ^^ string "  }\n"
           else empty)
       ^^ string "}"
diff --git a/src/constraint.ml b/src/constraint.ml
index d66705b6..cf861423 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -219,7 +219,7 @@ let save_digests () =
   DigestMap.iter output !known_problems;
   close_out out_chan
 
-let rec call_z3 constraints : smt_result =
+let call_z3' constraints : smt_result =
   let problems = [constraints] in
   let z3_file = smtlib_of_constraints constraints in
 
@@ -261,6 +261,12 @@ let rec call_z3 constraints : smt_result =
          else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown)
     end
 
+let call_z3 constraints =
+  let t = Profile.start_z3 () in
+  let result = call_z3' constraints in
+  Profile.finish_z3 t;
+  result
+
 let rec solve_z3 constraints var =
   let problems = [constraints] in
   let z3_file = smtlib_of_constraints ~get_model:true constraints in
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 3ad4c07f..9a48421a 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -359,10 +359,10 @@ and ocaml_assignment ctx (LEXP_aux (lexp_aux, _) as lexp) exp =
             else ocaml_atomic_exp ctx exp
           in
           separate space [zencode ctx id; string ":="; traced_exp]
-       | _ -> separate space [zencode ctx id; string ":="; ocaml_exp ctx exp]
+       | _ -> separate space [zencode ctx id; string ":="; parens (ocaml_exp ctx exp)]
      end
   | LEXP_deref ref_exp ->
-     separate space [ocaml_atomic_exp ctx ref_exp; string ":="; ocaml_exp ctx exp]
+     separate space [ocaml_atomic_exp ctx ref_exp; string ":="; parens (ocaml_exp ctx exp)]
   | _ -> string ("LEXP<" ^ string_of_lexp lexp ^ ">")
 and ocaml_lexp ctx (LEXP_aux (lexp_aux, _) as lexp) =
   match lexp_aux with
@@ -933,7 +933,7 @@ let ocaml_main spec sail_dir =
    @ [ "  zinitializze_registers ();";
        if !opt_trace_ocaml then "  Sail_lib.opt_trace := true;" else "  ();";
        "  Printexc.record_backtrace true;";
-       "  try zmain () with _ -> prerr_endline(\"Exiting due to uncaught exception\")\n";])
+       "  try zmain () with exn -> prerr_endline(\"Exiting due to uncaught exception:\\n\" ^ Printexc.to_string exn)\n";])
   |> String.concat "\n"
 
 let ocaml_pp_defs f defs generator_types =
diff --git a/src/process_file.ml b/src/process_file.ml
index bb789d0a..53293849 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -364,8 +364,10 @@ let output libpath out_arg files =
       output1 libpath out_arg f defs)
     files
 
-let rewrite_step defs (name,rewriter) =
+let rewrite_step defs (name, rewriter) =
+  let t = Profile.start () in
   let defs = rewriter defs in
+  Profile.finish ("rewrite " ^ name) t;
   let _ = match !(opt_ddump_rewrite_ast) with
     | Some (f, i) ->
       begin
diff --git a/src/profile.ml b/src/profile.ml
new file mode 100644
index 00000000..cb374403
--- /dev/null
+++ b/src/profile.ml
@@ -0,0 +1,91 @@
+(**************************************************************************)
+(*     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.                                                          *)
+(**************************************************************************)
+
+let opt_profile = ref false
+
+type profile = {
+    z3_calls : int;
+    z3_time : float
+  }
+
+let new_profile = {
+    z3_calls = 0;
+    z3_time = 0.0
+  }
+
+let profile_stack = ref []
+
+let update_profile f =
+  match !profile_stack with
+  | [] -> ()
+  | (p :: ps) ->
+     profile_stack := f p :: ps
+
+let start_z3 () =
+  update_profile (fun p -> { p with z3_calls = p.z3_calls + 1 });
+  Sys.time ()
+
+let finish_z3 t =
+  update_profile (fun p -> { p with z3_time = p.z3_time +. (Sys.time () -. t) })
+
+let start () =
+  profile_stack := new_profile :: !profile_stack;
+  Sys.time ()
+
+let finish msg t =
+  if !opt_profile then
+    begin match !profile_stack with
+    | p :: ps ->
+       prerr_endline (Printf.sprintf "%s %s: %fs" Util.("Profile" |> magenta |> clear) msg (Sys.time () -. t));
+       prerr_endline (Printf.sprintf "  Z3 calls: %d, Z3 time: %fs" p.z3_calls p.z3_time);
+       profile_stack := ps
+    | [] -> ()
+    end
+  else ()
diff --git a/src/rewrites.ml b/src/rewrites.ml
index c274ded4..591b86a7 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -2591,7 +2591,10 @@ let rewrite_tuple_assignments defs =
        let (_, ids) = List.fold_left (fun (n, ids) _ -> (n + 1, ids @ [mk_id ("tup__" ^ string_of_int n)])) (0, []) lexps in
        let block_assign i lexp = mk_exp (E_assign (strip_lexp lexp, mk_exp (E_id (mk_id ("tup__" ^ string_of_int i))))) in
        let block = mk_exp (E_block (List.mapi block_assign lexps)) in
-       let letbind = mk_letbind (mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))) (strip_exp exp) in
+       let letbind = mk_letbind (mk_pat (P_typ (Type_check.typ_of exp,
+                                                mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids)))))
+                                (strip_exp exp)
+       in
        let let_exp = mk_exp (E_let (letbind, block)) in
        begin
          try check_exp env let_exp unit_typ with
@@ -2641,7 +2644,7 @@ let rewrite_defs_remove_blocks =
   let e_aux = function
     | (E_block es,(l,_)) -> f l es
     | (e,annot) -> E_aux (e,annot) in
-    
+
   let alg = { id_exp_alg with e_aux = e_aux } in
 
   rewrite_defs_base
diff --git a/src/sail.ml b/src/sail.ml
index 3505ecf4..df095e0e 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -240,6 +240,9 @@ let options = Arg.align ([
   ( "-dfunction",
     Arg.String (fun f -> C_backend.opt_debug_function := f),
     " (debug) print debugging output for a single function");
+  ( "-dprofile",
+    Arg.Set Profile.opt_profile,
+    " (debug) provides basic profiling information for rewriting passes within Sail");
   ( "-Xconstraint_synonyms",
     Arg.Set Type_check.opt_constraint_synonyms,
     " (extension) allow constraint synonyms");
@@ -265,14 +268,18 @@ let interactive_env = ref Type_check.initial_env
 let load_files type_envs files =
   if !opt_memo_z3 then Constraint.load_digests () else ();
 
+  let t = Profile.start () in
   let parsed = List.map (fun f -> (f, parse_file f)) files in
   let ast =
     List.fold_right (fun (_, Parse_ast.Defs ast_nodes) (Parse_ast.Defs later_nodes)
                      -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
   let ast = Process_file.preprocess_ast options ast in
   let ast = convert_ast Ast_util.inc_ord ast in
+  Profile.finish "parsing" t;
 
+  let t = Profile.start () in
   let (ast, type_envs) = check_ast type_envs ast in
+  Profile.finish "type checking" t;
 
   let ast = rewrite_ast ast in