From 87140e97e3c1b2b1713a4458f8f5e622625c0683 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 26 Feb 2019 17:25:55 +0000 Subject: Make -o option work as usual with C compilation --- src/c_backend.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/c_backend.mli') diff --git a/src/c_backend.mli b/src/c_backend.mli index 10bf9f40..a11ac7f5 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -89,7 +89,7 @@ val initial_ctx : Env.t -> ctx val compile_aexp : ctx -> Ast.typ Anf.aexp -> instr list * (clexp -> instr) * instr list -val compile_ast : ctx -> string list -> tannot Ast.defs -> unit +val compile_ast : ctx -> out_channel -> string list -> tannot Ast.defs -> unit val bytecode_ast : ctx -> (cdef list -> cdef list) -> tannot Ast.defs -> cdef list -- cgit v1.2.3 From b118c78ba85320ef2d6632bc2a6ee4f0907e5d23 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 27 Feb 2019 19:24:05 +0000 Subject: 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 --- src/c_backend.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/c_backend.mli') diff --git a/src/c_backend.mli b/src/c_backend.mli index a11ac7f5..e6cc783c 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -59,6 +59,8 @@ val opt_trace : bool ref val opt_smt_trace : bool ref val opt_static : bool ref val opt_no_main : bool ref +val opt_no_rts : bool ref +val opt_prefix : string ref (** [opt_memo_cache] will store the compiled function definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the -- cgit v1.2.3 From fb362fcb5671b6f008794d0a7db31b1f2685e413 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 28 Feb 2019 16:28:56 +0000 Subject: Allow user-specified state to be passed through generated C For example: sail -c_extra_params "CPUMIPSState *env" -c_extra_args env would pass a QEMU MIPS cpu state to every non-builtin function call. Also add documentation for each C compilation option in C_backend.mli --- src/c_backend.mli | 49 +++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 43 insertions(+), 6 deletions(-) (limited to 'src/c_backend.mli') diff --git a/src/c_backend.mli b/src/c_backend.mli index e6cc783c..3b26acdf 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -53,18 +53,54 @@ open Type_check (** Global compilation options *) +(** Output a dataflow graph for each generated function in Graphviz + (dot) format. *) val opt_debug_flow_graphs : bool ref + +(** Print the ANF and IR representations of a specific function. *) val opt_debug_function : string ref + +(** Instrument generated code to output a trace. opt_smt_trace is WIP + but intended to enable generating traces suitable for concolic + execution with SMT. *) val opt_trace : bool ref val opt_smt_trace : bool ref + +(** Define generated functions as static *) val opt_static : bool ref + +(** Do not generate a main function *) val opt_no_main : bool ref + +(** (WIP) Do not include rts.h (the runtime), and do not generate code + that requires any setup or teardown routines to be run by a runtime + before executing any instruction semantics. *) val opt_no_rts : bool ref + +(** Ordinarily we use plain z-encoding to name-mangle generated Sail + identifiers into a form suitable for C. If opt_prefix is set, then + the "z" which is added on the front of each generated C function + will be replaced by opt_prefix. E.g. opt_prefix := "sail_" would + give sail_my_function rather than zmy_function. *) val opt_prefix : string ref -(** [opt_memo_cache] will store the compiled function definitions in - file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the - original function to be compiled. Enabled using the -memo +(** opt_extra_params and opt_extra_arguments allow additional state to + be threaded through the generated C code by adding an additional + parameter to each function type, and then giving an extra argument + to each function call. For example we could have + + opt_extra_params := Some "CPUMIPSState *env" + opt_extra_arguments := Some "env" + + and every generated function will take a pointer to a QEMU MIPS + processor state, and each function will be passed the env argument + when it is called. *) +val opt_extra_params : string option ref +val opt_extra_arguments : string option ref + +(** (WIP) [opt_memo_cache] will store the compiled function + definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum + of the original function to be compiled. Enabled using the -memo flag. Uses Marshal so it's quite picky about the exact version of the Sail version. This cache can obviously become stale if the C backend changes - it'll load an old version compiled without said @@ -82,13 +118,14 @@ val optimize_experimental : bool ref (** The compilation context. *) type ctx -(** Convert a typ to a IR ctyp *) -val ctyp_of_typ : ctx -> Ast.typ -> ctyp - (** Create a context from a typechecking environment. This environment should be the environment returned by typechecking the full AST. *) val initial_ctx : Env.t -> ctx +(** Convert a typ to a IR ctyp *) +val ctyp_of_typ : ctx -> Ast.typ -> ctyp + + val compile_aexp : ctx -> Ast.typ Anf.aexp -> instr list * (clexp -> instr) * instr list val compile_ast : ctx -> out_channel -> string list -> tannot Ast.defs -> unit -- cgit v1.2.3