Breaking out State into its own file

1 files changed, 61 insertions, 58 deletions

diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index 312f30e03..ec54fdc47 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -1,7 +1,9 @@
-Require Export QhasmCommon.
-Require Export QhasmUtil.
-
+Require Export QhasmCommon QhasmUtil State.
 Require Export ZArith.
+Require Export Bedrock.Word.
+
+Import State.
+Import Util.
 
 Definition evalTest {n} (o: TestOp) (invert: bool) (a b: word n): bool :=
   xorb invert
@@ -73,30 +75,30 @@ Definition evalRotOp {n} (o: RotOp) (a: word n) (m: nat): word n :=
   | Rotr => NToWord n (N.shiftr_nat (wordToN a) m)
   end.
 
-Definition evalOperation (o: Operation) (state: State): State :=
+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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | 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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | RotReg32 b r m =>
     match (getReg r state) with
     | Some v0 => setReg r (evalRotOp b v0 m) state
-    | None => state
+    | None => None
     end
 
   | OpReg64Constant b r c =>
@@ -104,18 +106,18 @@ Definition evalOperation (o: Operation) (state: State): State :=
     | Some v0 =>
       match c with
       | const64 v1 => setReg r (evalBinOp b v0 v1) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | 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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | OpReg128Constant b r c =>
@@ -123,67 +125,67 @@ Definition evalOperation (o: Operation) (state: State): State :=
     | Some v0 =>
       match c with
       | const128 v1 => setReg r (evalBinOp b v0 v1) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   | OpReg128Reg128 b r0 r1 =>
     match (getReg r0 state) with
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (evalBinOp b v0 v1) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   end.
 
-Definition evalAssignment (a: Assignment) (state: State): State :=
+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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | 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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | 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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | 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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | 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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign32Reg32 r0 r1 =>
@@ -191,45 +193,45 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | 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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | 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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | 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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | 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
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Stack32 r0 i s =>
@@ -237,9 +239,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Stack64 r s =>
@@ -247,9 +249,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Stack128 r s i =>
@@ -257,9 +259,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getStack s state) with
       | Some v1 => setReg r (getIndex v1 64 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Reg32 r0 i r1 =>
@@ -267,9 +269,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Reg64 r0 r1 =>
@@ -277,9 +279,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign3232Reg128 r0 r1 i =>
@@ -287,9 +289,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (getIndex v1 64 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign6464Reg32 r0 i r1 =>
@@ -297,9 +299,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign6464Reg64 r0 i r1 =>
@@ -307,9 +309,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 (setInPlace v0 v1 i) state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | Assign6464Reg128 r0 r1 =>
@@ -317,9 +319,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match (getReg r1 state) with
       | Some v1 => setReg r0 v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
 
   | AssignConstant r c =>
@@ -327,8 +329,9 @@ Definition evalAssignment (a: Assignment) (state: State): State :=
     | Some v0 =>
       match c with
       | const32 v1 => setReg r v1 state
-      | _ => state
+      | _ => None
       end
-    | None => state
+    | None => None
     end
   end.
+