Add more operators and print them

3 files changed, 84 insertions, 41 deletions

diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v
index 426a7e6..c400617 100644
--- a/src/translation/Veriloggen.v
+++ b/src/translation/Veriloggen.v
@@ -20,7 +20,7 @@ From Coq Require Import FSets.FMapPositive.
 
 From coqup Require Import HTL Verilog Coquplib.
 
-From compcert Require Errors Op AST.
+From compcert Require Errors Op AST Integers.
 
 Definition node : Type := positive.
 Definition reg : Type := positive.
@@ -112,38 +112,66 @@ End PTree.
 
 Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.
 
+Definition bop (op : binop) (r1 r2 : reg) : option expr :=
+  Some (Vbinop op (Vvar r1) (Vvar r2)).
+
+Definition boplit (op : binop) (r : reg) (l : Integers.int) : option expr :=
+  Some (Vbinop op (Vvar r) (Vlit (intToValue l))).
+
+Definition translate_comparison (c : Integers.comparison) (args : list reg) : option expr :=
+  match c, args with
+  | Integers.Ceq, r1::r2::nil => bop Veq r1 r2
+  | Integers.Cne, r1::r2::nil => bop Vne r1 r2
+  | Integers.Clt, r1::r2::nil => bop Vlt r1 r2
+  | Integers.Cgt, r1::r2::nil => bop Vgt r1 r2
+  | Integers.Cle, r1::r2::nil => bop Vle r1 r2
+  | Integers.Cge, r1::r2::nil => bop Vge r1 r2
+  | _, _ => None
+  end.
+
+Definition translate_condition (c : Op.condition) (args : list reg) : option expr :=
+  match c, args with
+  | Op.Ccomp c, _ => translate_comparison c args
+  | Op.Ccompu c, _ => None
+  | Op.Ccompimm c i, _ => None
+  | Op.Ccompuimm c i, _ => None
+  | Op.Cmaskzero n, _ => None
+  | Op.Cmasknotzero n, _ => None
+  | _, _ => None
+  end.
+
 (** Translate an instruction to a statement. *)
-Definition translate_instr (op : Op.operation) (args : list reg) (dst : reg) : option stmnt :=
-  let assign := nonblock dst in
+Definition translate_instr (op : Op.operation) (args : list reg) : option expr :=
   match op, args with
-  | Op.Omove, v::nil => Some (assign (Vvar v))
-  | Op.Ointconst n, _ => Some (assign (Vlit (intToValue n)))
-  | Op.Oneg, _ => None
-  | Op.Osub, _ => None
-  | Op.Omul, _ => None
-  | Op.Omulimm n, _ => None
+  | Op.Omove, r::nil => Some (Vvar r)
+  | Op.Ointconst n, _ => Some (Vlit (intToValue n))
+  | Op.Oneg, r::nil => Some (Vunop Vneg (Vvar r))
+  | Op.Osub, r1::r2::nil => bop Vsub r1 r2
+  | Op.Omul, r1::r2::nil => bop Vmul r1 r2
+  | Op.Omulimm n, r::nil => boplit Vmul r n
   | Op.Omulhs, _ => None
   | Op.Omulhu, _ => None
-  | Op.Odiv, _ => None
-  | Op.Odivu, _ => None
-  | Op.Omod, _ => None
-  | Op.Omodu, _ => None
-  | Op.Oand, _ => None
-  | Op.Oandimm n, _ => None
-  | Op.Oor, _ => None
-  | Op.Oorimm n, _ => None
-  | Op.Oxor, _ => None
-  | Op.Oxorimm n, _ => None
-  | Op.Onot, _ => None
-  | Op.Oshl, _ => None
-  | Op.Oshlimm n, _ => None
-  | Op.Oshr, _ => None
-  | Op.Oshrimm n, _ => None
-  | Op.Oshrximm n, _ => None
-  | Op.Oshru, _ => None
-  | Op.Oshruimm n, _ => None
-  | Op.Ororimm n, _ => None
-  | Op.Oshldimm n, _ => None
+  | Op.Odiv, r1::r2::nil => bop Vdiv r1 r2
+  | Op.Odivu, r1::r2::nil => bop Vdivu r1 r2
+  | Op.Omod, r1::r2::nil => bop Vmod r1 r2
+  | Op.Omodu, r1::r2::nil => bop Vmodu r1 r2
+  | Op.Oand, r1::r2::nil => bop Vand r1 r2
+  | Op.Oandimm n, r::nil => boplit Vand r n
+  | Op.Oor, r1::r2::nil => bop Vor r1 r2
+  | Op.Oorimm n, r::nil => boplit Vor r n
+  | Op.Oxor, r1::r2::nil => bop Vxor r1 r2
+  | Op.Oxorimm n, r::nil => boplit Vxor r n
+  | Op.Onot, r::nil => Some (Vunop Vnot (Vvar r))
+  | Op.Oshl, r1::r2::nil => bop Vshl r1 r2
+  | Op.Oshlimm n, r::nil => boplit Vshl r n
+  | Op.Oshr, r1::r2::nil => bop Vshr r1 r2
+  | Op.Oshrimm n, r::nil => boplit Vshr r n
+  | Op.Oshrximm n, r::nil => None
+  | Op.Oshru, r1::r2::nil => None
+  | Op.Oshruimm n, r::nil => None
+  | Op.Ororimm n, r::nil => None
+  | Op.Oshldimm n, r::nil => None
+  | Op.Ocmp c, _ => translate_condition c args
   | _, _ => None
   end.
 
