fix linker model in Asmblock

3 files changed, 31 insertions, 33 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index d52f3c24..93a81891 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -536,38 +536,18 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
   end.
 
-
-(** FIXME: not clear howto deal with these axioms in Asmblock.
-    The dependency over genv will get us in troubles...
-
-TODO: The solution is probably to put [symbol_low] and [symbol_high] [symbol_high_low]  with any dependency on "ge"
-as an hypothesis in RELSEM section.
-
-*)
-
-(** The two functions below axiomatize how the linker processes
-  symbolic references [symbol + offset].  It computes the
-  difference between the address and the PC, and splits it into:
-  - 12 low bits usable as an offset in an addressing mode;
-  - 21 high bits usable as argument to the ADRP instruction.
-
-  In CompCert's model, we cannot really describe PC-relative addressing,
-  but we can claim that the address of [symbol + offset] decomposes
-  as the sum of
-  - a low part, usable as an offset in an addressing mode;
-  - a high part, usable as argument to the ADRP instruction. *)
-
-Parameter symbol_low: genv -> ident -> ptrofs -> val.
-Parameter symbol_high: genv -> ident -> ptrofs -> val.
-
-Axiom symbol_high_low:
-  forall (ge: genv) (id: ident) (ofs: ptrofs),
-  Val.addl (symbol_high ge id ofs) (symbol_low ge id ofs) = Genv.symbol_address ge id ofs.
+(** See "Parameters" of the same names in Asm.v *) 
+Record aarch64_linker: Type := {
+  symbol_low: ident -> ptrofs -> val;
+  symbol_high: ident -> ptrofs -> val
+}.
 
 Section RELSEM.
 
+Variable lk: aarch64_linker.
 Variable ge: genv.
 
+
 (** The semantics is purely small-step and defined as a function
   from the current state (a register set + a memory state)
   to either [Next rs' m'] where [rs'] and [m'] are the updated register
@@ -777,7 +757,7 @@ Definition eval_addressing (a: addressing) (rs: regset): val :=
   | ADlsl base r n => Val.addl rs#base (Val.shll rs#r (Vint n))
   | ADsxt base r n => Val.addl rs#base (Val.shll (Val.longofint rs#r) (Vint n))
   | ADuxt base r n => Val.addl rs#base (Val.shll (Val.longofintu rs#r) (Vint n))
-  | ADadr base id ofs => Val.addl rs#base (symbol_low ge id ofs)
+  | ADadr base id ofs => Val.addl rs#base (symbol_low lk id ofs)
   | ADpostincr base n => Vundef (* not modeled yet *)
   end.
 
@@ -1600,5 +1580,5 @@ Inductive final_state: state -> int -> Prop :=
       rs#X0 = Vint r ->
       final_state (State rs m) r.
 
-Definition semantics (p: program) :=
-  Semantics step (initial_state p) final_state (Genv.globalenv p).
+Definition semantics (lk: aarch64_linker) (p: program) :=
+  Semantics (step lk) (initial_state p) final_state (Genv.globalenv p).
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.
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index b9f931c0..276e95d1 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -43,8 +43,17 @@ Hypothesis TRANSF: match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
+Definition lk :aarch64_linker := {| Asmblock.symbol_low:=Asm.symbol_low tge; Asmblock.symbol_high:=Asm.symbol_high tge|}.
+
+Lemma symbol_high_low: forall (id: ident) (ofs: ptrofs),
+  Val.addl (Asmblock.symbol_high lk id ofs) (Asmblock.symbol_low lk id ofs) = Genv.symbol_address ge id ofs.
+Proof.
+  unfold lk; simpl. intros; rewrite Asm.symbol_high_low.
+Admitted.
+
+
 Lemma transf_program_correct:
-  forward_simulation (Asmblock.semantics prog) (Asm.semantics tprog).
+  forward_simulation (Asmblock.semantics lk prog) (Asm.semantics tprog).
 Admitted. (* TODO *)
 
 End PRESERVATION.
@@ -108,8 +117,10 @@ Proof.
   + apply PseudoAsmblockproof.transf_program_correct; eauto.
     - intros; apply Asmblockgenproof.next_progress.
     - intros; eapply Asmblockgenproof.functions_bound_max_pos; eauto.
+      { intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. }
   + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
-    apply Asmblock_PRESERVATION.transf_program_correct. eauto.
+    { intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. }
+     apply Asmblock_PRESERVATION.transf_program_correct. eauto.
 Qed.
 
 End PRESERVATION.