From b28c1dc5e2c35238acb05cd0aed67176afaa71b6 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Thu, 13 Feb 2020 11:53:06 -0500
Subject: [PATCH] add back multiplication to make the fiat-crypto backend
 possible

---
 bedrock2/src/bedrock2/BasicCSyntax.v   | 4 ++++
 bedrock2/src/bedrock2/Semantics.v      | 4 ++++
 bedrock2/src/bedrock2/Syntax.v         | 2 +-
 compiler/src/compiler/FlatToRiscvDef.v | 4 ++++
 4 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/bedrock2/src/bedrock2/BasicCSyntax.v b/bedrock2/src/bedrock2/BasicCSyntax.v
index 3a37350a3..026af2321 100644
--- a/bedrock2/src/bedrock2/BasicCSyntax.v
+++ b/bedrock2/src/bedrock2/BasicCSyntax.v
@@ -14,6 +14,10 @@ Definition to_c_parameters : ToCString.parameters := {|
              match op with
              | add => e1++"+"++e2
              | sub => e1++"-"++e2
+             | mul => e1++"*"++e2
+             | mulhuu => "sizeof(intptr_t) == 4 ? ((uint64_t)"++e1++"*"++e2++")>>32 : ((__uint128_t)"++e1++"*"++e2++")>>64 /* TODO this has not been tested */"
+             | divu => e1++"/"++e2
+             | remu => e1++"%"++e2
              | and => e1++"&"++e2
              | or => e1++"|"++e2
              | xor => e1++"^"++e2
diff --git a/bedrock2/src/bedrock2/Semantics.v b/bedrock2/src/bedrock2/Semantics.v
index d3f3f053f..410f6f4ee 100644
--- a/bedrock2/src/bedrock2/Semantics.v
+++ b/bedrock2/src/bedrock2/Semantics.v
@@ -71,6 +71,10 @@ Section binops.
     match bop with
     | bopname.add => word.add
     | bopname.sub => word.sub
+    | bopname.mul => word.mul
+    | bopname.mulhuu => word.mulhuu
+    | bopname.divu => word.divu
+    | bopname.remu => word.modu
     | bopname.and => word.and
     | bopname.or => word.or
     | bopname.xor => word.xor
diff --git a/bedrock2/src/bedrock2/Syntax.v b/bedrock2/src/bedrock2/Syntax.v
index dd4a4b023..2c6c8a619 100644
--- a/bedrock2/src/bedrock2/Syntax.v
+++ b/bedrock2/src/bedrock2/Syntax.v
@@ -3,7 +3,7 @@ Require Coq.Strings.String.
 Require Import Coq.Numbers.BinNums.
 
 Module Import bopname.
-  Inductive bopname := add | sub | and | or | xor | sru | slu | srs | lts | ltu | eq.
+  Inductive bopname := add | sub | mul | mulhuu | divu | remu | and | or | xor | sru | slu | srs | lts | ltu | eq.
 End bopname.
 Notation bopname := bopname.bopname.
 
diff --git a/compiler/src/compiler/FlatToRiscvDef.v b/compiler/src/compiler/FlatToRiscvDef.v
index 42bcb2b1d..10f6d7b27 100644
--- a/compiler/src/compiler/FlatToRiscvDef.v
+++ b/compiler/src/compiler/FlatToRiscvDef.v
@@ -118,6 +118,10 @@ Section FlatToRiscv1.
     match op with
     | Syntax.bopname.add => [[Add rd rs1 rs2]]
     | Syntax.bopname.sub => [[Sub rd rs1 rs2]]
+    | Syntax.bopname.mul => [[Mul rd rs1 rs2]]
+    | Syntax.bopname.mulhuu => [[Mulhu rd rs1 rs2]]
+    | Syntax.bopname.divu => [[Divu rd rs1 rs2]]
+    | Syntax.bopname.remu => [[Remu rd rs1 rs2]]
     | Syntax.bopname.and => [[And rd rs1 rs2]]
     | Syntax.bopname.or  => [[Or  rd rs1 rs2]]
     | Syntax.bopname.xor => [[Xor rd rs1 rs2]]