Improve builtins tests

Test the builtin functions by compiling them to C, OCaml, and OCaml
via Lem. Split up some of the longer builtin test programs to avoid
stack overflows when compiling to OCaml, as 3000+ line long blocks can
cause issues with some re-writing steps.

Also test constant-folding with builtins (this should reduce the
asserts in these files to assert true), and also test constant folding
with the C compilation.

Fix a bug whereby vectors with heap-allocated elements were not
initialized correctly.

Fix a bug caused by compiling and optimising empty vector literals.

Fix an OCaml test case that broke due to the ref type being used. Now
uses references to registers.

Fix a bug where Sail would output big integers that lem can't
parse. Checks if integer is between Int32.min_int and Int32.max_int
and if not, use integerOfString to represent the integer. Really this
should be fixed in Lem.

Make the python test runner script the default for testing builtins
and running the C compilation tests in test/run_tests.sh

Add a ocaml_build_dir option that sets a custom build directory for
OCaml. This is needed for running OCaml tests in parallel so the
builds don't clobber one another.

10 files changed, 51 insertions, 26 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index cb500f08..29d48543 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -709,7 +709,7 @@ let rec string_of_exp (E_aux (exp, _)) =
      "{ " ^ string_of_exp exp ^ " with " ^ string_of_list "; " string_of_fexp fexps ^ " }"
   | E_record (FES_aux (FES_Fexps (fexps, _), _)) ->
      "{ " ^ string_of_list "; " string_of_fexp fexps ^ " }"
-  | E_var _ -> "INTERNAL LET"
+  | E_var (lexp, binding, exp) -> "var " ^ string_of_lexp lexp ^ " = " ^ string_of_exp binding ^ " in " ^ string_of_exp exp
   | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")"
   | E_internal_plet (pat, exp, body) -> "internal_plet " ^ string_of_pat pat ^ " = " ^ string_of_exp exp ^ " in " ^ string_of_exp body
   | E_nondet _ -> "NONDET"
@@ -1237,7 +1237,8 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
 
     | E_return exp -> E_return (subst id value exp)
     | E_exit exp -> E_exit (subst id value exp)
-    (* Not sure about this, but id should always be immutable while id' must be mutable so should be ok. *)
+
+    (* id should always be immutable while id' must be mutable register name so should be ok to never substitute here *)
     | E_ref id' -> E_ref id'
     | E_throw exp -> E_throw (subst id value exp)
 
@@ -1247,7 +1248,10 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
     | E_assert (exp1, exp2) -> E_assert (subst id value exp1, subst id value exp2)
 
     | E_internal_value v -> E_internal_value v
-    | _ -> failwith ("subst " ^ string_of_exp exp)
+
+    | E_var (lexp, exp1, exp2) -> E_var (subst_lexp id value lexp, subst id value exp1, subst id value exp2)
+
+    | E_internal_plet _ | E_internal_return _ -> failwith ("subst " ^ string_of_exp exp)
   in
   wrap e_aux
 
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 3e674cfd..fa41e1e1 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -136,6 +136,7 @@ let rec frag_rename from_id to_id = function
 (**************************************************************************)
 
 let string_of_value = function
+  | V_bits [] -> "UINT64_C(0)"
   | V_bits bs -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
   | V_int i -> Big_int.to_string i ^ "l"
   | V_bool true -> "true"
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 265bb8d6..d79a2957 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -261,9 +261,12 @@ let c_literals ctx =
 let mask m =
   if Big_int.less_equal m (Big_int.of_int 64) then
     let n = Big_int.to_int m in
-    if n mod 4 == 0
-    then "UINT64_C(0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ ")"
-    else "UINT64_C(" ^ String.make (64 - n) '0' ^ String.make n '1' ^ ")"
+    if n = 0 then
+      "UINT64_C(0)"
+    else if n mod 4 = 0 then
+      "UINT64_C(0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ ")"
+    else
+      "UINT64_C(" ^ String.make (64 - n) '0' ^ String.make n '1' ^ ")"
   else
     failwith "Tried to create a mask literal for a vector greater than 64 bits."
 
@@ -1892,7 +1895,8 @@ let sort_ctype_defs cdefs =
        List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors
   in
 
-  (* Create a reverse id graph of dependencies between types *)
+  (* Create a reverse (i.e. from types to the types that are dependent
+     upon them) id graph of dependencies between types *)
   let module IdGraph = Graph.Make(Id) in
 
   let graph =
@@ -1989,9 +1993,6 @@ let optimize ctx cdefs =
 let sgen_id id = Util.zencode_string (string_of_id id)
 let codegen_id id = string (sgen_id id)
 
-let upper_sgen_id id = Util.zencode_string (string_of_id id)
-let upper_codegen_id id = string (upper_sgen_id id)
-
 let rec sgen_ctyp = function
   | CT_unit -> "unit"
   | CT_bit -> "mach_bits"
