diff options
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 42 |
1 files changed, 28 insertions, 14 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 66170bc..dc82fb1 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -283,15 +283,22 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr : 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. + && Z.leb p Integers.Ptrofs.max_signed. 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))) else error (Errors.msg "Veriloggen: translate_eff_addressing address misaligned") + | Op.Aindexed2 offset, r1::r2::nil => + if (check_address_parameter offset) + then ret (Vbinop Vadd (Vvar r1) (boplitz Vadd r2 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)) @@ -385,23 +392,26 @@ 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 Vdiv (boplitz Vadd r1 off) (Vlit (ZToValue 32 4)))) + else error (Errors.msg "HTLgen: 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))))) - else error (Errors.msg "Htlgen: translate_arr_access address misaligned") + then ret (Vvari stack (Vbinop Vdiv (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue 32 offset))) (Vlit (ZToValue 32 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 (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") + (Vbinop Vdiv + (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + (ZToValue 32 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 + let a := Integers.Ptrofs.signed 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") + else error (Errors.msg "HTLgen: eff_addressing misaligned stack offset") + | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") end. Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := @@ -499,8 +509,11 @@ Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := (st_controllogic s)) (create_arr_state_incr s sz ln i). +Definition stack_correct (sz : Z) : bool := + (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0). + Definition transf_module (f: function) : mon module := - if (Z.eq_dec (Z.modulo f.(fn_stacksize) 4) 0) then + if stack_correct f.(fn_stacksize) 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)); @@ -559,7 +572,8 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program := (fun i v => Errors.OK v) p. *) -Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := +Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := true. +(* let ge := Globalenvs.Genv.globalenv p in match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with | Some b => @@ -568,7 +582,7 @@ Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := | _ => false end | _ => false - end. + end. *) Definition transl_program (p : RTL.program) : Errors.res HTL.program := if main_is_internal p |