diff options
Diffstat (limited to 'src/translation/HTLgen.v')
-rw-r--r-- | src/translation/HTLgen.v | 33 |
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)) |