From 8486b4c046914b1388b68fe906fe267108f84267 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 7 Jul 2020 17:27:08 +0100
Subject: Fixes to operators

---
 src/Compiler.v                | 2 ++
 src/translation/HTLgen.v      | 4 +++-
 src/translation/HTLgenproof.v | 7 +++++--
 src/verilog/Verilog.v         | 5 ++---
 4 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/Compiler.v b/src/Compiler.v
index db3a810..d716caa 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -98,6 +98,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.
@@ -129,6 +130,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 e0f860e..1cc30c7 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -366,7 +366,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 da0b662..dd1d967 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -587,6 +587,9 @@ Section CORRECTNESS.
     - rewrite Heqb in Heqb0. discriminate.
     - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate.
     - rewrite Heqb in Heqb0. discriminate.
+    (*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu,
+      Search Int.repr.
+      repeat (rewrite Int.unsigned_repr). auto.*)
     - unfold Op.eval_addressing32 in *. repeat (unfold_match H2); inv H2.
       + unfold translate_eff_addressing in *. repeat (unfold_match H1).
         destruct v0; inv Heql; rewrite H2; inv H1; repeat eval_correct_tac.
@@ -811,7 +814,7 @@ Section CORRECTNESS.
 
     inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia.
 
-    Unshelve. auto.
+    Unshelve. exact tt.
   Qed.
   Hint Resolve transl_inop_correct : htlproof.
 
@@ -863,7 +866,7 @@ Section CORRECTNESS.
     assert (HPle: Ple res0 (RTL.max_reg_function f))
       by (eapply RTL.max_reg_function_def; eauto; simpl; auto).
     unfold Ple in HPle. lia.
-    Unshelve. trivial.
+    Unshelve. exact tt.
   Qed.
   Hint Resolve transl_iop_correct : htlproof.
 
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 43df3dd..321bdc2 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 *)
 
@@ -325,7 +325,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 :=
-- 
cgit