Merge remote-tracking branch 'origin/mppa-cse3' into mppa-licm

5 files changed, 111 insertions, 35 deletions

diff --git a/backend/CSE2.v b/backend/CSE2.v
index dc206c75..8e2307b0 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -262,33 +262,29 @@ Definition load (chunk: memory_chunk) (addr : addressing)
   | None => load1 chunk addr dst args rel
   end.
 
-(* NO LONGER NEEDED
-Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop :=
-  match l with
-  | nil => True
-  | (r,sv)::tail => (tr ! r) = Some sv /\ list_represents tail tr
+Definition kill_builtin_res res rel :=
+  match res with
+  | BR r => kill_reg r rel
+  | _ => rel
   end.
 
-Lemma elements_represent :
-  forall { X : Type },
-  forall tr : (PTree.t X),
-    (list_represents (PTree.elements tr) tr).
-Proof.
-  intros.
-  generalize (PTree.elements_complete tr).
-  generalize (PTree.elements tr).
-  induction l; simpl; trivial.
-  intro COMPLETE.
-  destruct a as [ r sv ].
-  split.
-  {
-    apply COMPLETE.
-    left; reflexivity.
-  }
-  apply IHl; auto.
-Qed.
-*)
-    
+Definition apply_external_call ef (rel : RELATION.t) : RELATION.t :=
+  match ef with
+  | EF_builtin name sg
+  | EF_runtime name sg =>
+    match Builtins.lookup_builtin_function name sg with
+    | Some bf => rel
+    | None => kill_mem rel
+    end
+  | EF_malloc (* FIXME *)
+  | EF_external _ _
+  | EF_vstore _ 
+  | EF_free (* FIXME *)
+  | EF_memcpy _ _ (* FIXME *)
+  | EF_inline_asm _ _ _ => kill_mem rel
+  | _ => rel
+  end.
+                              
 Definition apply_instr instr (rel : RELATION.t) : RB.t :=
   match instr with
   | Inop _
@@ -298,7 +294,7 @@ Definition apply_instr instr (rel : RELATION.t) : RB.t :=
   | Iop op args dst _ => Some (gen_oper op dst args rel)
   | Iload trap chunk addr args dst _ => Some (load chunk addr dst args rel)
   | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
-  | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *)
+  | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel))
   | Itailcall _ _ _ | Ireturn _ => RB.bot
   end.
 
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 309ccce1..9e0ad909 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -1033,7 +1033,16 @@ Proof.
     assumption.
   }
   intuition congruence.
-Qed. 
+Qed.
+
+Lemma kill_builtin_res_sound:
+  forall res (m : mem) (rs : regset) vres (rel : RELATION.t)
+         (REL : sem_rel m rel rs),
+         (sem_rel m (kill_builtin_res res rel) (regmap_setres res vres rs)).
+Proof.
+  destruct res; simpl; intros; trivial.
+  apply kill_reg_sound; trivial.
+Qed.
 End SOUNDNESS.
 
 Definition match_prog (p tp: RTL.program) :=
@@ -1116,6 +1125,22 @@ Definition is_killed_in_fmap fmap pc res :=
   | Some map => is_killed_in_map map pc res
   end.
 
