1 files changed, 101 insertions, 90 deletions
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index b6261d1c6..ea39a04ac 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -22,112 +22,123 @@ Definition evalTest {n} (o: TestOp) (a b: word n): bool :=
 
 Definition evalCond (c: Conditional) (state: State): option bool :=
   match c with
-  | TestTrue => Some true
-  | TestFalse => Some false
-  | 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
+  | CTrue => Some true
+  | CZero n r =>
+    omap (getReg r state) (fun v =>
+      if (Nat.eq_dec O (wordToNat v))
+      then Some true
+      else Some false) 
+  | CReg n o a b =>
+    omap (getReg a state) (fun va =>
+      omap (getReg b state) (fun vb =>
+        Some (evalTest o va vb)))
+  | CConst n o a c => 
+    omap (getReg a state) (fun va =>
+      Some (evalTest o va (constValueW c)))
   end.
 
-Definition evalIOp {b} (io: IntOp) (x y: word b) :=
+Definition evalIntOp {b} (io: IntOp) (x y: word b): (word b) * option bool :=
   match io with
-  | IPlus => wplus x y
-  | IMinus => wminus x y
-  | IXor => wxor x y
-  | IAnd => wand x y
-  | IOr => wor x y
+  | Add =>
+    let v := (wordToN x + wordToN y)%N in
+    let c := (N.compare v (Npow2 b)) in
+
+    match c as c' return c' = c -> _ with
+    | Lt => fun _ => (NToWord b v, Some false)
+    | _ => fun _ => (NToWord b v, Some true)
+    end eq_refl
+
+  | Sub => (wminus x y, None)
+  | Xor => (wxor x y, None)
+  | And => (wand x y, None)
+  | Or => (wor x y, None)
   end.
 
-Definition evalRotOp {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)
+Definition evalCarryOp {b} (io: CarryOp) (x y: word b) (c: bool): (word b) * bool :=
+  match io with
+  | AddWidthCarry =>
+    let v := (wordToN x + wordToN y + (if c then 1%N else 0%N))%N in
+    let c := (N.compare v (Npow2 b)) in
+
+    match c as c' return c' = c -> _ with
+    | Lt => fun _ => (NToWord b v, false)
+    | _ => fun _ => (NToWord b v, true)
+    end eq_refl
   end.
 
 Definition evalDualOp {b} (duo: DualOp) (x y: word b) :=
   match duo with
-  | IMult =>
-    let wres := natToWord (b + b) (N.to_nat ((wordToN x) * (wordToN y))) in
+  | Mult =>
+    let v := (wordToN x * wordToN y)%N in
+    let wres := NToWord (b + b) v in
     (split1 b b wres, split2 b b wres)
   end.
 
-Definition evalOperation (o: Operation) (state: State): option State :=
-  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
-
-  match o with
-  | IOpConst n o r c =>
-    liftOpt (fun x y => setIntReg r (evalIOp o x y) state)
-      (getIntReg r state)
-      (match c with | constInt32 v => Some v | constInt64 v => Some v end)
-
-  | IOpReg n o a b =>
-    liftOpt (fun x y => setIntReg a (evalIOp o x y) state)
-      (getIntReg a state) (getIntReg b state)
-
-  | DOpReg n o a b h =>
-    liftOpt (fun x y =>
-        match (evalDualOp o x y) with
-        | (lw, hw) =>
-          match (setIntReg a lw state) with
-          | Some st' =>
-            match h with
-            | Some hr => setIntReg hr hw st'
-            | _ => Some st'
-            end
-          | None => None
-          end
-        end)
-      (getIntReg a state) (getIntReg b state)
-
-  | OpRot n o r i =>
-   match (getIntReg r state) with
-    | Some va => setIntReg r (evalRotOp o va i) state
-    | None => None
-    end
+Definition evalRotOp {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.
 
-Definition getIConst {n} (c: IConst n): word n :=
-  match c with
-  | constInt32 v => v
-  | constInt64 v => v
+Definition evalOperation (o: Operation) (state: State): option State :=
+  match o with
+  | IOpConst _ o r c =>
+    omap (getReg r state) (fun v =>
+      let (v', co) := (evalIntOp o v (constValueW c)) in
+      Some (setCarryOpt co (setReg r v' state)))
+
+  | IOpReg _ o a b =>
+    omap (getReg a state) (fun va =>
+      omap (getReg b state) (fun vb =>
+        let (v', co) := (evalIntOp o va vb) in
+        Some (setCarryOpt co (setReg a v' state))))
+
+  | IOpMem _ _ o r m i => 
+    omap (getReg r state) (fun va =>
+      omap (getMem m i state) (fun vb =>
+        let (v', co) := (evalIntOp o va vb) in
+        Some (setCarryOpt co (setReg r v' state))))
+
+  | DOp _ o a b (Some x) => 
+    omap (getReg a state) (fun va =>
+      omap (getReg b state) (fun vb =>
+        let (low, high) := (evalDualOp o va vb) in
+        Some (setReg x high (setReg a low state))))
+
+  | DOp _ o a b None => 
+    omap (getReg a state) (fun va =>
+      omap (getReg b state) (fun vb =>
+        let (low, high) := (evalDualOp o va vb) in
+        Some (setReg a low state)))
+
+  | ROp _ o r i => 
+    omap (getReg r state) (fun v =>
+      let v' := (evalRotOp o v i) in
+      Some (setReg r v' state))
+
+  | COp _ o a b => 
+    omap (getReg a state) (fun va =>
+      omap (getReg b state) (fun vb =>
+        match (getCarry state) with
+        | None => None
+        | Some c0 => 
+          let (v', c') := (evalCarryOp o va vb c0) in
+          Some (setCarry c' (setReg a v' state))
+        end))
   end.
 
-
 Definition evalAssignment (a: Assignment) (state: State): option State :=
-  let liftOpt := fun {A B} (f: A -> option B) (xo: option A) =>
-    match xo with
-    | (Some x') => f x'
-    | _ => None
-    end in
-
   match a with
-  | ARegStackInt n r s =>
-    liftOpt (fun x => setIntReg r x state) (getStack s state)
-
-  | AStackRegInt n s r =>
-    liftOpt (fun x => setStack s x state) (getIntReg r state)
-
-  | ARegRegInt n a b =>
-    liftOpt (fun x => setIntReg a x state) (getIntReg b state)
-
-  | AConstInt n r c => setIntReg r (getIConst c) state
-
-  | AIndex n m a b i =>
-    match (getStack b state) with
-    | Some v => setIntReg a (trunc n (getIndex v m i)) state
-    | _ => None
-    end
-
-  | APtr n r s =>
-    setIntReg r (NToWord 32 (N.of_nat (getStackIndex s))) state 
+  | ARegMem _ _ r m i => 
+    omap (getMem m i state) (fun v => Some (setReg r v state))
+  | AMemReg _ _ m i r =>
+    omap (getReg r state) (fun v => Some (setMem m i v state))
+  | AStackReg _ a b =>
+    omap (getReg b state) (fun v => Some (setStack a v state))
+  | ARegStack _ a b =>
+    omap (getStack b state) (fun v => Some (setReg a v state))
+  | ARegReg _ a b => 
+    omap (getReg b state) (fun v => Some (setReg a v state))
+  | AConstInt _ r c =>
+    Some (setReg r (constValueW c) state)
   end.