Merge branch 'master' into dwarf

3 files changed, 32 insertions, 4 deletions

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
diff --git a/driver/Interp.ml b/driver/Interp.ml
index e277ebe0..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
@@ -612,7 +632,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