Simpler QhasmCommon grammar

updating QhasmCommon

Pushing through changes

Pushing through changes

Pushing through changes

Pushing through changes

Pushing through changes

Pushing through changes

1 files changed, 126 insertions, 278 deletions

diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 009bcbd1e..92c27bb72 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -1,322 +1,170 @@
 Require Export QhasmCommon QhasmUtil State.
-Require Export ZArith.
+Require Export ZArith Sumbool.
 Require Export Bedrock.Word.
 
 Import State.
 Import Util.
 
-Definition evalTest {n} (o: TestOp) (invert: bool) (a b: word n): bool :=
-  xorb invert
+Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
+  let c := (N.compare (wordToN a) (wordToN b)) in
+
+  let eqBit := match c with | Eq => true | _ => false end in
+  let ltBit := match c with | Lt => true | _ => false end in
+  let gtBit := match c with | Gt => true | _ => false end in
+
   match o with
-  | TEq => weqb a b
-  | TLt =>
-    match (Z.compare (wordToZ a) (wordToZ b)) with
-    | Lt => true
-    | _ => false
-    end
-  | TUnsignedLt =>
-    match (N.compare (wordToN a) (wordToN b)) with
-    | Lt => true
-    | _ => false
-    end
-  | TGt =>
-    match (Z.compare (wordToZ a) (wordToZ b)) with
-    | Gt => true
-    | _ => false
-    end
-  | TUnsignedGt =>
-    match (N.compare (wordToN a) (wordToN b)) with
-    | Gt => true
-    | _ => false
-    end
+  | TEq => eqBit
+  | TLt => ltBit
+  | TLe => orb (eqBit) (ltBit)
+  | TGt => gtBit
+  | TGe => orb (eqBit) (gtBit)
   end.
 
-Definition evalCond (c: Conditional) (state: State): option bool :=
-  match c with
+Definition evalCond (c: Conditional) (state: State): option bool.
+  refine match c with
   | TestTrue => Some true
   | TestFalse => Some false
-  | TestReg32Reg32 o i r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r0 state) with
-      | Some v1 => Some (evalTest o i v0 v1)
+  | TestInt n t a b => 
+    match (getIntReg a state) with
+    | Some va =>
+      match (getIntReg b state) with
+      | Some vb => Some (evalTest t va vb)
       | _ => None
       end
     | _ => None
     end
-  | TestReg32Const o i r x =>
-    match (getReg r state) with
-    | Some v0 =>
-      match x with
-      | const32 v1 => Some (evalTest o i v0 v1)
+
+  | TestFloat n t a b =>
+    let aOpt := (getFloatReg a state) in
+    let bOpt := convert (getFloatReg a state) _ in
+
+    match aOpt with
+    | Some va =>
+      match bOpt with
+      | Some vb => Some (evalTest t va vb)
+      | _ => None
       end
     | _ => None
     end
