diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-22 09:22:23 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-22 09:22:23 +0200 |
| commit | 31ea5a5740f59f4af490fa7b264023b4deb7ab25 (patch) | |
| tree | cfb915c5b0520d01becfd9342563fe7dbe24154e /aarch64/Asmblockgenproof.v | |
| parent | 5dec4b189dd7775229199de11e4c81551b7baaf6 (diff) | |
| download | compcert-kvx-31ea5a5740f59f4af490fa7b264023b4deb7ab25.tar.gz compcert-kvx-31ea5a5740f59f4af490fa7b264023b4deb7ab25.zip | |
fix linker model in Asmblock
Diffstat (limited to 'aarch64/Asmblockgenproof.v')
| -rw-r--r-- | aarch64/Asmblockgenproof.v | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index 0e90cbf5..41082772 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -27,19 +27,26 @@ Section PRESERVATION. Lemma next_progress: forall (f:MB.function) (pos:Z), (pos < (next f pos))%Z. Admitted. +Variable lk: aarch64_linker. Variable prog: Machblock.program. Variable tprog: Asmblock.program. Hypothesis TRANSF: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. + +Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), + Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs. + Lemma functions_bound_max_pos: forall fb f, Genv.find_funct_ptr ge fb = Some (Internal f) -> (max_pos next f) <= Ptrofs.max_unsigned. Admitted. + + Lemma transf_program_correct: - forward_simulation (PseudoAsmblock.semantics next prog) (AB.semantics tprog). + forward_simulation (PseudoAsmblock.semantics next prog) (AB.semantics lk tprog). Admitted. End PRESERVATION. |