@@ -2268,10 +2269,10 @@ let codegen_type_def ctx = function
      in
      let codegen_undefined =
        let name = sgen_id id in
-       string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (upper_sgen_id first_id))
+       string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id))
      in
      string (Printf.sprintf "// enum %s" (string_of_id id)) ^^ hardline
-     ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) upper_codegen_id ids; rbrace ^^ semi]
+     ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) codegen_id ids; rbrace ^^ semi]
      ^^ twice hardline
      ^^ codegen_eq
      ^^ twice hardline
@@ -2664,6 +2665,11 @@ let codegen_vector ctx (direction, ctyp) =
       string (Printf.sprintf "static void internal_vector_init_%s(%s *rop, const int64_t len) {\n" (sgen_id id) (sgen_id id))
       ^^ string "  rop->len = len;\n"
       ^^ 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 "  }\n"
+          else empty)
       ^^ string "}"
     in
     let vector_undefined =
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 45d3efe0..20c0628d 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -61,7 +61,7 @@ let optimize_constant_fold = ref false
 
 let rec fexp_of_ctor (field, value) =
   FE_aux (FE_Fexp (mk_id field, exp_of_value value), no_annot)
-  
+
 and exp_of_value =
   let open Value in
   function
@@ -90,12 +90,16 @@ let safe_primops =
     [ "print_endline";
       "prerr_endline";
       "putchar";
+      "print";
+      "prerr";
       "print_bits";
       "print_int";
       "print_string";
       "prerr_bits";
       "prerr_int";
       "prerr_string";
+      "read_ram";
+      "write_ram";
       "Elf_loader.elf_entry";
       "Elf_loader.elf_tohost"
     ]
@@ -116,7 +120,6 @@ let rec run ast frame =
   match frame with
   | Interpreter.Done (state, v) -> v
   | Interpreter.Step (lazy_str, _, _, _) ->
-     prerr_endline (Lazy.force lazy_str);
      run ast (Interpreter.eval_frame ast frame)
   | Interpreter.Break frame ->
      run ast (Interpreter.eval_frame ast frame)
@@ -142,7 +145,7 @@ let rec rewrite_constant_function_calls' ast =
   let rewrite_count = ref 0 in
   let ok () = incr rewrite_count in
   let not_ok () = decr rewrite_count in
-  
+
   let lstate, gstate =
     Interpreter.initial_state ast safe_primops
   in
@@ -168,14 +171,14 @@ let rec rewrite_constant_function_calls' ast =
        fold, just continue without optimising. *)
     | _ -> E_aux (e_aux, annot)
   in
-    
+
   let rw_funcall e_aux annot =
     match e_aux with
     | E_app (id, args) when List.for_all is_constant args ->
        evaluate e_aux annot
 
     | E_field (exp, id) when is_constant exp ->
-       evaluate e_aux annot      
+       evaluate e_aux annot
 
     | E_if (E_aux (E_lit (L_aux (L_true, _)), _), then_exp, _) -> ok (); then_exp
     | E_if (E_aux (E_lit (L_aux (L_false, _)), _), _, else_exp) -> ok (); else_exp
@@ -188,7 +191,7 @@ let rec rewrite_constant_function_calls' ast =
          when is_constant bind ->
        ok ();
        subst id (E_aux (E_cast (typ, bind), annot)) exp
-       
+
     | _ -> E_aux (e_aux, annot)
   in
   let rw_exp = {
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 9a1d0ed2..be258e0d 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -660,7 +660,6 @@ let rec eval_frame' ast = function
      match (m, stack) with
      | Pure v, [] when is_value v -> Done (state, value_of_exp v)
      | Pure v, (head :: stack') when is_value v ->
-        (* print_endline ("Returning value: " ^ string_of_value (value_of_exp v) |> Util.cyan |> Util.clear); *)
         Step (stack_string head, (stack_state head, snd state), stack_cont head (value_of_exp v), stack')
      | Pure exp', _ ->
         let out' = lazy (Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp')) in
@@ -670,7 +669,6 @@ let rec eval_frame' ast = function
         let body = exp_of_fundef (get_fundef id ast) arg in
         Break (Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack))
      | Yield (Call(id, vals, cont)), _ ->
-        (* print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear); *)
         let arg = if List.length vals != 1 then tuple_value vals else List.hd vals in
         let body = exp_of_fundef (get_fundef id ast) arg in
         Step (lazy "", (initial_lstate, snd state), return body, (out, fst state, cont) :: stack)
