From cab28a5331400fee1a0dd1c5fa7d0366fa888f5f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 27 Jul 2008 07:34:38 +0000 Subject: MAJ documentation git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@702 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Linear.v | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) (limited to 'backend/Linear.v') diff --git a/backend/Linear.v b/backend/Linear.v index ca1a2bc4..900b6a50 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -202,6 +202,40 @@ Definition parent_locset (stack: list stackframe) : locset := | Stackframe f sp ls c :: stack' => ls end. +(** The main difference between the Linear transition relation + and the LTL transition relation is the handling of function calls. + In LTL, arguments and results to calls are transmitted via + [vargs] and [vres] components of [Callstate] and [Returnstate], + respectively. The semantics takes care of transferring these values + between the locations of the caller and of the callee. + + In Linear and lower-level languages (Mach, PPC), arguments and + results are transmitted implicitly: the generated code for the + caller arranges for arguments to be left in conventional registers + and stack locations, as determined by the calling conventions, where + the function being called will find them. Similarly, conventional + registers will be used to pass the result value back to the caller. + This is reflected in the definition of [Callstate] and [Returnstate] + above, where a whole location state [rs] is passed instead of just + the values of arguments or returns as in LTL. + + These location states passed across calls are treated in a way that + reflects the callee-save/caller-save convention: +- The [exec_Lcall] transition from [State] to [Callstate] + saves the current location state [ls] in the call stack, + and passes it to the callee. +- The [exec_function_internal] transition from [Callstate] to [State] + changes the view of stack slots ([Outgoing] slots slide to + [Incoming] slots as per [call_regs]). +- The [exec_Lreturn] transition from [State] to [Returnstate] + restores the values of callee-save locations from + the location state of the caller, using [return_regs]. + +This protocol makes it much easier to later prove the correctness of +the [Stacking] pass, which inserts actual code that performs the +saving and restoring of callee-save registers described above. +*) + Inductive step: state -> trace -> state -> Prop := | exec_Lgetstack: forall s f sp sl r b rs m, -- cgit