Merge branch 'develop' of github.com:ymherklotz/coqup into byte-addressing

1 files changed, 22 insertions, 11 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 09af28a..65b6627 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -432,24 +432,35 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
   match ni with
     (n, i) =>
     match i with
-    | Inop n' => add_instr n n' Vskip
+    | Inop n' =>
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+        add_instr n n' Vskip
+      else error (Errors.msg "State is larger than 2^32.")
     | Iop op args dst n' =>
-      do instr <- translate_instr op args;
-      do _ <- declare_reg None dst 32;
-      add_instr n n' (nonblock dst instr)
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned then
+        do instr <- translate_instr op args;
+        do _ <- declare_reg None dst 32;
+        add_instr n n' (nonblock dst instr)
+      else error (Errors.msg "State is larger than 2^32.")
     | Iload mem addr args dst n' =>
-      do addr' <- translate_eff_addressing addr args;
-      do _ <- declare_reg None dst 32;
-      add_instr n n' $ create_single_cycle_load stack addr' dst
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned
+      then do addr' <- translate_eff_addressing addr args;
+           do _ <- declare_reg None dst 32;
+           add_instr n n' $ create_single_cycle_load stack addr' dst
+      else error (Errors.msg "State is larger than 2^32.")
     | Istore mem addr args src n' =>
-      do addr' <- translate_eff_addressing addr args;
-      add_instr n n' $ create_single_cycle_store stack addr' src
+      if Z.leb (Z.pos n') Integers.Int.max_unsigned
+      then do addr' <- translate_eff_addressing addr args;
+           add_instr n n' $ create_single_cycle_store stack addr' src
+      else error (Errors.msg "State is larger than 2^32.")
     | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
     | Icond cond args n1 n2 =>
-      do e <- translate_condition cond args;
-      add_branch_instr e n n1 n2
+      if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned then
+        do e <- translate_condition cond args;
+        add_branch_instr e n n1 n2
+      else error (Errors.msg "State is larger than 2^32.")
     | Ijumptable r tbl =>
       do s <- get;
       add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))