@@ -680,7 +678,6 @@ let rec eval_frame' ast = function
         eval_frame' ast (Step (out, state', cont (), stack))
      | Yield (Early_return v), [] -> Done (state, v)
      | Yield (Early_return v), (head :: stack') ->
-        (* print_endline ("Returning value: " ^ string_of_value v |> Util.cyan |> Util.clear); *)
         Step (stack_string head, (stack_state head, snd state), stack_cont head v, stack')
      | Yield (Assertion_failed msg), _ ->
         failwith msg
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index efbe63f3..9757ec32 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -61,6 +61,7 @@ let opt_trace_ocaml = ref false
 (* Option to not build generated ocaml by default *)
 let opt_ocaml_nobuild = ref false
 let opt_ocaml_coverage = ref false
+let opt_ocaml_build_dir = ref "_sbuild"
 
 type ctx =
   { register_inits : tannot exp list;
@@ -705,9 +706,9 @@ let ocaml_compile spec defs =
        else
          failwith "Could not find sail share directory, " ^ share_dir ^ ". Make sure sail is installed or try setting environment variable SAIL_DIR."
   in
-  if Sys.file_exists "_sbuild" then () else Unix.mkdir "_sbuild" 0o775;
+  if Sys.file_exists !opt_ocaml_build_dir then () else Unix.mkdir !opt_ocaml_build_dir 0o775;
   let cwd = Unix.getcwd () in
-  Unix.chdir "_sbuild";
+  Unix.chdir !opt_ocaml_build_dir;
   let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/elf_loader.ml .") in
   let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/sail_lib.ml .") in
   let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/util.ml .") in
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 7c1b42ad..2b0fee22 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -338,7 +338,7 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
   match t with
   | Typ_app (Id_aux (Id "vector",_) as id, [Typ_arg_aux (Typ_arg_nexp size,_);ord;typ']) ->
      begin
-       let mk_typ nexp = 
+       let mk_typ nexp =
          Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
        in
        match Type_check.solve env size with
@@ -368,6 +368,9 @@ let doc_tannot_lem ctxt env eff typ =
      if eff then string " : M " ^^ parens ta
      else string " : " ^^ ta
 
+let min_int32 = Big_int.of_int64 (Int64.of_int32 Int32.min_int)
+let max_int32 = Big_int.of_int64 (Int64.of_int32 Int32.max_int)
+
 let doc_lit_lem (L_aux(lit,l)) =
   match lit with
   | L_unit  -> utf8string "()"
@@ -375,11 +378,13 @@ let doc_lit_lem (L_aux(lit,l)) =
   | L_one   -> utf8string "B1"
   | L_false -> utf8string "false"
   | L_true  -> utf8string "true"
-  | L_num i ->
+  | L_num i when Big_int.less_equal min_int32 i && Big_int.less_equal i max_int32 ->
      let ipp = Big_int.to_string i in
      utf8string (
        if Big_int.less i Big_int.zero then "((0"^ipp^"):ii)"
        else "("^ipp^":ii)")
+  | L_num i ->
+     utf8string (Printf.sprintf "(integerOfString \"%s\")" (Big_int.to_string i))
   | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_undef ->
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index 985136c4..c0b3440d 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -152,7 +152,7 @@ let print_code2 ff fname lnum1 cnum1 lnum2 cnum2 =
                        Util.(Str.string_before line cnum2 |> red_bg |> clear)
                        (Str.string_after line cnum2);
         close_in in_chan
-      with e -> (close_in_noerr in_chan; print_endline (Printexc.to_string e))
+      with e -> (close_in_noerr in_chan; prerr_endline (Printexc.to_string e))
     end
   with _ -> ()
 
diff --git a/src/sail.ml b/src/sail.ml
index 0b56ab21..b172a482 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -94,6 +94,9 @@ let options = Arg.align ([
   ( "-ocaml_trace",
     Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml],
     " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml");
+  ( "-ocaml_build_dir",
+    Arg.String (fun dir -> Ocaml_backend.opt_ocaml_build_dir := dir),
+    " set a custom directory to build generated OCaml");
   ( "-ocaml-coverage",
     Arg.Set Ocaml_backend.opt_ocaml_coverage,
     "Build ocaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx).");
diff --git a/src/value.ml b/src/value.ml
index dccb216e..c00b9687 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -381,6 +381,10 @@ let value_shiftr = function
   | [v1; v2] -> mk_vector (Sail_lib.shiftr (coerce_bv v1, coerce_int v2))
   | _ -> failwith "value shiftr"
 
+let value_vector_truncate = function
+  | [v1; v2] -> mk_vector (Sail_lib.vector_truncate (coerce_bv v1, coerce_int v2))
+  | _ -> failwith "value vector_truncate"
+
 let eq_value v1 v2 = string_of_value v1 = string_of_value v2
 
 let value_eq_anything = function
@@ -557,6 +561,7 @@ let primops =
       ("sub_vec_int", value_sub_vec_int);
       ("add_vec", value_add_vec);
       ("sub_vec", value_sub_vec);
+      ("vector_truncate", value_vector_truncate);
       ("read_ram", value_read_ram);
       ("write_ram", value_write_ram);
       ("trace_memory_read", fun _ -> V_unit);