fix linker model in Asmblock

1 files changed, 10 insertions, 30 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).