aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Linear.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2016-10-01 17:25:18 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2016-10-01 17:25:18 +0200
commite637d041c5c2ee3a3ed395a7dab6c9101e8eb16c (patch)
tree518d558674d3e1c6ff41c46d84c784e727ed5d04 /backend/Linear.v
parentad2a2c862abef3aee701d1bca0524fcbf2d07b30 (diff)
downloadcompcert-kvx-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.tar.gz
compcert-kvx-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.zip
Support for 64-bit architectures: generic support
- Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
Diffstat (limited to 'backend/Linear.v')
-rw-r--r--backend/Linear.v19
1 files changed, 5 insertions, 14 deletions
diff --git a/backend/Linear.v b/backend/Linear.v
index da1b4c04..55f92d16 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -17,17 +17,8 @@
instructions with explicit labels and ``goto'' instructions. *)
Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Op.
-Require Import Locations.
-Require Import LTL.
-Require Import Conventions.
+Require Import AST Integers Values Memory Events Globalenvs Smallstep.
+Require Import Op Locations LTL Conventions.
(** * Abstract syntax *)
@@ -194,7 +185,7 @@ Inductive step: state -> trace -> state -> Prop :=
find_function ros rs' = Some f' ->
sig = funsig f' ->
Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
- step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m)
+ step (State s f (Vptr stk Ptrofs.zero) (Ltailcall sig ros :: b) rs m)
E0 (Callstate s f' rs' m')
| exec_Lbuiltin:
forall s f sp rs m ef args res b vargs t vres rs' m',
@@ -236,14 +227,14 @@ Inductive step: state -> trace -> state -> Prop :=
| exec_Lreturn:
forall s f stk b rs m m',
Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
- step (State s f (Vptr stk Int.zero) (Lreturn :: b) rs m)
+ step (State s f (Vptr stk Ptrofs.zero) (Lreturn :: b) rs m)
E0 (Returnstate s (return_regs (parent_locset s) rs) m')
| exec_function_internal:
forall s f rs m rs' m' stk,
Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
rs' = undef_regs destroyed_at_function_entry (call_regs rs) ->
step (Callstate s (Internal f) rs m)
- E0 (State s f (Vptr stk Int.zero) f.(fn_code) rs' m')
+ E0 (State s f (Vptr stk Ptrofs.zero) f.(fn_code) rs' m')
| exec_function_external:
forall s ef args res rs1 rs2 m t m',
args = map (fun p => Locmap.getpair p rs1) (loc_arguments (ef_sig ef)) ->