very unstable, but interesting commit

2 files changed, 408 insertions, 35 deletions

diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v
index 2d3567a44..4c8fe8b9b 100644
--- a/src/Assembly/QhasmCommon.v
+++ b/src/Assembly/QhasmCommon.v
@@ -1,17 +1,35 @@
-Require Export String List.
+Require Export String List Logic.
 Require Export Bedrock.Word.
 
 Require Import ZArith NArith NPeano.
 Require Import Coq.Structures.OrderedTypeEx.
 Require Import FMapAVL FMapList.
+Require Import JMeq.
 
 Require Import QhasmUtil.
 
+Import ListNotations.
+
 Module NatM := FMapAVL.Make(Nat_as_OT).
 Definition DefMap: Type := NatM.t N.
 Definition StateMap: Type := NatM.t DefMap.
 Definition LabelMap: Type := NatM.t nat.
 
+(* Sugar *)
+
+Definition W := word 32.
+
+Definition convert {A B: Type} (x: A) (H: A = B): B :=
+ eq_rect A (fun B0 : Type => B0) x B H.
+
+Ltac create X Y :=
+  let H := fresh in (
+    assert (exists X, X = Y) as H
+      by (exists Y; abstract intuition);
+    destruct H).
+
+Local Obligation Tactic := abstract (Tactics.program_simpl; intuition).
+
 (* A formalization of x86 qhasm *)
 
 (* A constant upper-bound on the number of operations we run *)
@@ -32,7 +50,9 @@ Inductive Reg: nat -> Set :=
 Inductive Stack: nat -> Set :=
   | stack32: nat -> Stack 32
   | stack64: nat -> Stack 64
-  | stack128: nat -> Stack 128.
+  | stack128: nat -> Stack 128
+  | stack256: nat -> Stack 256
+  | stack512: nat -> Stack 512.
 
 (* Assignments *)
 Inductive Assignment : Set :=
@@ -114,44 +134,200 @@ Hint Constructors Conditional.
 (* Machine State *)
 
 Inductive State :=
-| fullState (regState: StateMap) (stackState: StateMap): State.
+| fullState (regState: StateMap) (stackState: DefMap): State.
+
+(* Reg, Stack, Const Utilities *)
+
+Definition getRegWords {n} (x: Reg n) :=
+  match x with
+  | reg32 loc => 1
+  | reg3232 loc => 2
+  | reg6464 loc => 4
+  | reg80 loc => 2
+  end.
+
+Definition getStackWords {n} (x: Stack n) :=
+  match x with
+  | stack32 loc => 1
+  | stack64 loc => 2
+  | stack128 loc => 4
+  | stack256 loc => 8
+  | stack512 loc => 16
+  end.
+
+Definition getRegIndex {n} (x: Reg n): nat :=
+  match x with
+  | reg32 loc => loc
+  | reg3232 loc => loc
+  | reg6464 loc => loc
+  | reg80 loc => loc
+  end.
+
+Definition getStackIndex {n} (x: Stack n): nat :=
+  match x with
+  | stack32 loc => loc
+  | stack64 loc => loc
+  | stack128 loc => loc
+  | stack256 loc => loc
+  | stack512 loc => loc
+  end.
+
+(* State Manipulations *)
+
+Definition getReg {n} (reg: Reg n) (state: State): option (word n) :=
+  match state with
+  | fullState regState stackState =>
+    match (NatM.find n regState) with
+      | Some map =>
+        match (NatM.find (getRegIndex reg) map) with
+        | Some m => Some (NToWord n m)
+        | _ => None
+        end
+      | None => None
+    end
+  end.
+
+Definition setReg {n} (reg: Reg n) (value: word n) (state: State): option State :=
+  match state with
+  | fullState regState stackState =>
+    match (NatM.find n regState) with
+      | Some map =>
+        Some (fullState
+          (NatM.add n (NatM.add (getRegIndex reg) (wordToN value) map)
+            regState) stackState)
+      | None => None
+    end
+  end.
+
+(* Per-word Stack Operations *)
+Definition getStack32 (entry: Stack 32) (state: State): option (word 32) :=
+  match state with
+  | fullState regState stackState =>
+    match entry with
+    | stack32 loc =>
+      match (NatM.find loc stackState) with
+      | Some n => Some (NToWord 32 n)
+      | _ => None
+      end
+    end
+  end.
 
