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/HTLgenproof.v | |
parent | 6b20fbbeaad23724ca7fbcc10c9445f5cb94b699 (diff) | |
download | vericert-b59a2e2913aa7ad010c0652e909ae790c07c7281.tar.gz vericert-b59a2e2913aa7ad010c0652e909ae790c07c7281.zip |
Enforce stack size alignment to fix proof.
Diffstat (limited to 'src/translation/HTLgenproof.v')
-rw-r--r-- | src/translation/HTLgenproof.v | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index a5396af..77a11dc 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -482,8 +482,8 @@ Section CORRECTNESS. (** Here we are assuming that any stack read will be within the bounds of the activation record. *) - assert (0 <= Integers.Ptrofs.unsigned i0 / 4) as READ_BOUND_LOW by admit. - assert (Integers.Ptrofs.unsigned i0 / 4 < f.(RTL.fn_stacksize) / 4) as READ_BOUND_HIGH by admit. + assert (0 <= Integers.Ptrofs.unsigned i0) as READ_BOUND_LOW by admit. + assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH by admit. eexists. split. eapply Smallstep.plus_one. @@ -509,16 +509,25 @@ Section CORRECTNESS. (** Equality proof *) (* FIXME: 32-bit issue. *) assert (forall x, valueToNat (ZToValue 32 x) = Z.to_nat x) as VALUE_IDENTITY by admit. - assert (4 * (Integers.Ptrofs.unsigned i0 / 4) = Integers.Ptrofs.unsigned i0) as MOD_IDENTITY. - { - rewrite Z.mul_comm. - rewrite ZLib.div_mul_undo; lia. - } rewrite VALUE_IDENTITY. specialize (H5 (Integers.Ptrofs.unsigned i0 / 4)). rewrite Z2Nat.id in H5; try lia. exploit H5; auto; intros. - rewrite MOD_IDENTITY in H0. + 1: { + split. + - apply Z.div_pos; lia. + - apply Zmult_lt_reg_r with (p := 4); try lia. + repeat rewrite ZLib.div_mul_undo; lia. + } + 2: { + assert (0 < RTL.fn_stacksize f) by lia. + apply Z.div_pos; lia. + } + replace (4 * (Integers.Ptrofs.unsigned i0 / 4)) with (Integers.Ptrofs.unsigned i0) in H0. + 2: { + rewrite Z.mul_comm. + rewrite ZLib.div_mul_undo; lia. + } rewrite Integers.Ptrofs.repr_unsigned in H0. rewrite H1 in H0. invert H0. assumption. |