Tweaks to C compilation to make it more usable for embedding into other programs

Can now set a prefix for generated C functions with -c_prefix so
-c_prefix sail_ would give sail_execute_CGetPerm over
zexecute_CGetPerm. We still have to use our standard name-mangling
scheme to avoid possible collisions within the name.

Can build C that doesn't expect the standard runtime, which leaves
operations like read_memory, write_memory etc to be stubbed in by
another C program including the generated Sail. Things like
letbindings are still an issue because we rely on a very small runtime
to initialize global letbindings and similar.

-c_separate_execute splits the execute function apart in the generated C

1 files changed, 6 insertions, 0 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index f14d423c..d8cb5a5d 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5170,6 +5170,11 @@ let rewrite_defs_ocaml = [
   (* ("separate_numbs", rewrite_defs_separate_numbs) *)
   ]
 
+let opt_separate_execute = ref false
+
+let if_separate f env defs =
+  if !opt_separate_execute then f env defs else defs
+
 let rewrite_defs_c = [
   ("no_effect_check", (fun _ defs -> opt_no_effects := true; defs));
 
@@ -5196,6 +5201,7 @@ let rewrite_defs_c = [
   ("simple_assignments", rewrite_simple_assignments);
   ("remove_vector_concat", rewrite_defs_remove_vector_concat);
   ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
+  ("split_execute", if_separate (rewrite_split_fun_constr_pats "execute"));
   ("exp_lift_assign", rewrite_defs_exp_lift_assign);
   ("merge_function_clauses", merge_funcls);
   ("recheck_defs", fun _ -> Optimize.recheck)