-Definition getReg {n} (reg: Reg n) (state: State): option (word n).
-  destruct state; inversion reg as [L H | L H | L H | L H];
-    destruct (NatM.find n regState) as [map |];
-    first [ destruct (NatM.find L map) as [n0 |] | exact None ];
-    first [ rewrite H; exact (Some (NToWord n n0)) | exact None ].
+Definition setStack32 (entry: Stack 32) (value: word 32) (state: State): option State :=
+  match state with
+  | fullState regState stackState =>
+    match entry with
+    | stack32 loc =>
+      (Some (fullState regState
+                       (NatM.add loc (wordToN value) stackState)))
+    end
+  end.
+
+Notation "'cast' e" := (convert e _) (at level 20).
+
+(* Iterating Stack Operations *)
+Lemma getStackWords_spec: forall {n} (x: Stack n), n = 32 * (getStackWords x).
+Proof. intros; destruct x; simpl; intuition. Qed.
+
+Definition segmentStackWord {n} (x: Stack n) (w: word n): word (32 * (getStackWords x)).
+  intros; destruct x; simpl; intuition.
+Defined.
+
+Definition desegmentStackWord {n} (x: Stack n) (w: word (32 * (getStackWords x))): word n.
+  intros; destruct x; simpl; intuition.
 Defined.
 
-Definition setReg {n} (reg: Reg n) (value: word n) (state: State): State.
-  inversion state; inversion reg as [L H | L H | L H | L H];
-    destruct (NatM.find n regState) as [map |];
-    first [
-       exact
-         (fullState
-           (NatM.add n
-             (NatM.add L (wordToN value) map) regState)
-             stackState)
-     | exact state ].
+Definition getWords' {n} (st: (list (word 32)) * word (32 * n)) :
+    if (Nat.eq_dec n O)
+    then (list (word 32))
+    else (list (word 32)) * word (32 * (n - 1)).
+
+  destruct (Nat.eq_dec n 0) as [H | H];
+    destruct st as [lst w].
+
+  - refine lst.
+
+  - refine (cons (split1 32 (32 * (n - 1)) (cast w)) lst,
+           (split2 32 (32 * (n - 1)) (cast w))); intuition.
+
 Defined.
 
