diff options
author | James Pollard <james@pollard.dev> | 2020-08-11 15:59:42 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-08-11 15:59:42 +0100 |
commit | bc9476199340bef845ea9c271d7a5ab0f0cdfcce (patch) | |
tree | 9a8d1822ee641aaae90f19e718085920ae5a94a1 /src/translation/HTLgen.v | |
parent | c64d5992e5c14d2dad7b528a37001ea7690d649e (diff) | |
download | vericert-bc9476199340bef845ea9c271d7a5ab0f0cdfcce.tar.gz vericert-bc9476199340bef845ea9c271d7a5ab0f0cdfcce.zip |
Remove alignment constraint during translation.
This is now inferred from the memory model.
Diffstat (limited to 'src/translation/HTLgen.v')
-rw-r--r-- | src/translation/HTLgen.v | 22 |
1 files changed, 10 insertions, 12 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 8245a06..87a6de6 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -300,37 +300,35 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : end. Definition check_address_parameter_signed (p : Z) : bool := - Z.eqb (Z.modulo p 4) 0 - && Z.leb Integers.Ptrofs.min_signed p + Z.leb Integers.Ptrofs.min_signed p && Z.leb p Integers.Ptrofs.max_signed. Definition check_address_parameter_unsigned (p : Z) : bool := - Z.eqb (Z.modulo p 4) 0 - && Z.leb p Integers.Ptrofs.max_unsigned. + Z.leb p Integers.Ptrofs.max_unsigned. 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 => if (check_address_parameter_signed off) then ret (boplitz Vadd r1 off) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address out of bounds") | Op.Ascaled scale offset, r1::nil => if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address out of bounds") | Op.Aindexed2 offset, r1::r2::nil => if (check_address_parameter_signed offset) then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset))) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds") | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds") | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in if (check_address_parameter_unsigned a) then ret (Vlit (ZToValue a)) - else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address misaligned") + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds") | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. @@ -418,19 +416,19 @@ Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) | Mint32, Op.Aindexed off, r1::nil => if (check_address_parameter_signed off) then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) - else error (Errors.msg "HTLgen: translate_arr_access address misaligned") + else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) then ret (Vvari stack (Vbinop Vdivu (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) (Vlit (ZToValue 4)))) - else error (Errors.msg "HTLgen: translate_arr_access address misaligned") + else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in if (check_address_parameter_unsigned a) then ret (Vvari stack (Vlit (ZToValue (a / 4)))) - else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") + else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset") | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") end. |