From e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:25:18 +0200 Subject: 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. --- backend/Linear.v | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) (limited to 'backend/Linear.v') 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)) -> -- cgit