starts compiling but still fake

5 files changed, 241 insertions, 11 deletions

diff --git a/backend/CSE3.v b/backend/CSE3.v
new file mode 100644
index 00000000..f4d75c51
--- /dev/null
+++ b/backend/CSE3.v
@@ -0,0 +1,27 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps CSE2deps.
+Require Import CSE3analysis HashedSet.
+
+Axiom preanalysis : RTL.function -> analysis_hints.
+
+Definition run f := preanalysis f.
+
+Definition transf_instr (fmap : analysis_hints)
+           (pc: node) (instr: instruction) := instr.
+
+Definition transf_function (f: function) : function :=
+  {| fn_sig := f.(fn_sig);
+     fn_params := f.(fn_params);
+     fn_stacksize := f.(fn_stacksize);
+     fn_code := PTree.map (transf_instr (preanalysis f)) f.(fn_code);
+     fn_entrypoint := f.(fn_entrypoint) |}.
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  AST.transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
+
+Definition match_prog (p tp: RTL.program) :=
+  match_program (fun ctx f tf => tf = transf_fundef f) eq p tp.
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 966d3fd1..ded31270 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -122,13 +122,25 @@ Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) :=
 Definition add_ilist_j (ilist : list reg) (j : eq_id) (m : Regmap.t PSet.t) :=
   List.fold_left (fun already i => add_i_j i j already) ilist m.
 
-Definition get_kills (eqs : PTree.t equation) :
+Definition get_reg_kills (eqs : PTree.t equation) :
   Regmap.t PSet.t :=
   PTree.fold (fun already (eqno : eq_id) (eq : equation) =>
                 add_i_j (eq_lhs eq) eqno
                         (add_ilist_j (eq_args eq) eqno already)) eqs
              (PMap.init PSet.empty).
 
+Definition eq_depends_on_mem eq :=
+  match eq_op eq with
+  | SLoad _ _ => true
+  | SOp op => op_depends_on_memory op
+  end.
+
+Definition get_mem_kills (eqs : PTree.t equation) : PSet.t :=
+  PTree.fold (fun already (eqno : eq_id) (eq : equation) =>
+                if eq_depends_on_mem eq
+                then PSet.add eqno already
+                else already) eqs PSet.empty.
+
 Definition is_move (op : operation) :
   { op = Omove } + { op <> Omove }.
 Proof.
@@ -157,7 +169,7 @@ Record eq_context := mkeqcontext
                          eq_find_oracle : node -> equation -> option eq_id;
                          eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t;
                          eq_kill_reg : reg -> PSet.t;
-                         eq_kill_mem : PSet.t;
+                         eq_kill_mem : unit -> PSet.t;
                          eq_moves : reg -> PSet.t }.
 
 Section OPERATIONS.
@@ -167,7 +179,7 @@ Section OPERATIONS.
     PSet.subtract rel (eq_kill_reg ctx r).
   
   Definition kill_mem (rel : RELATION.t) : RELATION.t :=
-    PSet.subtract rel (eq_kill_mem ctx).
+    PSet.subtract rel (eq_kill_mem ctx tt).
 
   Definition pick_source (l : list reg) := (* todo: take min? *)
     match l with
@@ -279,10 +291,27 @@ Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t :=
     end
   end.
 
-Definition forward_map (f : RTL.function) := DS.fixpoint
+Definition internal_analysis (f : RTL.function) := DS.fixpoint
   (RTL.fn_code f) RTL.successors_instr
   (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top).
 
 End OPERATIONS.
 
