diff options
| author | James Pollard <james@pollard.dev> | 2020-06-22 18:38:22 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-22 18:38:22 +0100 |
| commit | 91c19499997ffc7f1e78f7bf0908b43615cf67f1 (patch) | |
| tree | 6ec10f308113862cdbd912afc952eda39792d0f5 /src/translation/HTLgen.v | |
| parent | be6ad3cd886b3ea79abe6addc2f2add779f55292 (diff) | |
| download | vericert-kvx-91c19499997ffc7f1e78f7bf0908b43615cf67f1.tar.gz vericert-kvx-91c19499997ffc7f1e78f7bf0908b43615cf67f1.zip | |
Start Aindexed proof.
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 2364a0f..cc6a3f8 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -252,7 +252,10 @@ Definition check_address_parameter (p : Z) : bool := Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) - | Op.Aindexed off, r1::nil => ret (boplitz Vadd r1 off) + | Op.Aindexed off, r1::nil => + if (check_address_parameter off) + then ret (boplitz Vadd r1 off) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Ascaled scale offset, r1::nil => if (check_address_parameter scale) && (check_address_parameter offset) then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) @@ -345,7 +348,9 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) (args : list reg) (stack : reg) : mon expr := match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) | Mint32, Op.Aindexed off, r1::nil => - ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4))))) + if (check_address_parameter off) + then ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4))))) + else error (Errors.msg "Veriloggen: translate_arr_access address misaligned") | Mint32, Op.Ascaled scale offset, r1::nil => if (check_address_parameter scale) && (check_address_parameter offset) then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4))))) |