actually-decent PseudoConversion semantics

3 files changed, 191 insertions, 63 deletions

diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index df18bd402..edb95d38a 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -56,7 +56,7 @@ Module Pseudo (M: PseudoMachine) <: Language.
     | PVar: forall n, Index n -> Pseudo n 1
     | PConst: forall n, const -> Pseudo n 1
 
-    | PBin: forall n m, WBinOp -> Pseudo n m -> Pseudo n m -> Pseudo n m
+    | PBin: forall n, WBinOp -> Pseudo n 1 -> Pseudo n 1 -> Pseudo n 1
     | PNat: forall n, WNatOp -> nat -> Pseudo n 1
     | PShift: forall n, WShiftOp -> Pseudo n 1 -> nat -> Pseudo n 1
 
@@ -71,25 +71,35 @@ Module Pseudo (M: PseudoMachine) <: Language.
 
   Definition Program := Pseudo vars vars.
 
-  Definition applyBin (op: WBinOp) (a b: list const): option (list const) :=
+  Definition applyBin (op: WBinOp) (a b: word width): option (list const) :=
     match op with
-    | Wplus => None
-    | Wmult => None
-    | Wminus => None
-    | Wand => None
+    | Wplus => Some [(wplus a b)]
+    | Wmult => Some [(wmult a b)]
+    | Wminus => Some [(wminus a b)]
+    | Wand => Some [(wand a b)]
     end.
 
-  Definition applyNat (op: WNatOp) (v: nat): option (list const) :=
-    match op with
-    | Wones => None
-    | Wzeros => None
-    end.
+  Definition applyNat (op: WNatOp) (v: Index width): option (list const).
+    refine match op with
+    | Wones => Some [convert (zext (wones v) (width - v)) _]
+    | Wzeros => Some [wzero width]
+    end; abstract (
+      destruct v; simpl;
+      replace (x + (width - x)) with width;
+      intuition ).
+  Defined.
 
-  Definition applyShift (op: WShiftOp) (v: const) (n: nat): option (list const) :=
-    match op with
-    | Wshl => None
-    | Wshr => None
-    end.
+  Definition applyShift (op: WShiftOp) (v: const) (n: Index width): option (list const).
+    refine match op with
+    | Wshl => Some [convert (Word.combine (wzero n) (split1 (width - n) n (convert v _))) _]
+    | Wshr => Some [convert (Word.combine (split2 n (width - n) (convert v _)) (wzero n)) _]
+    end; abstract (
+      unfold const;
+      destruct n; simpl;
+      replace (width - x + x) with width;
+      replace (x + (width - x)) with width;
+      intuition ).
+  Defined.
 
   Inductive PseudoEval: forall n m, Pseudo n m -> State -> State -> Prop :=
     | PEVar: forall s n (i: Index n) w,
@@ -99,11 +109,11 @@ Module Pseudo (M: PseudoMachine) <: Language.
     | PEConst: forall n s w,
         PseudoEval n 1 (PConst n w) s [w]
 
-    | PEBin: forall n m a b s sa sb s' op,
+    | PEBin: forall n a b s sa sb s' op,
         applyBin op sa sb = Some s'
-      -> PseudoEval n m a s sa
-      -> PseudoEval n m b s sb
-      -> PseudoEval n m (PBin n m op a b) s s'
+      -> PseudoEval n 1 a s [sa]
+      -> PseudoEval n 1 b s [sb]
+      -> PseudoEval n 1 (PBin n op a b) s s'
 
     | PENat: forall n op v s s',
         applyNat op v = Some s'
diff --git a/src/Assembly/PseudoConversion.v b/src/Assembly/PseudoConversion.v
index 359659343..0ffe420f2 100644
--- a/src/Assembly/PseudoConversion.v
+++ b/src/Assembly/PseudoConversion.v
@@ -46,63 +46,175 @@ Module PseudoConversion (M: PseudoMachine).
 
     Inductive Mapping :=
       | regM: forall (r: IReg width) (v: nat), v = getIRegIndex r -> Mapping
