From 1e29e518e62ad88e9c2e2b180beb07434a07cdd7 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 3 Nov 2014 10:11:23 +0100 Subject: Record public global definitions via field "prog_public" in AST.program. For the moment, this field is ignored. --- driver/Interp.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index e277ebe0..1291d70c 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -612,7 +612,8 @@ let change_main_function p old_main old_main_ty = fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in { prog_main = new_main_id; - prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs } + prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs; + prog_public = p.prog_public } let rec find_main_function name = function | [] -> None -- cgit From ad8c37d0ebb36cb2e54baeacf5a4c7ff145b1a99 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 3 Nov 2014 17:40:22 +0100 Subject: Add Genv.public_symbol operation. Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating. --- driver/Interp.ml | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index 1291d70c..9bb9d237 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -380,13 +380,33 @@ let do_printf m fmt args = let (>>=) opt f = match opt with None -> None | Some arg -> f arg +(* Like eventval_of_val, but accepts static globals as well *) + +let convert_external_arg ge v t = + match v, t with + | Vint i, AST.Tint -> Some (EVint i) + | Vfloat f, AST.Tfloat -> Some (EVfloat f) + | Vsingle f, AST.Tsingle -> Some (EVsingle f) + | Vlong n, AST.Tlong -> Some (EVlong n) + | Vptr(b, ofs), AST.Tint -> + Genv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) + | _, _ -> None + +let rec convert_external_args ge vl tl = + match vl, tl with + | [], [] -> Some [] + | v1::vl, t1::tl -> + convert_external_arg ge v1 t1 >>= fun e1 -> + convert_external_args ge vl tl >>= fun el -> Some (e1 :: el) + | _, _ -> None + let do_external_function id sg ge w args m = match extern_atom id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> print_string (do_printf m fmt args'); flush stdout; - Cexec.list_eventval_of_val ge args sg.sig_args >>= fun eargs -> + convert_external_args ge args sg.sig_args >>= fun eargs -> Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m) | _ -> None -- cgit From 10941819e09e2f9090e7fe39301a0b9026a0eba0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 5 Nov 2014 14:36:14 +0100 Subject: Verification of the Unusedglob pass (removal of unreferenced static global definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating. --- driver/Compiler.v | 9 ++++++++- driver/Driver.ml | 2 +- 2 files changed, 9 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index fb813c7c..0afa7bfb 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -46,6 +46,7 @@ Require Renumber. Require Constprop. Require CSE. Require Deadcode. +Require Unusedglob. Require Allocation. Require Tunneling. Require Linearize. @@ -65,6 +66,7 @@ Require Renumberproof. Require Constpropproof. Require CSEproof. Require Deadcodeproof. +Require Unusedglobproof. Require Allocproof. Require Tunnelingproof. Require Linearizeproof. @@ -135,6 +137,8 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 6) @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 7) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 8) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -244,7 +248,8 @@ Proof. set (p21 := total_if optim_constprop Renumber.transf_program p2) in *. destruct (partial_if optim_CSE CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate. destruct (partial_if optim_redundancy Deadcode.transf_program p3) as [p31|] eqn:?; simpl in H; try discriminate. - destruct (Allocation.transf_program p31) as [p4|] eqn:?; simpl in H; try discriminate. + destruct (Unusedglob.transform_program p31) as [p32|] eqn:?; simpl in H; try discriminate. + destruct (Allocation.transf_program p32) as [p4|] eqn:?; simpl in H; try discriminate. set (p5 := Tunneling.tunnel_program p4) in *. destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate. set (p7 := CleanupLabels.transf_program p6) in *. @@ -263,6 +268,8 @@ Proof. eapply partial_if_simulation; eauto. apply CSEproof.transf_program_correct. apply compose_forward_simulation with (RTL.semantics p31). eapply partial_if_simulation; eauto. apply Deadcodeproof.transf_program_correct. + apply compose_forward_simulation with (RTL.semantics p32). + apply Unusedglobproof.transf_program_correct; auto. apply compose_forward_simulation with (LTL.semantics p4). apply Allocproof.transf_program_correct; auto. apply compose_forward_simulation with (LTL.semantics p5). diff --git a/driver/Driver.ml b/driver/Driver.ml index 76509f41..fec87420 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -150,7 +150,7 @@ let compile_c_ast sourcename csyntax ofile = let asm = match Compiler.transf_c_program csyntax with | Errors.OK asm -> - Asmexpand.expand_program (Unusedglob.transf_program asm) + Asmexpand.expand_program asm | Errors.Error msg -> print_error stderr msg; exit 2 in -- cgit From 00a5e1af73862b1b1aa29b5a07fe43f80f29c764 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 4 Dec 2014 15:16:55 +0100 Subject: Removed unused variable and changed the search for the installation directory. Use Sys.executable_name instead of Sys.argv.(0). --- driver/Configuration.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 1956b151..aff638e7 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -23,7 +23,7 @@ let _ = open_in env_file with Not_found -> let dir = Sys.getcwd () - and name = Sys.argv.(0) in + and name = Sys.executable_name in let dirname = if Filename.is_relative name then Filename.dirname (Filename.concat dir name) else -- cgit From 2fa738f7c3ea91734752bc47b14d8a461e4fd5c2 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 15 Dec 2014 16:18:05 +0100 Subject: Stdlib path is ignored when the configuration has_runtime_lib is set to false. --- driver/Configuration.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'driver') diff --git a/driver/Configuration.ml b/driver/Configuration.ml index aff638e7..e73125f7 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -58,8 +58,6 @@ let get_config key = let bad_config key v = Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2 -let stdlib_path = get_config "stdlib_path" - let prepro = get_config "prepro" let asm = get_config "asm" let linker = get_config "linker" @@ -81,6 +79,13 @@ let has_runtime_lib = | "false" -> false | v -> bad_config "has_runtime_lib" v + +let stdlib_path = + if has_runtime_lib then + get_config "stdlib_path" + else + "" + let asm_supports_cfi = match get_config "asm_supports_cfi" with | "true" -> true -- cgit