From 31ea5a5740f59f4af490fa7b264023b4deb7ab25 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 22 Jun 2020 09:22:23 +0200 Subject: fix linker model in Asmblock --- aarch64/Asmblockgenproof.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'aarch64/Asmblockgenproof.v') 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. -- cgit