-      | stackM: forall (r: Stack width) (v: nat), v = getStackIndex r -> Mapping.
-
-    Definition natM (x: nat): Mapping.
-      refine (
-        let N := activeRegisters in
-        let r := (ireg x) in
-        let s := (stack (x - N)) in
-
-        if (dec_lt x N)
-        then (regM r (getIRegIndex r) _)
-        else (stackM s (getStackIndex s) _));
-      abstract intuition.
+      | stackM: forall (r: Stack width) (v: nat), v = getStackIndex r -> Mapping
+      | constM: forall (r: IConst width) (v: nat), v = getIConstValue r -> Mapping.
+
+    Definition mapping_dec (a b: Mapping): {a = b} + {a <> b}.
+      refine (match (a, b) as p' return (a, b) = p' -> _ with
+      | (regM x v _, regM y v' _) => fun _ => 
+        if (Nat.eq_dec v v') then left _ else right _
+
+      | (stackM x v _, stackM y v' _) => fun _ => 
+        if (Nat.eq_dec v v') then left _ else right _
+
+      | (constM x v _, constM y v' _) => fun _ => 
+        if (Nat.eq_dec v v') then left _ else right _
+
+      | _ => fun _ => right _
+      end (eq_refl (a, b))); admit. (* TODO (rsloan): prove *)
     Defined.
 
-    Definition freshN (cur: list nat): nat :=
-      let range := (fix f (x: nat) :=
-        match x with
+    Definition freshMapping (cur: list Mapping) (len: nat): list Mapping :=
+      let used := (fix g (lst: list Mapping) :=
+        match lst with
+        | nil => []
+        | cons c cs =>
+          match c with
+          | stackM _ v _ => cons v (g cs)
+          | _ => g cs
+          end
+        end) cur in
+
+      let open := fun x =>
+        negb (proj1_sig (bool_of_sumbool (in_dec Nat.eq_dec x used))) in
+
+      let maxStack := len + (length cur) in 
+
+     (fix gen (rem bound: nat) :=
+        match bound with
         | O => []
-        | S x' => cons ((length cur) - x) (f x')
-        end) in
+        | S bound' =>
+          match rem with
+          | O => []
+          | S rem' =>
+            let loc := (maxStack - bound) in
+            let s := stack loc in
+
+            if (open loc)
+            then cons (stackM s (getStackIndex s) eq_refl) (gen rem' bound')
+            else gen rem bound'
+          end
+        end) len maxStack.
+
+    Fixpoint moveMapping (a b: list Mapping): AlmostQhasm.Program :=
+      match (a, b) with
+      | (cons ahd atl, cons bhd btl) =>
+        let curOp := 
+          match (ahd, bhd) with
+          | (regM ra va _, regM rb vb _) =>
+            AAssign (ARegRegInt width rb ra)
+
+          | (stackM ra va _, regM rb vb _) =>
+            AAssign (ARegStackInt width rb ra)
+
+          | (regM ra va _, stackM rb vb _) =>
+            AAssign (AStackRegInt width rb ra)
+
+          | (stackM ra va _, stackM rb vb _) =>
+            ASeq
+              (AAssign (ARegStackInt width overflowReg ra))
+              (AAssign (AStackRegInt width rb overflowReg))
+
+          | (constM ra va _, stackM rb vb _) =>
+            ASeq
+              (AAssign (AConstInt width overflowReg ra))
+              (AAssign (AStackRegInt width rb overflowReg))
+
+          | (constM ra va _, regM rb vb _) =>
+            AAssign (AConstInt width rb ra)
+
+          | _ => ASkip
+          end in
+        ASeq curOp (moveMapping atl btl)
+      | _ => ASkip
+      end.
+
+    Definition binProg (op: WBinOp) (a b: Mapping): AlmostQhasm.Program * Mapping :=
+      let iop :=
+        match op with
+        | Wplus => IPlus
+        | Wminus => IMinus
+        | Wand => IAnd
+        end in
+
+      match (a, b) with
+      | (regM ra va _, regM rb vb _) =>
+        (AAssign (ARegRegInt width rb ra), a)
+
+      | (stackM ra va _, regM rb vb _) =>
+        AAssign (ARegStackInt width rb ra)
 
-      let curRange := (range (length cur)) in
+      | (regM ra va _, stackM rb vb _) =>
+        AAssign (AStackRegInt width rb ra)
 
-      let notInCur := fun x =>
-        negb (proj1_sig (bool_of_sumbool
-          (in_dec Nat.eq_dec x cur))) in
+      | (stackM ra va _, stackM rb vb _) =>
+        ASeq
+          (AAssign (ARegStackInt width overflowReg ra))
+          (AAssign (AStackRegInt width rb overflowReg))
 
-      let options := filter notInCur curRange in
+      | (stackM ra va _, constM rb vb _) =>
+        ASeq
+          (AAssign (AConstInt width overflowReg ra))
+          (AAssign (AStackRegInt width rb overflowReg))
 
-      match options with
-      | cons x xs => x
-      | nil => O (* will never happen. TODO (rsloan): False_rec this *)
+      | (stackM ra va _, constM rb vb _) =>
+        AAssign (AConstInt width rb ra)
+
+      | (constM ra va _, constM rb vb _) =>
+        AAssign (AConstInt width rb ra)
+
+      | _ => ASkip
+      end.
+
+
+    Definition shiftProg (op: WShiftOp) (v: const) (n: Index width): AlmostQhasm.Program :=
+      match op with
+      | Wshl => 
+      | Wshr => 
       end.
 
-    Fixpoint convertProgram' {n m} (prog: Pseudo n m) (mapping: list nat): option AlmostQhasm.Program :=
+    Fixpoint convertProgram' {n m}
+             (prog: Pseudo n m)
+             (mapping: list nat)
+             (avoid: list nat)
+             (ret: nat):
+        option (AlmostQhasm.Program * (nat -> nat -> AlmostQhasm.Program) * list nat) :=
+
       let option_map' := fun x f => option_map f x in
+      let otup_map := fun x f =>
+        match x with
+        | Some res =>
+          match (f (fst res) (snd res)) with
+          | Some res' => Some res'
+          | _ => None
+          end
+        | _ => None
+        end in
+ 
       match prog with
       | PVar n i =>
-        option_map' (nth_error mapping n) (fun v =>
-          match (natM v) with
-          | regM r v _ =>
-            AAssign (ARegRegInt width (ireg 0) r)
-          | stackM s v _ =>
-            AAssign (ARegStackInt width (ireg 0) s)
-          end)
+        option_map' (nth_error mapping n) (fun v => (ASkip, [v]))
 
       | PConst n c =>
-        Some (AAssign (AConstInt width (ireg 0) (iconst c)))
-
-      | PBin n m o a b =>
-        option_map' (nth_error mapping n) (fun v =>
-          match (natM v) with
-          | regM r v _ =>
-            AAssign (ARegRegInt width (ireg 0) r)
-          | stackM s v _ =>
-            AAssign (ARegStackInt width (ireg 0) s)
-          end)
+        (ASkip, [constM (iconst c) (getIConstValue (iconst c)) eq_refl])
+
+      | PBin n o a b =>
+        let ret' := (ret + 1) mod activeRegisters in
+        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 =>
+            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
+              Some (ASeq m0 (ASeq bprog (ASeq m1 (ASeq aprog oper))), amap)
+
+            | _ => None
+            end))
 
       | PNat n o v => None
 
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 65831d80a..410389638 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -93,6 +93,12 @@ Definition getStackWords {n} (x: Stack n) :=
   | stack128 loc => 4
   end.
 
+Definition getIConstValue {n} (x: IConst n): nat :=
+  match x with
+  | constInt32 v => wordToNat v
+  | constInt64 v => wordToNat v
+  end.
+
 Definition getIRegIndex {n} (x: IReg n): nat :=
   match x with
   | regInt32 loc => loc