Merge branch 'develop' into dev-nadesh-provendev-nadesh-proven

4 files changed, 8 insertions, 8 deletions

diff --git a/src/Compiler.v b/src/Compiler.v
index 2ade983..8820f14 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -103,6 +103,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
   @@@ Cminorgen.transl_program
   @@@ Selection.sel_program
   @@@ RTLgen.transl_program
+  @@ print (print_RTL 0)
   @@@ transf_backend.
 
 Local Open Scope linking_scope.
@@ -134,6 +135,7 @@ Proof.
   destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate.
   destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate.
   destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate.
+  rewrite ! compose_print_identity in T.
   destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate.
   unfold transf_backend in T. simpl in T. rewrite ! compose_print_identity in T.
   destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate.
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index db24a1d..1869a8f 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -271,8 +271,6 @@ Definition translate_comparison_imm (c : Integers.comparison) (args : list reg)
 
 Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : mon expr :=
   match c, args with
-  | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)
-  | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)
   | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2)
   | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2)
   | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2)
@@ -283,8 +281,6 @@ Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : m
 Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int)
   : mon expr :=
   match c, args with
-  | Integers.Ceq, r1::nil => ret (boplit Veq r1 i)
-  | Integers.Cne, r1::nil => ret (boplit Vne r1 i)
   | Integers.Clt, r1::nil => ret (boplit Vltu r1 i)
   | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i)
   | Integers.Cle, r1::nil => ret (boplit Vleu r1 i)
@@ -360,7 +356,9 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
     (Vlit (intToValue n))))*)
   | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)
   | Op.Oshruimm n, r::nil => ret (boplit Vshru r n)
-  | Op.Ororimm n, r::nil => ret (boplit Vror r n)
+  | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")
+  (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32)))
+                                        (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*)
   | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))
   | Op.Ocmp c, _ => translate_condition c args
   | Op.Osel c AST.Tint, r1::r2::rl =>
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 813a94b..943b76e 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -342,6 +342,7 @@ Section CORRECTNESS.
 
   Hypothesis TRANSL : match_prog prog tprog.
 
+
 (*   Lemma TRANSL' : *)
 (*     Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. *)
 (*   Proof. intros; apply match_prog_matches; assumption. Qed. *)
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 06e250a..6a1bece 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -143,8 +143,8 @@ Inductive binop : Type :=
 | Vxor : binop  (** xor (binary [^|]) *)
 | Vshl : binop  (** shift left ([<<]) *)
 | Vshr : binop (** shift right ([>>>]) *)
-| Vshru : binop (** shift right unsigned ([>>]) *)
-| Vror : binop. (** shift right unsigned ([>>]) *)
+| Vshru : binop. (** shift right unsigned ([>>]) *)
+(*| Vror : binop (** shift right unsigned ([>>]) *)*)
 
 (** ** Unary Operators *)
 
@@ -330,7 +330,6 @@ Definition binop_run (op : binop) (v1 v2 : value) : option value :=
   | Vshl => Some (Int.shl v1 v2)
   | Vshr => Some (Int.shr v1 v2)
   | Vshru => Some (Int.shru v1 v2)
-  | Vror => Some (Int.ror v1 v2)
   end.
 
 Definition unop_run (op : unop) (v1 : value) : value :=