diff options
Diffstat (limited to 'src/translation/HTLgenspec.v')
| -rw-r--r-- | src/translation/HTLgenspec.v | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 7d89a76..a78256b 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -140,7 +140,7 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - forall mem addr args s s' i c src n, translate_arr_access mem addr args stk s = OK c s' i -> tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) - (state_goto st n). + (state_goto st n) | tr_instr_Ijumptable : forall cexpr tbl r, cexpr = tbl_to_case_expr st tbl -> @@ -165,6 +165,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> m = (mkmodule f.(RTL.fn_params) data control @@ -421,13 +422,18 @@ Proof. inversion s; subst. unfold transf_module in *. - destruct (Z.eq_dec (RTL.fn_stacksize f mod 4) 0); monadInv Heqr. + unfold stack_correct in *. + destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; + destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH; + destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN; + simplify; + monadInv Heqr. (* TODO: We should be able to fold this into the automation. *) pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. rewrite <- STK_LEN. - econstructor; simpl; trivial. + econstructor; simpl; auto. intros. inv_incr. assert (EQ3D := EQ3). |