-Definition totoro := RELATION.lub.
+Record analysis_hints :=
+  mkanalysis_hints
+    { hint_eq_catalog :  PTree.t equation;
+      hint_eq_find_oracle : node -> equation -> option eq_id;
+      hint_eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t }.
+
+Definition analysis (eqs : PTree.t equation) (hints : analysis_hints) :=
+  let reg_kills := get_reg_kills eqs in 
+  let mem_kills := get_mem_kills eqs in
+  let moves := get_moves eqs in
+  internal_analysis (ctx := {|
+      eq_catalog := fun eq_id => PTree.get eq_id (hint_eq_catalog hints);
+      eq_find_oracle := hint_eq_find_oracle hints ;
+      eq_rhs_oracle  := hint_eq_rhs_oracle hints;
+      eq_kill_reg := fun reg => PMap.get reg reg_kills;
+      eq_kill_mem := fun _ => mem_kills;
+      eq_moves    := fun reg => PMap.get reg moves
+      |}).
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml
new file mode 100644
index 00000000..26f19fd6
--- /dev/null
+++ b/backend/CSE3analysisaux.ml
@@ -0,0 +1,36 @@
+open CSE3analysis
+open Maps
+open HashedSet
+open Camlcoq
+
+let flatten_eq eq =
+  ((P.to_int eq.eq_lhs), eq.eq_op, List.map P.to_int eq.eq_args);;
+
+let preanalysis (f : RTL.coq_function) =
+  let cur_eq_id = ref 0
+  and cur_catalog = ref PTree.empty
+  and eq_table = Hashtbl.create 100
+  and rhs_table = Hashtbl.create 100
+  and cur_kill_reg = ref (PMap.init PSet.empty)
+  and cur_kill_mem = ref PSet.empty
+  and cur_moves = ref (PMap.init PSet.empty) in
+  let eq_find_oracle node eq =
+    Hashtbl.find_opt eq_table (flatten_eq eq)
+  and rhs_find_oracle node sop args =
+    match Hashtbl.find_opt rhs_table (sop, List.map P.to_int args) with
+    | None -> PSet.empty
+    | Some s -> s in
+  let mutating_eq_find_oracle node eq =
+    incr cur_eq_id; None in (* FIXME *)
+  ignore 
+    (internal_analysis
+      { eq_catalog     = (fun eq_id -> PTree.get eq_id !cur_catalog);
+        eq_find_oracle = mutating_eq_find_oracle;
+        eq_rhs_oracle  = rhs_find_oracle ;
+        eq_kill_reg    = (fun reg -> PMap.get reg !cur_kill_reg);
+        eq_kill_mem    = (fun () -> !cur_kill_mem);
+        eq_moves       = (fun reg -> PMap.get reg !cur_moves)
+      } f);
+  { hint_eq_catalog    = !cur_catalog;
+    hint_eq_find_oracle= eq_find_oracle;
+    hint_eq_rhs_oracle = rhs_find_oracle };;
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index c0a9be48..f805d2b8 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -134,9 +134,9 @@ Lemma get_kills_has_lhs :
     PTree.get j eqs = Some {| eq_lhs := lhs;
                               eq_op  := sop;
                               eq_args:= args |} ->
-    PSet.contains (Regmap.get lhs (get_kills eqs)) j = true.
+    PSet.contains (Regmap.get lhs (get_reg_kills eqs)) j = true.
 Proof.
-  unfold get_kills.
+  unfold get_reg_kills.
   intros.
   rewrite PTree.fold_spec.
   change (fold_left
@@ -154,9 +154,9 @@ Lemma get_kills_has_arg :
                               eq_op  := sop;
                               eq_args:= args |} ->
     In arg args ->
-    PSet.contains (Regmap.get arg (get_kills eqs)) j = true.
+    PSet.contains (Regmap.get arg (get_reg_kills eqs)) j = true.
 Proof.
-  unfold get_kills.
+  unfold get_reg_kills.
   intros.
   rewrite PTree.fold_spec.
   change (fold_left
@@ -232,14 +232,14 @@ Section SOUNDNESS.
                                  eq_op  := SOp op;
                                  eq_args:= args |} ->
       op_depends_on_memory op = true ->