+Lemma external_call_sound:
+  forall ef (rel : RELATION.t) sp (m m' : mem) (rs : regset) vargs t vres
+         (REL : sem_rel fundef unit ge sp m rel rs)
+         (CALL : external_call ef ge vargs m t vres m'),
+    sem_rel fundef unit ge sp m' (apply_external_call ef rel) rs.
+Proof.
+  destruct ef; intros; simpl in *.
+  all: eauto using kill_mem_sound.
+  all: unfold builtin_or_external_sem in *.
+  1, 2: destruct (Builtins.lookup_builtin_function name sg);
+    eauto using kill_mem_sound;
+    inv CALL; eauto using kill_mem_sound.
+  all: inv CALL.
+  all: eauto using kill_mem_sound.
+Qed.
+  
 Definition sem_rel_b' := sem_rel_b fundef unit ge.
 Definition fmap_sem' := fmap_sem fundef unit ge.
 Definition subst_arg_ok' := subst_arg_ok fundef unit ge.
@@ -1578,9 +1603,9 @@ Proof.
   destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
   destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
   
-  apply sem_rel_b_ge with (rb2 := Some RELATION.top).
+  apply sem_rel_b_ge with (rb2 := Some (kill_builtin_res res (apply_external_call ef mpc))).
   {
-    replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)).
+    replace (Some (kill_builtin_res res (apply_external_call ef mpc))) with (apply_instr' (fn_code f) pc (map # pc)).
     {
       eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
       2: apply apply_instr'_bot.
@@ -1591,8 +1616,8 @@ Proof.
     rewrite MPC.
     reflexivity.
   }
-  apply top_ok.
-  
+  apply kill_builtin_res_sound.
+  eapply external_call_sound with (m := m); eassumption.
 
 (* cond *)
 - econstructor; split.
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 90ce4ce7..bc5d3244 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -325,6 +325,29 @@ Section OPERATIONS.
              (rel : RELATION.t) : RELATION.t :=
     store1 chunk addr (forward_move_l rel args) src ty rel.
 
+  Definition kill_builtin_res res rel :=
+    match res with
+    | BR r => kill_reg r rel
+    | _ => rel
+    end.
+
+  Definition apply_external_call ef (rel : RELATION.t) : RELATION.t :=
+    match ef with
+    | EF_builtin name sg
+    | EF_runtime name sg =>
+      match Builtins.lookup_builtin_function name sg with
+      | Some bf => rel
+      | None => kill_mem rel
+      end
+    | EF_malloc (* FIXME *)
+    | EF_external _ _
+    | EF_vstore _ 
+    | EF_free (* FIXME *)
+    | EF_memcpy _ _ (* FIXME *)
+    | EF_inline_asm _ _ _ => kill_mem rel
+    | _ => rel
+    end.
+
   Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : RB.t :=
   match instr with
   | Inop _
@@ -335,7 +358,7 @@ Section OPERATIONS.
   | Iop op args dst _ => Some (oper dst (SOp op) args rel)
   | Iload trap chunk addr args dst _ => Some (oper dst (SLoad chunk addr) args rel)
   | Icall _ _ _ dst _ => Some (kill_reg dst (kill_mem rel))
-  | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *)
+  | Ibuiltin ef _ res _ => Some (kill_builtin_res res (apply_external_call ef rel))
   | Itailcall _ _ _ | Ireturn _ => RB.bot
   end.
   End PER_NODE.
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index b87ec92c..f4ec7a10 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -869,6 +869,36 @@ Section SOUNDNESS.
 
   Hint Resolve store_sound : cse3.
 
+  Lemma kill_builtin_res_sound:
+    forall res (m : mem) (rs : regset) vres (rel : RELATION.t)
+           (REL : sem_rel rel rs m),
+      (sem_rel (kill_builtin_res (ctx:=ctx) res rel)
+               (regmap_setres res vres rs) m).
+  Proof.
+    destruct res; simpl; intros; trivial.
+    apply kill_reg_sound; trivial.
+  Qed.
+
+  Hint Resolve kill_builtin_res_sound : cse3.
+
+  Lemma external_call_sound:
+    forall ge ef (rel : RELATION.t) (m m' : mem) (rs : regset) vargs t vres
+           (REL : sem_rel rel rs m)
+           (CALL : external_call ef ge vargs m t vres m'),
+      sem_rel (apply_external_call (ctx:=ctx) ef rel) rs m'.
+  Proof.
+    destruct ef; intros; simpl in *.
+    all: eauto using kill_mem_sound.
+    all: unfold builtin_or_external_sem in *.
+    1, 2: destruct (Builtins.lookup_builtin_function name sg);
+      eauto using kill_mem_sound;
+      inv CALL; eauto using kill_mem_sound.
+    all: inv CALL.
+    all: eauto using kill_mem_sound.
+  Qed.
+
+  Hint Resolve external_call_sound : cse3.
+
   Section INDUCTIVENESS.
     Variable fn : RTL.function.
     Variable tenv : typing_env.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 19fb20be..53872e62 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -224,7 +224,6 @@ Proof.
   eapply function_ptr_translated; eauto.
 Qed.
 
-Check sem_rel_b.
 Inductive match_stackframes: list stackframe -> list stackframe -> signature -> Prop :=
   | match_stackframes_nil: forall sg,
       sg.(sig_res) = Tint ->
@@ -428,8 +427,8 @@ Ltac IND_STEP :=
         destruct ((fst (preanalysis tenv fn)) # mpc) as [zinv | ];
         simpl in *;
         intuition;
-        eapply rel_ge; eauto with cse3;
-        idtac mpc mpc' fn minstr
+        eapply rel_ge; eauto with cse3 (* ; for printing
+        idtac mpc mpc' fn minstr *)
       end.
 
 Lemma if_same : forall {T : Type} (b : bool) (x : T),
@@ -753,6 +752,9 @@ Proof.
     + econstructor; eauto.
       * eapply wt_exec_Ibuiltin with (f:=f); eauto with wt.
       * IND_STEP.
+        apply kill_builtin_res_sound; eauto with cse3.
+        eapply external_call_sound; eauto with cse3.
+        
   - (* Icond *)
     econstructor. split.
     + eapply exec_Icond with (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); try eassumption.