@@ -163,17 +191,21 @@ Definition transf_instr (n : node) (i : instruction) (s : state) : mon node :=
   | Hnop n' =>
     add_instr n n' s Vskip
   | Hnonblock op args dst n' =>
-    match (translate_instr op args dst) with
-    | Some instr => add_instr n n' s instr
+    match translate_instr op args with
+    | Some instr => add_instr n n' s (nonblock dst instr)
     | _ => Error (Errors.msg "Instruction is not implemented.")
     end
-  | Hload _ _ _ _ _ => Error (Errors.msg "Load not implemented.")
-  | Hstore _ _ _ _ _ => Error (Errors.msg "Store not implemented.")
-  | Hinst _ _ _ _ => Error (Errors.msg "Call not implemented.")
-  | Htailcall _ _ _ => Error (Errors.msg "Tailcall not implemented.")
-  | Hcond _ _ _ _ => Error (Errors.msg "Cond not implemented.")
+  | Hload _ _ _ _ _ => Error (Errors.msg "Loads are not implemented.")
+  | Hstore _ _ _ _ _ => Error (Errors.msg "Stores are not implemented.")
+  | Hinst _ _ _ _ => Error (Errors.msg "Calls are not implemented.")
+  | Htailcall _ _ _ => Error (Errors.msg "Tailcalls are not implemented.")
+  | Hcond cond args n1 n2 => Error (Errors.msg "Condition not implemented.")
   | Hjumptable _ _ => Error (Errors.msg "Jumptable not implemented.")
-  | Hfinish _ => OK n s
+  | Hfinish r =>
+    match r with
+    | Some x => OK n s
+    | None => OK n s
+    end
   end.
 
 Definition make_stm_cases (s : positive * stmnt) : expr * stmnt :=
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 016a626..04a35de 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -49,6 +49,10 @@ let pprint_binop = function
   | Vshl -> " << "
   | Vshr -> " >> "
 
+let unop = function
+  | Vneg -> " ~ "
+  | Vnot -> " ! "
+
 let register a = P.to_int a
 
 let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (valueToZ l))
@@ -56,7 +60,7 @@ let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (valueToZ l))
 let rec pprint_expr = function
   | Vlit l -> literal l
   | Vvar s -> sprintf "reg_%d" (register s)
-  | Vunop e -> concat ["(~"; pprint_expr e; ")"]
+  | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
   | Vbinop (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"]
   | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"]
 
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 09eb914..50a6809 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -54,12 +54,18 @@ Inductive binop : Type :=
 | Vadd : binop  (** addition (binary [+]) *)
 | Vsub : binop  (** subtraction (binary [-]) *)
 | Vmul : binop  (** multiplication (binary [*]) *)
-| Vdiv : binop  (** multiplication (binary [*]) *)
-| Vmod : binop  (** division ([/]) *)
+| Vdiv : binop  (** division (binary [/]) *)
+| Vdivu : binop  (** division unsigned (binary [/]) *)
+| Vmod : binop  (** remainder ([%]) *)
+| Vmodu : binop  (** remainder unsigned ([/]) *)
 | Vlt : binop   (** less than ([<]) *)
+| Vltu : binop   (** less than unsigned ([<]) *)
 | Vgt : binop   (** greater than ([>]) *)
+| Vgtu : binop   (** greater than unsigned ([>]) *)
 | Vle : binop   (** less than or equal ([<=]) *)
+| Vleu : binop   (** less than or equal unsigned ([<=]) *)
 | Vge : binop   (** greater than or equal ([>=]) *)
+| Vgeu : binop   (** greater than or equal unsigned ([>=]) *)
 | Veq : binop   (** equal to ([==]) *)
 | Vne : binop   (** not equal to ([!=]) *)
 | Vand : binop  (** and (binary [&]) *)
@@ -69,7 +75,8 @@ Inductive binop : Type :=
 | Vshr : binop. (** shift left ([<<]) *)
 
 Inductive unop : Type :=
-| Vneg : unop. (** negation ([~]) *)
+| Vneg  (** negation ([~]) *)
+| Vnot. (** not operation [!] *)
 
 Inductive expr : Type :=
 | Vlit : value -> expr