diff options
| -rw-r--r-- | aarch64/Asmgen.v | 7 | ||||
| -rw-r--r-- | aarch64/Asmgenproof1.v | 2 | ||||
| -rw-r--r-- | aarch64/extractionMachdep.v | 1 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 5 |
4 files changed, 13 insertions, 2 deletions
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 1c0e41a1..875f3fd1 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -20,6 +20,11 @@ Local Open Scope string_scope. Local Open Scope list_scope. Local Open Scope error_monad_scope. +(** Alignment check for symbols *) + +Parameter symbol_is_aligned : ident -> Z -> bool. +(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) + (** Extracting integer or float registers. *) Definition ireg_of (r: mreg) : res ireg := @@ -942,7 +947,7 @@ Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg) (insn (ADimm X16 Int64.zero) :: k)) | Aglobal id ofs, nil => assertion (negb (Archi.pic_code tt)); - if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero + if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k) else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k)) | Ainstack ofs, nil => diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v index 663ee50b..6d44bcc8 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmgenproof1.v @@ -1592,7 +1592,7 @@ Proof. simpl; rewrite Int64.add_zero; auto. intros. apply C; eauto with asmgen. - (* Aglobal *) - destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero); inv TR. + destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR. + econstructor; econstructor; split. apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. auto. split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence. diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v index a447d12f..e82056e2 100644 --- a/aarch64/extractionMachdep.v +++ b/aarch64/extractionMachdep.v @@ -21,3 +21,4 @@ Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *) (* Asm *) Extract Constant Asm.symbol_low => "fun _ _ _ -> assert false". Extract Constant Asm.symbol_high => "fun _ _ _ -> assert false". +Extract Constant Asmgen.symbol_is_aligned => "C2C.atom_is_aligned". diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c1dfa9f4..9ae7bbd9 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -61,6 +61,11 @@ let atom_alignof a = with Not_found -> None +let atom_is_aligned a sz = + match atom_alignof a with + | None -> false + | Some align -> align mod (Z.to_int sz) = 0 + let atom_sections a = try (Hashtbl.find decl_atom a).a_sections |