starts compiling but still fake

1 files changed, 27 insertions, 0 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.