-  end.
+  end; abstract (
+    inversion a; inversion b;
+    unfold aOpt, getFractionalBits;
+    simpl; intuition).
+Defined.
+
+Definition evalOperation (o: Operation) (state: State): option State.
+  refine (
+  let evalIOp := fun {b} (io: IntOp) (x y: word b) =>
+    match io with
+    | IPlus => wplus x y
+    | IMinus => wminus x y
+    | IXor => wxor x y
+    | IAnd => wand x y
+    | IOr => wor x y
+    end in
+
+  let evalFOp := fun {b} (fo: FloatOp) (x y: word b) =>
+    match fo with
+    | FAnd => wand x y
+    | FPlus => wplus x y
+    | FMult => wmult x y
+    end in
+
+  let evalRotOp := fun {b} (ro: RotOp) (x: word b) (n: nat) =>
+    match ro with
+    | Shl => NToWord b (N.shiftl_nat (wordToN x) n)
+    | Shr => NToWord b (N.shiftr_nat (wordToN x) n)
+    end in
+
+  let liftOpt := fun {A B C} (f: A -> B -> option C) (xo: option A) (yo: option B) =>
+    match (xo, yo) with
+    | (Some x, Some y) => f x y
+    | _ => None
+    end in
 
-Definition evalBinOp {n} (o: BinOp) (a b: word n): word n :=
   match o with
-  | Plus => wplus a b
-  | Minus => wminus a b
-  | Mult => wmult a b
-  | Div => NToWord n ((wordToN a) / (wordToN b))%N
-  | Or => wor a b
-  | Xor => wxor a b
-  | And => wand a b
-  end.
+  | IOpConst o r c =>
+    liftOpt (fun x y => setIntReg r (evalIOp o x y) state)
+      (getIntReg r state)
+      (match c with | constInt32 v => Some v end)
 
-Definition evalRotOp {n} (o: RotOp) (a: word n) (m: nat): word n :=
-  match o with
-  | Shl => NToWord n (N.shiftl_nat (wordToN a) m)
-  | Shr => NToWord n (N.shiftr_nat (wordToN a) m)
+  | IOpReg o a b =>
+    liftOpt (fun x y => setIntReg a (evalIOp o x y) state)
+      (getIntReg a state) (getIntReg b state)
 
-  (* TODO (rsloan): not actually rotate operations *)
-  | Rotl => NToWord n (N.shiftl_nat (wordToN a) m)
-  | Rotr => NToWord n (N.shiftr_nat (wordToN a) m)
-  end.
+  | FOpConst32 o r c =>
+    liftOpt (fun x y => setFloatReg r (evalFOp o x y) state)
+      (getFloatReg r state)
+      (match c with | constFloat32 v => Some (convert v _) end)
 
-Definition evalOperation (o: Operation) (state: State): option State :=
-  match o with
-  | OpReg32Constant b r c =>
-    match (getReg r state) with
-    | Some v0 =>
-      match c with
-      | const32 v1 => setReg r (evalBinOp b v0 v1) state
-      end
-    | None => None
-    end
+  | FOpReg32 o a b =>
+    liftOpt (fun x y => setFloatReg a (evalFOp o x y) state)
+      (getFloatReg a state) (convert (getFloatReg b state) _)
 
-  | OpReg32Reg32 b r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (evalBinOp b v0 v1) state
-      | _ => None
-      end
-    | None => None
-    end
+  | FOpConst64 o r c =>
+    liftOpt (fun x y => setFloatReg r (evalFOp o x y) state)
+      (getFloatReg r state)
+      (match c with | constFloat64 v => Some (convert v _) end)
 
-  | RotReg32 b r m =>
-    match (getReg r state) with
-    | Some v0 => setReg r (evalRotOp b v0 m) state
-    | None => None
-    end
+  | FOpReg64 o a b =>
+    liftOpt (fun x y => setFloatReg a (evalFOp o x y) state)
+      (getFloatReg a state) (convert (getFloatReg b state) _)
 
-  | OpReg64Constant b r c =>
-    match (getReg r state) with
-    | Some v0 =>
-      match c with
-      | const64 v1 => setReg r (evalBinOp b v0 v1) state
-      end
+  | OpRot o r i =>
+   match (getIntReg r state) with
+    | Some va => setIntReg r (evalRotOp o va i) state
     | None => None
     end
+  end); abstract intuition.
+Defined.
 
-  | OpReg64Reg64 b r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (evalBinOp b v0 v1) state
-      | _ => None
-      end
-    | None => None
-    end
+Definition getIConst {n} (c: IConst n): word n :=
+  match c with
+  | constInt32 v => v
+  end.
 
