progress on CSE2 builtins

2 files changed, 20 insertions, 31 deletions

diff --git a/backend/CSE2.v b/backend/CSE2.v
index 900a7517..e2ab9f07 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -375,33 +375,12 @@ 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
+Fixpoint 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_instr instr (rel : RELATION.t) : RB.t :=
   match instr with
   | Inop _
@@ -411,7 +390,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 _ _ res _ => Some (kill_builtin_res res (kill_mem rel))
   | Itailcall _ _ _ | Ireturn _ => RB.bot
   end.
 
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 309ccce1..e61cde3d 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) :=
@@ -1578,9 +1587,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 (kill_mem mpc))).
   {
-    replace (Some RELATION.top) with (apply_instr' (fn_code f) pc (map # pc)).
+    replace (Some (kill_builtin_res res (kill_mem 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 +1600,9 @@ Proof.
     rewrite MPC.
     reflexivity.
   }
-  apply top_ok.
-  
+  apply kill_builtin_res_sound.
+  apply kill_mem_sound with (m := m).
+  assumption.
 
 (* cond *)
 - econstructor; split.