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

1 files changed, 22 insertions, 26 deletions

diff --git a/backend/CSE2.v b/backend/CSE2.v
index dc206c75..cad740ba 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
+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_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.