summaryrefslogtreecommitdiff
path: root/src/constant_fold.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-08-17 18:49:33 +0100
committerAlasdair Armstrong2018-08-17 20:42:09 +0100
commitc0f68b6712c916a3cf16f933840a48ec22330289 (patch)
tree549577f558afb31e4171229e37783fce532835bc /src/constant_fold.ml
parentc3595cbfc8f4f04cb13c693054ba62487bcd0e24 (diff)
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.
Diffstat (limited to 'src/constant_fold.ml')
-rw-r--r--src/constant_fold.ml15
1 files changed, 9 insertions, 6 deletions
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 = {