From b59a2e2913aa7ad010c0652e909ae790c07c7281 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 18 Jun 2020 17:47:21 +0100 Subject: Enforce stack size alignment to fix proof. --- src/translation/HTLgen.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/translation/HTLgen.v') 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 -- cgit