-  (* Don't implement the 128-wide ops yet:
-     I think x86 doesn't do them like this *)
-  | _ => None end.
+Definition getFConst {n} (c: FConst n): word n :=
+  match c with
+  | constFloat32 v => v
+  | constFloat64 v => v
+  end.
 
 Definition evalAssignment (a: Assignment) (state: State): option State :=
-  match a with
-  | Assign32Stack32 r s =>
-    match (getReg r state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r v1 state
-      | _ => None
-      end
-    | None => None
-    end
-
-  | Assign32Stack16 r s i =>
-    match (getReg r state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r (trunc 32 (getIndex v1 16 i)) state
-      | _ => None
-      end
-    | None => None
-    end
-  | Assign32Stack8 r s i =>
-    match (getReg r state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r (trunc 32 (getIndex v1 8 i)) state
-      | _ => None
-      end
-    | None => None
-    end
-  | Assign32Stack64 r s i =>
-    match (getReg r state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r (getIndex v1 32 i) state
-      | _ => None
-      end
-    | None => None
-    end
-  | Assign32Stack128 r s i =>
-    match (getReg r state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r (getIndex v1 32 i) state
-      | _ => None
-      end
-    | None => None
-    end
-
-  | Assign32Reg32 r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 v1 state
-      | _ => None
-      end
-    | None => None
-    end
-  | Assign32Reg16 r0 r1 i =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (trunc 32 (getIndex v1 16 i)) state
-      | _ => None
-      end
-    | None => None
-    end
-  | Assign32Reg8 r0 r1 i =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (trunc 32 (getIndex v1 8 i)) state
-      | _ => None
-      end
-    | None => None
-    end
-  | Assign32Reg64 r0 r1 i =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (getIndex v1 32 i) state
-      | _ => None
-      end
-    | None => None
-    end
-  | Assign32Reg128 r0 r1 i =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (getIndex v1 32 i) state
-      | _ => None
-      end
-    | None => None
-    end
+  let liftOpt := fun {A B} (f: A -> option B) (xo: option A) =>
+    match xo with
+    | (Some x') => f x'
+    | _ => None
+    end in
 
-  | Assign3232Stack32 r0 i s =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => None
-      end
-    | None => None
-    end
+  match a with
+  | ARegStackInt n r s =>
+    liftOpt (fun x => setIntReg r x state) (getStack s state)
 
-  | Assign3232Stack64 r s =>
-    match (getReg r state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r v1 state
-      | _ => None
-      end
-    | None => None
-    end
+  | ARegStackFloat n r s =>
+    liftOpt (fun x => setFloatReg r x state) (getStack s state)
 
-  | Assign3232Stack128 r s i =>
-    match (getReg r state) with
-    | Some v0 =>
-      match (getStack s state) with
-      | Some v1 => setReg r (getIndex v1 64 i) state
-      | _ => None
-      end
-    | None => None
-    end
+  | AStackRegInt n s r =>
+    liftOpt (fun x => setStack s x state) (getIntReg r state)
 
-  | Assign3232Reg32 r0 i r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => None
-      end
-    | None => None
-    end
+  | AStackRegFloat n s r =>
+    liftOpt (fun x => setStack s x state) (getFloatReg r state)
 
-  | Assign3232Reg64 r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 v1 state
-      | _ => None
-      end
-    | None => None
-    end
+  | ARegRegInt n a b =>
+    liftOpt (fun x => setIntReg a x state) (getIntReg b state)
 
-  | Assign3232Reg128 r0 r1 i =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (getIndex v1 64 i) state
-      | _ => None
-      end
-    | None => None
-    end
+  | ARegRegFloat n a b =>
+    liftOpt (fun x => setFloatReg a x state) (getFloatReg b state)
 
-  | Assign6464Reg32 r0 i r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => None
-      end
-    | None => None
-    end
+  | AConstInt n r c => setIntReg r (getIConst c) state
 
-  | Assign6464Reg64 r0 i r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => None
-      end
-    | None => None
-    end
+  | AConstFloat n r c => setFloatReg r (getFConst c) state
 
-  | Assign6464Reg128 r0 r1 =>
-    match (getReg r0 state) with
-    | Some v0 =>
-      match (getReg r1 state) with
-      | Some v1 => setReg r0 v1 state
-      | _ => None
-      end
-    | None => None
+  | AIndex n m a b i =>
+    match (getIntReg b state) with
+    | Some v => setIntReg a (trunc n (getIndex v m i)) state
+    | _ => None
     end
 
-  | AssignConstant r c =>
-    match (getReg r state) with
-    | Some v0 =>
-      match c with
-      | const32 v1 => setReg r v1 state
-      end
-    | None => None
-    end
+  | APtr n r s =>
+    setIntReg r (NToWord 32 (N.of_nat (getStackIndex s))) state 
   end.
-