-      PSet.contains (eq_kill_mem ctx) j = true.
+      PSet.contains (eq_kill_mem ctx tt) j = true.
 
   Hypothesis ctx_kill_mem_has_load :
     forall lhs chunk addr args j,
       eq_catalog ctx j = Some {| eq_lhs := lhs;
                                  eq_op  := SLoad chunk addr;
                                  eq_args:= args |} ->
-      PSet.contains (eq_kill_mem ctx) j = true.
+      PSet.contains (eq_kill_mem ctx tt) j = true.
 
   Theorem kill_reg_sound :
     forall rel rs m dst v,
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
new file mode 100644
index 00000000..408b3cee
--- /dev/null
+++ b/backend/CSE3proof.v
@@ -0,0 +1,138 @@
+(*
+Replace available expressions by the register containing their value.
+
+Proofs.
+
+David Monniaux, CNRS, VERIMAG
+ *)
+
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE3 CSE3analysis CSE3analysisproof.
+
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+End SOUNDNESS.
+
+
+Definition match_prog (p tp: RTL.program) :=
+  match_program (fun cu f tf => tf = transf_fundef f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_prog p (transf_program p).
+Proof.
+  intros. apply match_transform_program; auto.
+Qed.
+
+Section PRESERVATION.
+
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_transf TRANSL).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  Genv.find_funct_ptr tge v = Some (transf_fundef f).
+Proof (Genv.find_funct_ptr_transf TRANSL).
+
+Lemma symbols_preserved:
+  forall id,
+  Genv.find_symbol tge id = Genv.find_symbol ge id.
+Proof (Genv.find_symbol_transf TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_transf TRANSL).
+
+Lemma sig_preserved:
+  forall f, funsig (transf_fundef f) = funsig f.
+Proof.
+  destruct f; trivial.
+Qed.
+
+Lemma find_function_translated:
+  forall ros rs fd,
+  find_function ge ros rs = Some fd ->
+  find_function tge ros rs = Some (transf_fundef fd).
+Proof.
+  unfold find_function; intros. destruct ros as [r|id].
+  eapply functions_translated; eauto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
+  eapply function_ptr_translated; eauto.
+Qed.
+
+Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
+| match_frames_intro: forall res f sp pc rs,
+    (* (forall m : mem,
+     forall vres, (fmap_sem' sp m (forward_map f) pc rs # res <- vres)) -> *)
+    match_frames (Stackframe res f sp pc rs)
+                 (Stackframe res (transf_function f) sp pc rs).
+
+Inductive match_states: RTL.state -> RTL.state -> Prop :=
+  | match_regular_states: forall stk f sp pc rs m stk'
+                                 (STACKS: list_forall2 match_frames stk stk'),
+      (* (fmap_sem' sp m (forward_map f) pc rs) -> *)
+      match_states (State stk f sp pc rs m)
+                   (State stk' (transf_function f) sp pc rs m)
+  | match_callstates: forall stk f args m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Callstate stk f args m)
+                   (Callstate stk' (transf_fundef f) args m)
+  | match_returnstates: forall stk v m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Returnstate stk v m)
+                   (Returnstate stk' v m).
+  
+
+Lemma step_simulation:
+  forall S1 t S2, RTL.step ge S1 t S2 ->
+  forall S1', match_states S1 S1' ->
+              exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
+Proof.
+Admitted.
+Lemma transf_initial_states:
+  forall S1, RTL.initial_state prog S1 ->
+  exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2.
+Proof.
+  intros. inv H. econstructor; split.
+  econstructor.
+    eapply (Genv.init_mem_transf TRANSL); eauto.
+    rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto.
+    eapply function_ptr_translated; eauto.
+    rewrite <- H3; apply sig_preserved.
+  constructor. constructor.
+Qed.
+
+Lemma transf_final_states:
+  forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r.
+Proof.
+  intros. inv H0. inv H. inv STACKS. constructor.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
+Proof.
+  eapply forward_simulation_step.
+  apply senv_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact step_simulation.
+Qed.
+
+End PRESERVATION.