actually-decent PseudoConversion semantics

1 files changed, 61 insertions, 37 deletions

diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
index 0ffe420f2..cf5a3d11b 100644
--- a/src/Assembly/PseudoConversion.v
+++ b/src/Assembly/PseudoConversion.v
@@ -24,8 +24,9 @@ Module PseudoConversion (M: PseudoMachine).
   Module Conv <: Conversion P AlmostQhasm.
     Import P M.
 
-    Definition activeRegisters := 6.
-    Definition overflowReg := ireg 6.
+    Definition activeRegisters := 5.
+    Definition r0 := ireg 5.
+    Definition r1 := ireg 6.
 
     Definition convertState (st: AlmostQhasm.State): P.State :=
       match st with
@@ -112,13 +113,13 @@ Module PseudoConversion (M: PseudoMachine).
 
           | (stackM ra va _, stackM rb vb _) =>
             ASeq
-              (AAssign (ARegStackInt width overflowReg ra))
-              (AAssign (AStackRegInt width rb overflowReg))
+              (AAssign (ARegStackInt width r0 ra))
+              (AAssign (AStackRegInt width rb r0))
 
           | (constM ra va _, stackM rb vb _) =>
             ASeq
-              (AAssign (AConstInt width overflowReg ra))
-              (AAssign (AStackRegInt width rb overflowReg))
+              (AAssign (AConstInt width r0 ra))
+              (AAssign (AStackRegInt width rb r0))
 
           | (constM ra va _, regM rb vb _) =>
             AAssign (AConstInt width rb ra)
@@ -129,56 +130,79 @@ Module PseudoConversion (M: PseudoMachine).
       | _ => ASkip
       end.
 
-    Definition binProg (op: WBinOp) (a b: Mapping): AlmostQhasm.Program * Mapping :=
+    Definition wordToConstM (w: word width) :=
+      constM (iconst w) (getIConstValue (iconst w)) eq_refl.
+
+    (* Invariant: never return r0 or r1 in our mapping *)
+    Definition binProg (op: WBinOp) (a b: Mapping):
+        AlmostQhasm.Program * Mapping :=
       let iop :=
         match op with
         | Wplus => IPlus
         | Wminus => IMinus
-        | Wand => IAnd
+        | _ => IAnd
         end in
 
       match (a, b) with
-      | (regM ra va _, regM rb vb _) =>
-        (AAssign (ARegRegInt width rb ra), a)
+      | (regM ra va pa, regM rb vb _) =>
+        (AOp (IOpReg width iop ra rb), regM ra va pa)
 
-      | (stackM ra va _, regM rb vb _) =>
-        AAssign (ARegStackInt width rb ra)
+      | (stackM ra va _, regM rb vb pb) =>
+        (ASeq (AAssign (ARegStackInt width r0 ra))
+              (AOp (IOpReg width iop rb r0)),
+         regM rb vb pb) (* Assumption: commutativity forall IntOp *)
 
-      | (regM ra va _, stackM rb vb _) =>
-        AAssign (AStackRegInt width rb ra)
+      | (regM ra va pa, stackM rb vb _) =>
+        (ASeq (AAssign (ARegStackInt width r0 rb))
+              (AOp (IOpReg width iop ra r0)),
+         regM ra va pa)
 
       | (stackM ra va _, stackM rb vb _) =>
-        ASeq
-          (AAssign (ARegStackInt width overflowReg ra))
-          (AAssign (AStackRegInt width rb overflowReg))
-
-      | (stackM ra va _, constM rb vb _) =>
-        ASeq
-          (AAssign (AConstInt width overflowReg ra))
-          (AAssign (AStackRegInt width rb overflowReg))
+        (ASeq (AAssign (ARegStackInt width r1 ra))
+          (ASeq (AAssign (ARegStackInt width r0 rb))
+            (AOp (IOpReg width iop r1 r0))),
+         regM r1 (getIRegIndex r1) eq_refl)
 
       | (stackM ra va _, constM rb vb _) =>
-        AAssign (AConstInt width rb ra)
+        (ASeq (AAssign (ARegStackInt width r1 ra))
+          (AOp (IOpConst width iop r1 rb)),
+         regM r1 (getIRegIndex r1) eq_refl)
 
       | (constM ra va _, constM rb vb _) =>
-        AAssign (AConstInt width rb ra)
-
-      | _ => ASkip
+        (ASkip,
+          let v := match iop with
+            | IPlus => wplus
+            | IMinus => wminus
+            | _ => wand
+            end width (natToWord width va) (natToWord width vb)
+          in constM (iconst v) (getIConstValue (iconst v)) eq_refl)
+
+      | _ => (ASkip, wordToConstM (wzero width))
       end.
 
-
-    Definition shiftProg (op: WShiftOp) (v: const) (n: Index width): AlmostQhasm.Program :=
-      match op with
-      | Wshl => 
-      | Wshr => 
+    Definition shiftProg (op: WShiftOp) (m: Mapping) (n: Index width):
+        AlmostQhasm.Program * Mapping :=
+      let qop := match op with | Wshl => Shl | Wshr => Shr end in
+      match m with
+      | regM r v _ =>
+        (AOp (OpRot width qop r n), regM r (getIRegIndex r) eq_refl)
+      | stackM r v _ =>
+        (ASeq (AAssign (ARegStackInt width r1 r)) (AOp (OpRot width qop r1 n)),
+         regM r1 (getIRegIndex r1) eq_refl)
+      | constM r v _ =>
+        (ASkip, wordToConstM
+          match qop with
+          | Shl => NToWord width (N.shiftl_nat (N.of_nat v) n)
+          | Shr => NToWord width (N.shiftr_nat (N.of_nat v) n)
+          end)
       end.
 
     Fixpoint convertProgram' {n m}
              (prog: Pseudo n m)
-             (mapping: list nat)
-             (avoid: list nat)
+             (mapping: list Mapping)
+             (avoid: list Mapping)
              (ret: nat):
-        option (AlmostQhasm.Program * (nat -> nat -> AlmostQhasm.Program) * list nat) :=
+        option (AlmostQhasm.Program * list nat) :=
 
       let option_map' := fun x f => option_map f x in
       let otup_map := fun x f =>
@@ -203,14 +227,14 @@ Module PseudoConversion (M: PseudoMachine).
         let tmp0 := freshMapping (avoid ++ mapping) n in
         let tmp1 := freshMapping (avoid ++ mapping ++ tmp0) m in
 
-        otup_map (convertProgram' a mapping ret) (fun aprog amap =>
-          otup_map (convertProgram' b mapping ret') (fun bprog bmap =>
+        otup_map (convertProgram' a mapping avoid ret) (fun aprog amap =>
+          otup_map (convertProgram' b mapping avoid ret') (fun bprog bmap =>
             let m0 := moveMapping mapping tmp0 in
             let m1 := moveMapping bmap tmp1 in
 
             match (amap, bmap) with
             | ([av], [bv]) =>
-              let oper := binProg m o av bv in
+              let oper := binProg m o av bv r1 in
               Some (ASeq m0 (ASeq bprog (ASeq m1 (ASeq aprog oper))), amap)
 
             | _ => None