diff options
| -rw-r--r-- | cfrontend/C2C.ml | 2 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Driver.ml | 4 | ||||
| -rw-r--r-- | driver/Interp.ml | 55 |
4 files changed, 42 insertions, 20 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 2386eed9..ef028255 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1495,7 +1495,7 @@ let convertProgram p = let p' = { prog_defs = gl2; prog_public = public_globals gl2; - prog_main = intern_string "main"; + prog_main = intern_string !Clflags.main_function_name; prog_types = typs; prog_comp_env = ce } in Diagnostics.check_errors (); diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 2db9399f..80883372 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -67,3 +67,4 @@ let option_small_const = ref (!option_small_data) let option_timings = ref false let stdlib_path = ref Configuration.stdlib_path let use_standard_headers = ref Configuration.has_standard_headers +let main_function_name = ref "main" diff --git a/driver/Driver.ml b/driver/Driver.ml index 66cfeaa7..043e43c1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -233,6 +233,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -trace Have the interpreter produce a detailed trace of reductions -random Randomize execution order -all Simulate all possible execution orders + -main <name> Start executing at function <name> instead of main() |} let print_usage_and_exit () = @@ -355,7 +356,8 @@ let cmdline_actions = Exact "-quiet", Unit (fun () -> Interp.trace := 0); Exact "-trace", Unit (fun () -> Interp.trace := 2); Exact "-random", Unit (fun () -> Interp.mode := Interp.Random); - Exact "-all", Unit (fun () -> Interp.mode := Interp.All) + Exact "-all", Unit (fun () -> Interp.mode := Interp.All); + Exact "-main", String (fun s -> main_function_name := s) ] (* Optimization options *) (* -f options: come in -f and -fno- variants *) diff --git a/driver/Interp.ml b/driver/Interp.ml index d4286779..6c83e819 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -587,41 +587,60 @@ let world_program prog = (* Massaging the program to get a suitable "main" function *) -let change_main_function p old_main old_main_ty = - let old_main = Evalof(Evar(old_main, old_main_ty), old_main_ty) in +let change_main_function p new_main_fn = + let new_main_id = intern_string "%main%" in + { p with + Ctypes.prog_main = new_main_id; + Ctypes.prog_defs = + (new_main_id, Gfun(Internal new_main_fn)) :: p.Ctypes.prog_defs } + +let call_main3_function main_id main_ty = + let main_var = Evalof(Evar(main_id, main_ty), main_ty) in let arg1 = Eval(Vint(coqint_of_camlint 0l), type_int32s) in let arg2 = arg1 in let body = - Sreturn(Some(Ecall(old_main, Econs(arg1, Econs(arg2, Enil)), type_int32s))) in - let new_main_fn = - { fn_return = type_int32s; fn_callconv = cc_default; - fn_params = []; fn_vars = []; fn_body = body } in - let new_main_id = intern_string "___main" in - { prog_main = new_main_id; - Ctypes.prog_defs = (new_main_id, Gfun(Ctypes.Internal new_main_fn)) :: p.Ctypes.prog_defs; - Ctypes.prog_public = p.Ctypes.prog_public; - prog_types = p.prog_types; - prog_comp_env = p.prog_comp_env } + Sreturn(Some(Ecall(main_var, Econs(arg1, Econs(arg2, Enil)), type_int32s))) + in + { fn_return = type_int32s; fn_callconv = cc_default; + fn_params = []; fn_vars = []; fn_body = body } + +let call_other_main_function main_id main_ty main_ty_res = + let main_var = Evalof(Evar(main_id, main_ty), main_ty) in + let body = + Ssequence(Sdo(Ecall(main_var, Enil, main_ty_res)), + Sreturn(Some(Eval(Vint(coqint_of_camlint 0l), type_int32s)))) in + { fn_return = type_int32s; fn_callconv = cc_default; + fn_params = []; fn_vars = []; fn_body = body } let rec find_main_function name = function | [] -> None - | (id, Gfun fd) :: gdl -> if id = name then Some fd else find_main_function name gdl - | (id, Gvar v) :: gdl -> find_main_function name gdl + | (id, Gfun fd) :: gdl -> + if id = name then Some fd else find_main_function name gdl + | (id, Gvar v) :: gdl -> + find_main_function name gdl let fixup_main p = match find_main_function p.Ctypes.prog_main p.Ctypes.prog_defs with | None -> - fprintf err_formatter "ERROR: no main() function@."; + fprintf err_formatter "ERROR: no entry function %s()@." + (extern_atom p.Ctypes.prog_main); None | Some main_fd -> match type_of_fundef main_fd with | Tfunction(Tnil, Ctypes.Tint(I32, Signed, _), _) -> Some p - | Tfunction(Tcons(Ctypes.Tint _, Tcons(Tpointer(Tpointer(Ctypes.Tint(I8,_,_),_),_), Tnil)), + | Tfunction(Tcons(Ctypes.Tint _, + Tcons(Tpointer(Tpointer(Ctypes.Tint(I8,_,_),_),_), Tnil)), Ctypes.Tint _, _) as ty -> - Some (change_main_function p p.Ctypes.prog_main ty) + Some (change_main_function p + (call_main3_function p.Ctypes.prog_main ty)) + | Tfunction(Tnil, ty_res, _) as ty -> + Some (change_main_function p + (call_other_main_function p.Ctypes.prog_main ty ty_res)) | _ -> - fprintf err_formatter "ERROR: wrong type for main() function@."; + fprintf err_formatter + "ERROR: wrong type for entry function %s()@." + (extern_atom p.Ctypes.prog_main); None (* Execution of a whole program *) |