text‹
C a function pointer type does not have to specify the names of the function parameters.
when translating a call to a function pointer from C into SIMPL we need a
way to pass the function parameters. Recall that in SIMPL local variables are represented
part of the state, there is no lambda binding at that stage. For ordinary function calls
know the names of the parameters and can refer to them, for function pointers we do not know
names. Our approach is to generally switch to uniform names for the parameters,
the position and the type like: ‹in1_int›, ‹in2_unsigned›.
mapping to the original names in the C file is implemented as syntactic sugar in the context.
this mapping depends on the actual function we have to make sure to work in the correct
. The main interface to this mapping is defined in 🍋‹../c-parser/HPInter.ML› e.g.:
that the current implementation is a little bit fragile as it also depends on the
translations for lookup and update in the underlying @{command statespace}. ›
subsubsection‹Correspondence proofs›
text‹
function pointer call boils down to an indirection. Instead of calling the function directly by
name we go via the function pointer and have to resolve the name from that pointer, e.g. by
environment mapping pointers to functions.
we come along a function pointer call in a correspondence proof we need a correspondence
for the function pointer. Were do we get it from? In full generality we do not know
about were the function pointer might be pointing to.
drastic way out could be to add a guard at the call point, which guarantees that
is such a proof. This makes the proof trivial, but the code gets polluted with
guards which also show up at the user level. So whenever one wants to proof
property about the resulting function one has to deal with this guard.
keep the user level proofs clean, we first decided to use assumptions on the function
environment (mapping function pointers to functions) and doing the correspondence proofs
those assumptions. The assumptions were managed in locales. While this 🪙‹open world› approach was appealing
of its modular and abstract take on function pointers it showed various shortcomings
practice:
▪ Performance of locales was bad due to a complex locale hierarchy with lots of assumptions
and lemmas.
▪ Complexity of the code managing the various use cases we supported:
▪ Constant function pointer as parameter to a function. Here constant means that the parameter is not
modified within the function body.
▪ Function pointer via constant global variable. Think of the global variable as a kind of dispatcher
or class table, e.g. Array of structs representing "object descriptions" with
function pointers as fields.
▪ C-style object method calls: Instead of a pure function pointer, a pointer to a structure
which containes function pointers is passed as a parameter.
that experience we decided to go a for a 🪙‹closed world› approach: The complete C-program
to be known a priory. The C-Parser and autocorres make this assumption in other places as well.
function pointers this means that at each function pointer call we can statically determine the
that might be called. So the function pointer call becomes a case distinction. This
complexity and the number of locales and we do not have to distinguish the various
-cases of function pointers for the correspondence proofs.
C-Parser tries to infer the relevant functions at each function pointer call. When it does
not succeed the user can manually add an attribute to the C code enumerating the potential callees.
› subsubsection‹Mutual recursion›
text‹
general approach to resolve a function pointer call is via a lookup in a program environment
maps the pointer to the definition of the function. In SIMPL the function is
by a piece of syntax, and the program environment is an explicit context @{term Γ} which
in the semantic rules for SIMPL. Moreover, for each function that might be called via
function pointer we introduce a pointer to that function. These pointers, and the assumption
all of them are distinct are put to the locale of global variables.
the final phase of Autocorres we introduce similar program environments @{term ‹P›}
map the pointers to monadic HOL functions definitions. The main use of those environments
put into equations of the form @{term "P some_function_pointer = some_function"}. These
collected in @{thm fun_ptr_simps}.
function pointer environments themselves are defined by means of @{const map_of_default}.
details on the construction of these environments comes below.
from phase L2 on the parameters
functions become lambda abstractions we introduce distinct program environment for each
type.
also support mutual recursion via function pointers (case 2 above), e.g. a function
call itself indirectly via a some function pointer variables. As all callees are statically
the global program analysis
this into account to determine the strongly connected components aka. (recursive) cliques.
›
subsection‹Global locale: ‹..._global_addresses››
text‹The global locale fixes a function pointer for each function and assumes distincness of
pointers. This locale is created during the initialisation phase of the C-Parser @{command install_C_file}
the individual functions are processed.
fundamental locale is storing the addresses of global variables, including function
and some basic properties about them. ›
context fnptr_global_addresses begin text‹
each function pointer a constant is declared
.g. @{const "fnptr.odd_disp"}, @{const "fnptr.add"}.
that these constants have to be qualified by the program name.
case there would be a conflict with Isabelle internal names, e.g. a function ending with ‹__›
name is suffixed with @{ML Hoare.proc_deco}, cf. @{ML NameGeneration.fun_ptr_name}. ›
ML ‹Hoare.proc_deco›
text‹
the global variables and their defining equations, i.e. initialisation expressions
collected in @{thm global_const_defs}.› thm global_const_defs thm global_const_array_selectors ― ‹more efficient access to array components› thm global_const_non_array_selectors thm global_const_selectors
text‹To express distinctness of function pointers we make use of the infrastructure 🍋‹$ISABELLE_HOME/src/HOL/Statespace/DistinctTreeProver.thy›, which is also the
for @{command statespace}. A tree data structure is used to efficiently derive
and subset properties. ›
thm fun_ptr_distinct thm fun_ptr_subtree
text‹For every function pointer the locale assumes that they are not NULL,
.e. @{const c_fnptr_guard}. Based on the distinctness of the function pointers
derive some simplification rules for @{const map_of_default}.› thm fun_ptr_guards thm fun_ptr_simps end
text‹Let us see the evolution of a function pointer call during the various autocorres phase. The
is function ‹call_binop›, which calls function pointers via a global dispatcher ‹dispatcher›.
C-Parser has inferred that via this array the actual potential callees are ‹add›, ‹mul› or ‹minus›.
set of potential function pointers is annotated in a SIMPL exception value:
{term "UndefinedFunction {fnptr.add, fnptr.mul, fnptr.minus}"} within the 'dynamic' function call:
{const dynCall_exn}. From this annotation autocorres derives the function pointer environments. › thm call_binop_body_def
text‹In phases L1, L2, IO, and HL the @{const map_of_default} is unfolded to a nested
{const L2_condition}.› thm l2_call_binop'_def thm hl_call_binop'_def
text‹In phase TS the nested conditions are folded into an @{const map_of_default} again.› thm ts.call_binop'_def
text‹Finally after all functions are processed by autocorres we pick the
{const map_of_default}s from all the functions, define the environments @{const P} and insert those
the final definitions of the functions.› thm call_binop'_def thm dispatcher.binop.P_def
text‹All the environements definitions are collected in @{thm P_defs} and all final functions in
{thm final_defs}› thmP_defs thm final_defs
text‹The environments are defined as qualified constants, with the base name @{const P} and the
indicating some kind of canonical access path. For example in function @{const call_binop'} the
is @{const dispatcher.binop.P}, where qualifier ‹dispatcher› comes from the global array
qualifier ‹binop› form the selected structure field. The general format of the qualifiers is:
🍋‹[function-name.]variable-name[.selector-name]*›
selectors are structure field selectors, intermediate array indices are omitted. The function-name
introduced function pointers selected via local function parameters or variables, or in case
access to a global variable has to be disambiguated. ›
text‹Note that all definitions of the functions as well as the environments are on theory level.
do not need any locale parameters or assumptions for the definitions.
, do derive the equations for accessing the function pointer environments we have to take
of the function pointers into account. This disjointness assumption is in
{locale fnptr_global_addresses}. › context fnptr_global_addresses begin
text‹Collection @{thm fun_ptr_simps} for positive equations for function pointers that are
in the environment.› thm fun_ptr_simps
text‹Collection @{thm fun_ptr_undefined_simps} for negative equations for function pointers that are
in the environment.› thm fun_ptr_undefined_simps
text‹These lemmas are derived from the more basic collections on @{const map_of_default}› thm fun_ptr_map_of_default_eqs thm fun_ptr_map_of_default_fallthrough_eqs
end
subsection‹Function / Recursive-clique specific locales›
subsubsection‹L1›
thm l1_def ―‹all relevant l1 definitions› thm ac_def ―‹definitions of all layers›
text‹Note that there are two variants of the definition of @{const l1_add'}. First the
definition and then an optimised version, already removing some
handling. Here are the names of the theorems:› thm l1_add'_def thm l1_opt_add'_def
context fnptr_global_addresses begin text‹const‹l1_call_binop'› makes a function pointer call via the const‹dispatcher› array selecting const‹binop_C›. So it might call const‹l1_add'›, const‹l1_minus'› or const‹l1_mul'›.
note that the function pointer call is wrapped in a const‹L1_guarded›. In
the guard ensures that the index into the array is in range. › thm l1_call_binop'_def thm global_const_defs thm l1_def
text‹The correspondence proofs are performed within the corres locale @{locale fnptr_global_addresses}.
results are
to @{thm l1_corres}. Note that the correspondence proofs of the potential callees are
. @{command autocorres} resolves call dependencies and
performs the correspondence proofs of the potential callees.› thm l1_call_binop'_corres thm l1_corres thm l1_def end
text‹This function performs a function pointer call on a function parameter. › thm l1_parameter_call'_def thm l1_def
context fnptr_global_addresses begin thm l1_parameter_call'_corres thm l1_corres end
context fnptr_global_addresses begin thm l2_call_binop'_corres thm l2_corres thm l2_def end
thm l2_parameter_call'_def thm l2_def
context fnptr_global_addresses begin
thm l2_parameter_call'_corres thm l2_corres thm l2_def end
text‹When defining (mutual) recursion indirectly via function pointers this is handled
any other (mutual) recursion.
the general flow of how to arrive at a new level with definition and correspondence proof.
▪ First the induction step of the correspondence proof is performed, assuming that the recursive
calls are in the correspondence relation.
▪ If that proof is successful the function body or bodies are used to do the actual definition(s) of the
function(s).
▪ After the definition is done the actual correspondence proof is performed using the induction step
as major ingredient, replacing the body / bodies with the new definition(s). ›
context fnptr_global_addresses begin thm fun_ptr_simps thm l2_corres thm l2_def thm l2_odd_disp'_def ―‹Foundational definition of @{command fixed_point}. FIXME: should we conceale this?› thm l2_odd_disp'.simps end
context fnptr_global_addresses begin thm fun_ptr_simps thm l2_corres thm l2_def thm l2_odd_disp'.simps (* thm l2_impl_odd_disp'_def *) \<comment>\<open>canonical variant. FIXME: should we rename this (simps?)?\<close> end
context fnptr_global_addresses begin thm wa_call_binop'_corres thm wa_corres thm wa_def end
thm wa_parameter_call'_def thm wa_def
context fnptr_global_addresses begin thm wa_parameter_call'_corres thm wa_corres thm wa_def end
subsubsection‹TS›
text‹const‹add'› is defined within the option monad. Note that (lifted version) also end
in the more expressive program environments (cf. @{thm fun_ptr_simps}). So function pointer
to this function can be performed in any of those monads.› thm add'_def thm fun_ptr_simps thm ts_def
thm fun_ptr_simps thm call_binop'_def thm ts_def
context fnptr_global_addresses begin thm call_binop'_corres thm ts_corres thm ts_def end
thm fun_ptr_simps thm fac'.simps thm ts_def
context fnptr_global_addresses begin thm fac'_corres thm ts_corres thm ts_def end
text‹Recall that in case of a function pointer call via a parameter we assume correspondence
the parameter. So in which monad should we end up? Which monad should we assume for the
? Currently we assume the same monad as for the function. We consecutively try the
from the most restrictive to the most expressive monad and we end up in the monad
the first successful proof. If you want a different (more expressive) monad you can
this via the autocorres option ‹ts_force›.›
thm parameter_call'_def thm wa_def
context fnptr_global_addresses begin thm parameter_call'_corres thm wa_corres thm wa_def end
thm ts_def
subsubsection‹Final AutoCorres›
text‹Once all phases are passed and the correspondence proofs between the consecutive layers are
they are combined to the final correspondence layer, from SIMPL upto TS. The program
@{const P} are defined and inserted into the functions.› context fnptr_global_addresses begin thm parameter_call'_ac_corres end
context fnptr_global_addresses begin thm call_binop'_ac_corres end
context fnptr_global_addresses begin thm odd_disp'_ac_corres thm even_disp'_ac_corres end
text‹When all functions of a C file are translated the following summary locales are introduced.›
context fnptr_global_addresses ―‹All implementation locales of phase TS› begin thm fun_ptr_simps thm even_disp'.simps (* thm impl_even_disp'_def *) (* fixme: naming? *) thm ac_def end
context fnptr_global_addresses ―‹All corres locales of all phases› begin thm l1_corres thm l2_corres thm hl_corres thm wa_corres thm ts_corres thm ac_corres thm final_defs thmP_defs
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