-Definition getStack {n} (entry: Stack n) (state: State): option (word n).
-  destruct state; inversion entry as [L H | L H | L H];
-    destruct (NatM.find n stackState) as [map |];
-    first [ destruct (NatM.find L map) as [n0 |] | exact None ];
-    first [ rewrite H; exact (Some (NToWord n n0)) | exact None ].
+Program Fixpoint getWords'_iter (n: nat) (st: (list (word 32)) * word (32 * n)): list (word 32) :=
+  match n with
+  | O => fst st
+  | (S m) => getWords'_iter m (cast (getWords' st))
+  end.
+Admit Obligations. (* TODO (rsloan): remove admit, shouldn't be hard *)
+
+Definition getWords {len} (wd: word (32 * len)): list (word 32) :=
+  getWords'_iter len ([], wd).
+
+Definition joinWordOpts_expandTerm {n} (w: word (32 + 32 * n)): word (32 * S n).
+  replace (32 * S n) with (32 + 32 * n) by abstract intuition; assumption.
 Defined.
 
-Definition setStack {n} (entry: Stack n) (value: word n) (state: State): State.
-  inversion state; inversion entry as [L H | L H | L H];
-    destruct (NatM.find n stackState) as [map |];
-    first [
-       exact
-         (fullState regState
-           (NatM.add n
-             (NatM.add L (wordToN value) map) regState))
-     | exact state ].
+Fixpoint joinWordOpts (wds: list (option (word 32))): option word :=
+  match wds with
+  | nil => None
+  | (cons wo wos) =>
+    match wo with
+    | None => None
+    | Some w =>
+      match (joinWordOpts wos) with
+      | None => None
+      | (Some joined) =>
+        match joined with
+        | anyWord joinedLen joinedWord =>
+            Some (anyWord (S joinedLen) (joinWordOpts_expandTerm (combine w joinedWord)))
+        end
+      end
+    end
+  end.
+
+Definition setStack {n} (entry: Stack n) (value: word n) (state: State) : option State :=
+  (fix setStack_iter (wds: list (word 32)) (nextLoc: nat) (state: State) :=
+     match wds with
+     | [] => Some state
+     | w :: ws =>
+       match (setStack32 (stack32 nextLoc) w state) with 
+       | Some st' => setStack_iter ws (S nextLoc) st'
+       | None => None
+       end
+     end) (getWords (segmentStackWord entry value)) (getStackIndex entry) state.
+
+Fixpoint getStack_iter (rem: nat) (loc: nat) (state: State): list (option (word 32)) :=
+  match rem with
+  | O => []
+  | (S rem') =>
+    (getStack32 (stack32 loc) state) ::
+      (getStack_iter rem' (loc + 32) state)
+  end.
+
+Obligation Tactic := abstract (unfold Datatypes.length; intuition).
+Fixpoint getStack {n} (entry: Stack n) (state: State) : option (word n).
+  refine (
+    let m := getStackWords entry in
+    let i := getStackIndex entry in
+    let wos := (getStack_iter m i state) in
+    let joined := (joinWordOpts wos) in
+    option_map (fun a => cast a) joined
+  ); intuition.
+
+  replace (Datatypes.length _) with (getStackWords entry); intuition.
+  unfold wds.
+  induction (getStackWords entry); simpl; intuition.
+  destruct entry.
+
+  simpl; intuition.
 Defined.
 
 Definition emptyState: State :=
   fullState (NatM.empty DefMap) (NatM.empty DefMap).
+
+(* For register allocation checking *)
+Definition regCount (base: nat): nat :=
+  match base with
+  | 32 => 7   | 64 => 8
+  | 128 => 8  | 80 => 8
+  | _ => 0
+  end.
+
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index 0504ed3a6..d1b273c98 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -1,5 +1,9 @@
-Require Export Qhasm Language Conversion.
-Require Export String.
+Require Export Language Conversion.
+Require Export Qhasm.
+Require Import QhasmCommon QhasmEvalCommon QhasmUtil.
+Require Export String Ascii.
+Require Import NArith NPeano.
+Require Export Bedrock.Word.
 
 Module QhasmString <: Language.
   Definition Program := string.
@@ -10,9 +14,202 @@ End QhasmString.
 
 Module StringConversion <: Conversion Qhasm QhasmString.
 
+  (* The easy one *)
   Definition convertState (st: QhasmString.State): option Qhasm.State := None.
 
-  (* TODO (rsloan): Actually implement string conversion *)
+  (* Hexadecimal Primitives *)
+
+  Section Hex.
+    Local Open Scope string_scope.
+
+    Definition natToDigit (n : nat) : string :=
+      match n with
+        | 0  => "0"  | 1  => "1"  | 2  => "2"  | 3  => "3"
+        | 4  => "4"  | 5  => "5"  | 6  => "6"  | 7  => "7"
+        | 8  => "8"  | 9  => "9"  | 10 => "A"  | 11 => "B"
+        | 12 => "C"  | 13 => "D"  | 14 => "E"  | _  => "F"
+      end.
+
+    Fixpoint nToHex' (n: N) (digitsLeft: nat): string :=
+        match digitsLeft with
+        | O => ""
+        | S nextLeft =>
+            match n with
+            | N0 => "0"
+            | _ => (nToHex' (N.shiftr_nat n 4) nextLeft) ++
+                (natToDigit (N.to_nat (N.land n 15%N)))
+            end
+        end.
+
+    Definition nToHex (n: N): string :=
+      let size := (N.size n) in
+      let div4 := fun x => (N.shiftr x 2%N) in
+      let size' := (size + 4 - (N.land size 3))%N in
+      nToHex' n (N.to_nat (div4 size')).
+
+  End Hex.
+
+  (* Conversion of elements *)
+
+  Section Elements.
+    Local Open Scope string_scope.
+
+    Definition nameSuffix (n: nat): string := 
+      (nToHex (N.of_nat n)).
+
+    Definition wordToString {n} (w: word n): string := 
+      "0x" ++ (nToHex (wordToN w)).
+
+    Coercion wordToString : word >-> string.
+
+    Definition constToString {n} (c: Const n): string :=
+      match c with
+      | const32 w => "0x" ++ w
+      | const64 w => "0x" ++ w
+      | const128 w => "0x" ++ w
+      end.
+
+    Coercion constToString : Const >-> string.
+
+    Definition indexToString {n} (i: Index n): string :=
+      "0x" ++ (nToHex (N.of_nat i)).
+
+    Coercion indexToString : Index >-> string.
+
+    Definition regToString {n} (r: Reg n): option string :=
+      Some match r with
+      | reg32 n => "ex" ++ (nameSuffix n)
+      | reg3232 n => "mm" ++ (nameSuffix n)
+      | reg6464 n => "xmm" ++ (nameSuffix n)
+      | reg80 n => "st" ++ (nameSuffix n)
+      end.
+
+    Definition stackToString {n} (s: Stack n): option string :=
+      Some match s with
+      | stack32 n => "word" ++ (nameSuffix n)
+      | stack64 n => "double" ++ (nameSuffix n)
+      | stack128 n => "quad" ++ (nameSuffix n)
+      end.
+
+    Definition stackLocation {n} (s: Stack n): word 32 :=
+      combine (natToWord 8 n) (natToWord 24 n).
+
+    Definition assignmentToString (a: Assignment): option string :=
+      match a with
+      | Assign32Stack32 r s =>
+        match (regToString r, stackToString s) with
+        | (Some s0, Some s1) => s0 ++ " = " ++ s1
+        | _ => None
+        end.
+      | Assign32Stack16 r s i => r0 ++ " = " ++ r1
+      | Assign32Stack8 r s i =>
+      | Assign32Stack64 r s i =>
+      | Assign32Stack128 r s i =>
+
+      | Assign32Reg32 r0 r1 => r0 ++ " = " ++ r1 
+      | Assign32Reg16 r0 r1 i =>
+      | Assign32Reg8 r0 r1 i =>
+      | Assign32Reg64 r0 r1 i =>
+      | Assign32Reg128 r0 r1 i =>
+
+      | Assign3232Stack32 r i s =>
+      | Assign3232Stack64 r s =>
+      | Assign3232Stack128 r s i =>
+
+      | Assign3232Reg32 r0 i r1 =>
+      | Assign3232Reg64 r0 r1 =>
+      | Assign3232Reg128 r0 r1 i =>
+
+      | Assign6464Reg32 r0 i r1 =>
+      | Assign6464Reg64 r0 i r1 =>
+      | Assign6464Reg128 r0 r1 =>
+
+      | AssignConstant r c =>
+      end.
+
+    Definition binOpToString (b: BinOp): string :=
+      match b with
+      | Plus => "+"
+      | Minus => "-"
+      | Mult => "*"
+      | Div => "/"
+      | Xor => "^"
+      | And => "&"
+      | Or => "|"
+      end.
+
+    Definition rotOpToString (r: RotOp): string :=
+      match r with
+      | Shl => "<<"
+      | Shr => ">>"
+      | Rotl => "<<<"
+      | Rotr => ">>>"
+      end.
+
+    Definition operationToString (o: Operation): string :=
+      match o with
+      | OpReg32Constant b r c =>
+        (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c)
+      | OpReg32Reg32 b r0 r1 =>
+        (regToString r0) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString r1)
+      | RotReg32 o r i =>
+        (regToString r) ++ " " ++ (rotOpToString o) ++ "= " ++ (constToString i)
+
+      | OpReg64Constant b r c =>
+        (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c)
+      | OpReg64Reg64 b r0 r1 =>
+        (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c)
+
+      | OpReg128Constant b r c =>
+        (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c)
+      | OpReg128Reg128 b r0 r1 =>
+        (regToString r) ++ " " ++ (binOpToString b) ++ "= " ++ (constToString c)
+      end.
+
+    Definition testOpToString (t: TestOp): string :=
+      match t with
+      | TEq =>
+      | TLt =>
+      | TUnsignedLt =>
+      | TGt =>
+      | TUnsignedGt =>
+      end.
+
+    Definition conditionalToString (c: Conditional): string :=
+      match c with
+      | TestTrue =>
+      | TestFalse =>
+      | TestReg32Reg32 o i r0 r1 =>
+      | TestReg32Const o i r c =>
+      end.
+
+  End Elements.
+
+  Section Parsing.
+
+    Inductive Entry :=
+      | regEntry: forall n, Reg n => Entry
+      | stackEntry: forall n, Stack n => Entry
+      | constEntry: forall n, Const n => Entry.
+
+    Definition allRegs (prog: Qhasm.Program): list Entry := [(* TODO *)]
+
+  End Parsing.
+
+  (* Macroscopic Conversion Methods *)
+
+  Definition convertStatement (statement: Qhasm.QhasmStatement): string :=
+    match prog with
+    | QAssign a =>
+    | QOp o =>
+    | QJmp c l =>
+    | QLabel l =>
+    end.
+
+  Definition convertProgramPrologue (prog: Qhasm.Program): option string :=
+
+  Definition convertProgramEpilogue (prog: Qhasm.Program): option string :=
+
   Definition convertProgram (prog: Qhasm.Program): option string :=
     Some EmptyString.