diff options
| author | James Pollard <james@pollard.dev> | 2020-06-18 17:47:21 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-18 17:47:21 +0100 |
| commit | b59a2e2913aa7ad010c0652e909ae790c07c7281 (patch) | |
| tree | 0942c72c352dbf73e7d63190ea04c7d7b668d9e8 /src/translation/HTLgen.v | |
| parent | 6b20fbbeaad23724ca7fbcc10c9445f5cb94b699 (diff) | |
| download | vericert-kvx-b59a2e2913aa7ad010c0652e909ae790c07c7281.tar.gz vericert-kvx-b59a2e2913aa7ad010c0652e909ae790c07c7281.zip | |
Enforce stack size alignment to fix proof.
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 73f2b63..f661aa6 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -436,6 +436,7 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := (create_arr_state_incr s sz ln i). Definition transf_module (f: function) : mon module := + if (Z.eq_dec (Z.modulo f.(fn_stacksize) 4) 0) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); @@ -459,7 +460,8 @@ Definition transf_module (f: function) : mon module := rst clk current_state.(st_scldecls) - current_state.(st_arrdecls)). + current_state.(st_arrdecls)) + else error (Errors.msg "Stack size misalignment."). Definition max_state (f: function) : state := let st := Pos.succ (max_reg_function f) in |