Merge of the newmem branch:

- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 25 insertions, 5 deletions

diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 9b2e63e..f6c59fc 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -865,12 +865,21 @@ Inductive tr_stmt (c: code) (map: mapping):
      tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
      c!n2 = Some (Icall sig (inl _ rf) rargs rd nd) ->
      reg_map_ok map rd optid ->
-     tr_stmt c map (Scall optid sig b cl) ns nd nexits ngoto nret rret
+     tr_stmt c map (Scall optid sig (inl _ b) cl) ns nd nexits ngoto nret rret
+  | tr_Scall_imm: forall optid sig id cl ns nd nexits ngoto nret rret rd n2 rargs,
+     tr_exprlist c map nil cl ns n2 rargs ->
+     c!n2 = Some (Icall sig (inr _ id) rargs rd nd) ->
+     reg_map_ok map rd optid ->
+     tr_stmt c map (Scall optid sig (inr _ id) cl) ns nd nexits ngoto nret rret
   | tr_Stailcall: forall sig b cl ns nd nexits ngoto nret rret n1 rf n2 rargs,
      tr_expr c map nil b ns n1 rf None ->
      tr_exprlist c map (rf :: nil) cl n1 n2 rargs ->
      c!n2 = Some (Itailcall sig (inl _ rf) rargs) ->
-     tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret
+     tr_stmt c map (Stailcall sig (inl _ b) cl) ns nd nexits ngoto nret rret
+  | tr_Stailcall_imm: forall sig id cl ns nd nexits ngoto nret rret n2 rargs,
+     tr_exprlist c map nil cl ns n2 rargs ->
+     c!n2 = Some (Itailcall sig (inr _ id) rargs) ->
+     tr_stmt c map (Stailcall sig (inr _ id) cl) ns nd nexits ngoto nret rret
   | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 rargs,
      tr_exprlist c map nil al ns n1 rargs ->
      c!n1 = Some (Ibuiltin ef rargs rd nd) ->
@@ -1251,23 +1260,34 @@ Proof.
   apply tr_expr_incr with s3; auto.
   eapply transl_expr_charact; eauto 4 with rtlg.
   (* Scall *)
+  destruct s0 as [b | id]; monadInv TR; saturateTrans.
+  (* indirect *)
   econstructor; eauto 4 with rtlg.
   eapply transl_expr_charact; eauto 3 with rtlg.
   apply tr_exprlist_incr with s5. auto. 
   eapply transl_exprlist_charact; eauto 3 with rtlg.
-  eapply alloc_regs_target_ok with (s1 := s1); eauto 3 with rtlg.
+  eapply alloc_regs_target_ok with (s1 := s0); eauto 3 with rtlg.
   apply regs_valid_cons; eauto 3 with rtlg.
-  apply regs_valid_incr with s1; eauto 3 with rtlg.
+  apply regs_valid_incr with s0; eauto 3 with rtlg.
   apply regs_valid_cons; eauto 3 with rtlg.
   apply regs_valid_incr with s2; eauto 3 with rtlg.
   eapply alloc_optreg_map_ok with (s1 := s2); eauto 3 with rtlg.
+  (* direct *)
+  econstructor; eauto 4 with rtlg.
+  eapply transl_exprlist_charact; eauto 3 with rtlg.
+  eapply alloc_optreg_map_ok with (s1 := s0); eauto 3 with rtlg.
   (* Stailcall *)
-  assert (RV: regs_valid (x :: nil) s1).
+  destruct s0 as [b | id]; monadInv TR; saturateTrans.
+  (* indirect *)
+  assert (RV: regs_valid (x :: nil) s0).
     apply regs_valid_cons; eauto 3 with rtlg. 
   econstructor; eauto 3 with rtlg.
   eapply transl_expr_charact; eauto 3 with rtlg.
   apply tr_exprlist_incr with s4; auto.
   eapply transl_exprlist_charact; eauto 4 with rtlg.
+  (* direct *)
+  econstructor; eauto 3 with rtlg.
+  eapply transl_exprlist_charact; eauto 4 with rtlg.
   (* Sbuiltin *)
   econstructor; eauto 4 with rtlg.
   eapply transl_exprlist_charact; eauto 3 with rtlg.