diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 10:09:12 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 10:09:12 +0100 |
commit | 9491b9dda35897c8abde560b79a323d47aac0ec4 (patch) | |
tree | afe20a1f1e169c68e25a6a9c138b5898f6ce6693 /src/translation/HTLgen.v | |
parent | c5170915a81ca1bca420cd4683855cc7ba8ff8c4 (diff) | |
parent | e05b93c540d2e0e2cb9f4ab01460eba080b65401 (diff) | |
download | vericert-9491b9dda35897c8abde560b79a323d47aac0ec4.tar.gz vericert-9491b9dda35897c8abde560b79a323d47aac0ec4.zip |
Merge branch 'arrays-proof' into develop
Diffstat (limited to 'src/translation/HTLgen.v')
-rw-r--r-- | src/translation/HTLgen.v | 44 |
1 files changed, 27 insertions, 17 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 68f9900..43a6674 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -17,7 +17,7 @@ *) From compcert Require Import Maps. -From compcert Require Errors Globalenvs. +From compcert Require Errors Globalenvs Integers. From compcert Require Import AST RTL. From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad. @@ -245,19 +245,28 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") end. +Definition check_address_parameter (p : Z) : bool := + Z.eqb (Z.modulo p 4) 0 + && Z.leb Integers.Ptrofs.min_signed p + && Z.leb p Integers.Ptrofs.min_signed. + Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := - match a, args with + 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.Aindexed2 off, r1::r2::nil => ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 off)) | Op.Ascaled scale offset, r1::nil => - ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) - | Op.Aindexed2scaled scale offset, r1::r2::nil => - ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - (* Stack arrays/referenced variables *) + if (check_address_parameter scale) && (check_address_parameter offset) + then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter scale) && (check_address_parameter offset) + then ret (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) - ret (Vlit (ZToValue 32 a)) - | _, _ => error (Errors.msg "Htlgen: eff_addressing instruction not implemented: other") + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter a) + then ret (Vlit (ZToValue 32 a)) + else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") end. (** Translate an instruction to a statement. FIX mulhs mulhu *) @@ -340,23 +349,24 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := 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 => (* FIXME: Cannot guarantee alignment *) + | Mint32, Op.Aindexed off, r1::nil => ret (Vvari stack (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (off / 4))))) | Mint32, Op.Ascaled scale offset, r1::nil => - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + 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))))) else error (Errors.msg "Htlgen: translate_arr_access address misaligned") | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) + if (check_address_parameter scale) && (check_address_parameter offset) then ret (Vvari stack (Vbinop Vadd (Vbinop Vadd (boplitz Vdiv r1 4) (Vlit (ZToValue 32 (offset / 4)))) (boplitz Vmul r2 (scale / 4)))) else error (Errors.msg "Htlgen: translate_arr_access address misaligned") | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) - if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) - else error (Errors.msg "Htlgen: eff_addressing misaligned stack offset") - | _, _, _ => error (Errors.msg "Htlgen: translate_arr_access unsuported addressing") + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter a) + then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) + else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset") + | _, _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing") end. Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := |