Fix Qhasm and AlmostQhasm with new State machinery

3 files changed, 23 insertions, 30 deletions

diff --git a/src/Assembly/AlmostQhasm.v b/src/Assembly/AlmostQhasm.v
index 31128fbfb..0ec47fc37 100644
--- a/src/Assembly/AlmostQhasm.v
+++ b/src/Assembly/AlmostQhasm.v
@@ -4,6 +4,7 @@ Require Import List.
 
 Module AlmostQhasm <: Language.
   Import ListNotations.
+  Import State.
 
   (* A constant upper-bound on the number of operations we run *)
   Definition maxOps: nat := 1000.
@@ -44,8 +45,8 @@ Module AlmostQhasm <: Language.
       | (Some st') => eval b st'
       | _ => None
       end
-    | AAssign a => Some (evalAssignment a state)
-    | AOp a => Some (evalOperation a state)
+    | AAssign a => evalAssignment a state
+    | AOp a => evalOperation a state
     | ACond c a b =>
       if (evalCond c state)
       then eval a state
diff --git a/src/Assembly/Qhasm.v b/src/Assembly/Qhasm.v
index 05e607462..00961a49a 100644
--- a/src/Assembly/Qhasm.v
+++ b/src/Assembly/Qhasm.v
@@ -4,6 +4,7 @@ Require Import List NPeano.
 
 Module Qhasm <: Language.
   Import ListNotations.
+  Import State.
 
   (* A constant upper-bound on the number of operations we run *)
   Definition maxOps: nat := 1000.
@@ -45,20 +46,26 @@ Module Qhasm <: Language.
           match stmt with
           | QAssign a => (evalAssignment a state, None)
           | QOp o => (evalOperation o state, None)
-          | QLabel l => (state, None)
+          | QLabel l => (Some state, None)
           | QJmp c l =>
             if (evalCond c state)
-            then (state, Some l)
-            else (state, None)
+            then (Some state, Some l)
+            else (Some state, None)
           end
         in
           match jmp with
           | None =>
             if (Nat.eq_dec loc maxLoc)
-            then Some nextState
-            else eval' prog nextState (S loc) h labelMap maxLoc
+            then nextState
+            else match nextState with
+              | Some st' => eval' prog st' (S loc) h labelMap maxLoc
+              | _ => None
+              end
           | Some nextLoc =>
-            eval' prog nextState nextLoc h labelMap nextLoc
+            match nextState with
+            | Some st' => eval' prog st' nextLoc h labelMap maxLoc
+            | _ => None
+            end
           end
       | None => None
       end
diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index ec54fdc47..009bcbd1e 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -82,10 +82,10 @@ Definition evalOperation (o: Operation) (state: State): option State :=
     | Some v0 =>
       match c with
       | const32 v1 => setReg r (evalBinOp b v0 v1) state
-      | _ => None
       end
     | None => None
     end
+
   | OpReg32Reg32 b r0 r1 =>
     match (getReg r0 state) with
     | Some v0 =>
@@ -95,6 +95,7 @@ Definition evalOperation (o: Operation) (state: State): option State :=
       end
     | None => None
     end
+
   | RotReg32 b r m =>
     match (getReg r state) with
     | Some v0 => setReg r (evalRotOp b v0 m) state
@@ -106,10 +107,10 @@ Definition evalOperation (o: Operation) (state: State): option State :=
     | Some v0 =>
       match c with
       | const64 v1 => setReg r (evalBinOp b v0 v1) state
-      | _ => None
       end
     | None => None
     end
+
   | OpReg64Reg64 b r0 r1 =>
     match (getReg r0 state) with
     | Some v0 =>
@@ -120,25 +121,9 @@ Definition evalOperation (o: Operation) (state: State): option State :=
     | None => None
     end
 
-  | OpReg128Constant b r c =>
-    match (getReg r state) with
-    | Some v0 =>
-      match c with
-      | const128 v1 => setReg r (evalBinOp b v0 v1) state
-      | _ => None
-      end
-    | 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
-      | _ => None
-      end
-    | None => None
-    end
-  end.
+  (* Don't implement the 128-wide ops yet:
+     I think x86 doesn't do them like this *)
+  | _ => None end.
 
 Definition evalAssignment (a: Assignment) (state: State): option State :=
   match a with
@@ -151,6 +136,7 @@ Definition evalAssignment (a: Assignment) (state: State): option State :=
       end
     | None => None
     end
+
   | Assign32Stack16 r s i =>
     match (getReg r state) with
     | Some v0 =>
@@ -329,7 +315,6 @@ Definition evalAssignment (a: Assignment) (state: State): option State :=
     | Some v0 =>
       match c with
       | const32 v1 => setReg r v1 state
-      | _ => None
       end
     | None => None
     end