diff --git a/thys/Isabelle_C/C11-FrontEnd/C_Appendices.thy b/thys/Isabelle_C/C11-FrontEnd/C_Appendices.thy --- a/thys/Isabelle_C/C11-FrontEnd/C_Appendices.thy +++ b/thys/Isabelle_C/C11-FrontEnd/C_Appendices.thy @@ -1,842 +1,842 @@ (****************************************************************************** * Isabelle/C * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) chapter \Annexes\ theory C_Appendices imports "examples/C1" - "Isar_Ref.Base" + Isar_Ref.Base begin (*<*) ML \ \\<^file>\~~/src/Doc/antiquote_setup.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Doc/antiquote_setup.ML Author: Makarius Auxiliary antiquotations for the Isabelle manuals. *) \ structure C_Antiquote_Setup = struct (* misc utils *) fun translate f = Symbol.explode #> map f #> implode; val clean_string = translate (fn "_" => "\\_" | "#" => "\\#" | "$" => "\\$" | "%" => "\\%" | "<" => "$<$" | ">" => "$>$" | "{" => "\\{" | "|" => "$\\mid$" | "}" => "\\}" | "\" => "-" | c => c); fun clean_name "\" = "dots" | clean_name ".." = "ddot" | clean_name "." = "dot" | clean_name "_" = "underscore" | clean_name "{" = "braceleft" | clean_name "}" = "braceright" | clean_name s = s |> translate (fn "_" => "-" | "\" => "-" | "#" => "symbol-hash" | "\" => "symbol-lower-approx" | "\" => "symbol-upper-down" | c => c); (* Isabelle/Isar entities (with index) *) local val arg = enclose "{" "}" o clean_string; fun entity check markup binding index = Thy_Output.antiquotation_raw (binding |> Binding.map_name (fn name => name ^ (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name)) (fn ctxt => fn (logic, (name, pos)) => let val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding); val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; val hyper = enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; val idx = (case index of NONE => "" | SOME is_def => "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); val _ = if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else (); val latex = idx ^ (Output.output name |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |> hyper o enclose "\\mbox{\\isa{" "}}"); in Latex.string latex end); fun entity_antiqs check markup kind = entity check markup kind NONE #> entity check markup kind (SOME true) #> entity check markup kind (SOME false); in val _ = Theory.setup (entity_antiqs C_Annotation.check_command "isacommand" \<^binding>\annotation\); end; end; \ (*>*) section \Syntax Commands for Isabelle/C\ subsection \Outer Classical Commands\ text \ \begin{matharray}{rcl} @{command_def "C_file"} & : & \local_theory \ local_theory\ \\ @{command_def "C"} & : & \local_theory \ local_theory\ \\ @{command_def "C_export_boot"} & : & \local_theory \ local_theory\ \\ @{command_def "C_prf"} & : & \proof \ proof\ \\ @{command_def "C_val"} & : & \any \\ \\ @{command_def "C_export_file"} & : & \any \\ \\ \end{matharray} \begin{tabular}{rcll} @{attribute_def C_lexer_trace} & : & \attribute\ & default \false\ \\ @{attribute_def C_parser_trace} & : & \attribute\ & default \false\ \\ @{attribute_def C_ML_verbose} & : & \attribute\ & default \true\ \\ @{attribute_def C_starting_env} & : & \attribute\ & default \empty\ \\ @{attribute_def C_starting_rule} & : & \attribute\ & default \translation_unit\ \\ \end{tabular} \<^rail>\ @@{command C_file} @{syntax name} ';'? ; (@@{command C} | @@{command C_export_boot} | @@{command C_prf} | @@{command C_val}) @{syntax text} ; @@{command C_export_file} ; \ \<^descr> \<^theory_text>\C_file name\ reads the given C file, and let any attached semantic back-ends to proceed for further subsequent evaluation. Top-level C bindings are stored within the (global or local) theory context; the initial environment is set by default to be an empty one, or the one returned by a previous \<^theory_text>\C_file\ (depending on @{attribute_def C_starting_env}). The entry-point of the grammar taken as initial starting parser is read from @{attribute_def C_starting_rule} (see \<^url>\https://www.haskell.org/happy/doc/html/sec-directives.html#sec-parser-name\). Multiple \<^theory_text>\C_file\ commands may be used to build larger C projects if they are all written in a single theory file (existing parent theories are ignored, and not affecting the current working theory). \<^descr> \<^theory_text>\C\ is similar to \<^theory_text>\C_file\, but evaluates directly the given \text\. Top-level resulting bindings are stored within the (global or local) theory context. \<^descr> \<^theory_text>\C_export_boot\ is similar to \<^theory_text>\ML_export\, except that the code in input is understood as being processed by \<^theory_text>\C\ instead of \<^theory_text>\ML\. \<^descr> \<^theory_text>\C_prf\ is similar to \<^theory_text>\ML_prf\, except that the code in input is understood as being processed by \<^theory_text>\C\ instead of \<^theory_text>\ML\. \<^descr> \<^theory_text>\C_val\ is similar to \<^theory_text>\ML_val\, except that the code in input is understood as being processed by \<^theory_text>\C\ instead of \<^theory_text>\ML\. \<^descr> \<^theory_text>\C_export_file\ is similar to \<^theory_text>\generate_file fic = \code\ export_generated_files fic\, except that \<^item> \code\ refers to the dump of all existing previous C code in the current theory (parent theories are ignored), \<^item> and any ML antiquotations in \code\ are not analyzed by \<^theory_text>\generate_file\ (in contrast with its default behavior). \ text \ \<^descr> @{attribute C_lexer_trace} indicates whether the list of C tokens associated to the source text should be output (that list is computed during the lexing phase). \<^descr> @{attribute C_parser_trace} indicates whether the stack forest of Shift-Reduce node should be output (it is the final stack which is printed, i.e., the one taken as soon as the parsing terminates). \<^descr> @{attribute C_ML_verbose} indicates whether nested \<^theory_text>\ML\ commands are acting similarly as their default verbose configuration in top-level. \<^descr> @{attribute C_starting_env} makes the start of a C command (e.g., \<^theory_text>\C_file\, \<^theory_text>\C\) initialized with the environment of the previous C command if existing. \<^descr> @{attribute C_starting_rule} sets which parsing function will be used to parse the next C commands (e.g., \<^theory_text>\C_file\, \<^theory_text>\C\). \ subsection \Inner Annotation Commands\ text \ \<^rail>\ (@@{annotation "#ML_file"} | @@{annotation ML_file} | @@{annotation "ML_file\"} | @@{annotation "#C_file"} | @@{annotation C_file} | @@{annotation "C_file\"}) @{syntax name} ';'? ; (@@{annotation "#ML"} | @@{annotation ML} | @@{annotation "ML\"} | @@{annotation "#setup"} | @@{annotation setup} | @@{annotation "setup\"} | @@{annotation "\setup"} | @@{annotation "\setup\"} | @@{annotation "#C"} | @@{annotation C} | @@{annotation "C\"} | @@{annotation "#C_export_boot"} | @@{annotation C_export_boot} | @@{annotation "C_export_boot\"}) @{syntax text} ; (@@{annotation "#C_export_file"} | @@{annotation C_export_file} | @@{annotation "C_export_file\"} | @@{annotation highlight} | @@{annotation "highlight\"}) ; \ \<^descr> \<^C_theory_text>\ML_file\, \<^C_theory_text>\C_file\, \<^C_theory_text>\ML\, \<^C_theory_text>\setup\, \<^C_theory_text>\C\, \<^C_theory_text>\C_export_boot\, and \<^C_theory_text>\C_export_file\ behave similarly as the respective outer commands \<^theory_text>\ML_file\, \<^theory_text>\C_file\, \<^theory_text>\ML\, \<^theory_text>\setup\, \<^theory_text>\C\, \<^theory_text>\C_export_boot\, \<^theory_text>\C_export_file\. \<^descr> \<^C_theory_text>\\setup \f'\\ has the same semantics as \<^C_theory_text>\setup \f\\ whenever \<^term>\\ stack top env. f' stack top env = f\. In particular, depending on where the annotation \<^C_theory_text>\\setup \f'\\ is located in the C code, the additional values \stack\, \top\ and \env\ can drastically vary, and then can be possibly used in the body of \f'\ for implementing new interactive features (e.g., in contrast to \f\, which by default does not have the possibility to directly use the information provided by \stack\, \top\ and \env\). \<^descr> \<^C_theory_text>\highlight\ changes the background color of the C tokens pointed by the command. \<^descr> \<^C_theory_text>\#ML_file\, \<^C_theory_text>\#C_file\, \<^C_theory_text>\#ML\, \<^C_theory_text>\#setup\, \<^C_theory_text>\#C\, \<^C_theory_text>\#C_export_boot\, and \<^C_theory_text>\#C_export_file\ behave similarly as the respective (above inner) commands \<^C_theory_text>\ML_file\, \<^C_theory_text>\C_file\, \<^C_theory_text>\ML\, \<^C_theory_text>\setup\, \<^C_theory_text>\C\, \<^C_theory_text>\C_export_boot\, and \<^C_theory_text>\C_export_file\ except that their evaluations happen as earliest as possible. \<^descr> \<^C_theory_text>\ML_file\\, \<^C_theory_text>\C_file\\, \<^C_theory_text>\ML\\, \<^C_theory_text>\setup\\, \<^C_theory_text>\\setup\\, \<^C_theory_text>\C\\, \<^C_theory_text>\C_export_boot\\, \<^C_theory_text>\C_export_file\\, and \<^C_theory_text>\highlight\\ behave similarly as the respective (above inner) commands \<^C_theory_text>\ML_file\, \<^C_theory_text>\C_file\, \<^C_theory_text>\ML\, \<^C_theory_text>\setup\, \<^C_theory_text>\\setup\, \<^C_theory_text>\C\, \<^C_theory_text>\C_export_boot\, \<^C_theory_text>\C_export_file\, and \<^C_theory_text>\highlight\ except that their evaluations happen as latest as possible. \ subsection \Inner Directive Commands\ text \ \<^descr> Among the directives provided as predefined in Isabelle/C, we currently have: \<^C>\#define _\ and \<^C>\#undef _\. In particular, for the case of \<^C>\#define _\, rewrites are restricted to variable-form macros: support of functional macros is not yet provided. \<^descr> In Isabelle/C, not-yet-defined directives (such as \<^C>\#include _\ or \<^C>\#if #endif\, etc.) do not make the parsing fail, but are treated as ``free variable commands''. \ section \Quick Start (for People More Familiar with C than Isabelle)\ text \ \<^item> Assuming we are working with Isabelle 2019 \<^url>\http://isabelle.in.tum.de/dist/Isabelle2019_app.tar.gz\, the shortest way to start programming in C is to open a new theory file with the shell-command: \<^verbatim>\$ISABELLE_HOME/bin/isabelle jedit -d $AFP_HOME/thys Scratch.thy\ where \<^verbatim>\$ISABELLE_HOME\ is the path of the above extracted Isabelle source, and \<^verbatim>\$AFP_HOME\ is the downloaded content of \<^url>\https://bitbucket.org/isa-afp/afp-2019\.\<^footnote>\This folder particularly contains the Isabelle/C project, located in \<^url>\https://bitbucket.org/isa-afp/afp-2019/src/default/thys/Isabelle_C\. To inspect the latest developper version, one can also replace \<^verbatim>\$AFP_HOME/thys\ by the content downloaded from \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c\.\ \<^item> The next step is to copy this minimal content inside the newly opened window: \<^verbatim>\theory Scratch imports Isabelle_C.C_Main begin C \ // C code \ end\ \<^item> \<^emph>\Quod Erat Demonstrandum!\ This already enables the support of C code inside the special brackets ``\<^verbatim>\\\\'', now depicted as ``\\\\'' for readability reasons. \ text_raw \ \begin{figure} \centering \includegraphics[width=\textwidth]{figures/C-export-example} \caption{Making the File Browser Pointing to the Virtual File System} \label{fig:file-bro} \end{figure} \ text \ Additionally, Isabelle/C comes with several functionalities that can be alternatively explored: \<^item> To write theorems and proofs along with C code, the special C comment \<^C>\/*@ (* Isabelle content *) */\ can be used at any position where C comments are usually regularly allowed. At the time of writing, not yet all Isabelle commands can be written in C comments, and certain proof-solving-command combinations are also not yet implemented --- manual registration of commands to retrieve some more or less native user-experience remains possible though. Generally, the kind of content one can write in C comments should be arbitrary. The exhaustive list of Isabelle commands is provided in the accompanying above archive, for example in \<^dir>\$ISABELLE_HOME/src/Doc/Isar_Ref\ or \<^url>\https://isabelle.in.tum.de/doc/isar-ref.pdf\. \<^item> Instead of starting from scratch, any existing C files can also be opened with Isabelle/C, it suffices to replace: \begin{tabular}{c} \<^verbatim>\C\ \<^theory_text>\\ /* C */ \\ \\ by \\ \<^verbatim>\C_file\ \<^theory_text>\\~/file.c\\ \end{tabular} Once done, one can press a CTRL-like key while hovering the mouse over the file name, then followed by a click on it to open a new window loading that file. \<^item> After a \<^verbatim>\C\ \<^theory_text>\\ /* C */ \\ command, one has either the possibility to keep the content as such in the theory file, or use \<^verbatim>\C_export_file\ to export all previous C content into a ``real'' C file. -Note that since Isabelle2019, Isabelle uses a virtual file-system. This has the consequence, that +Note that since Isabelle2019, Isabelle/C uses a virtual file-system. This has the consequence, that some extra operations are needed to export a file generated into the virtual file-system of Isabelle into the ``real'' file-system. First, the \<^verbatim>\C_export_file\ command needs to be activated, by putting the cursor on the command. This leads to the following message in the output window: \<^verbatim>\See theory exports "C/*/*.c"\ (see \autoref{fig:file-bro}). By clicking on \theory exports\ in this message, Isabelle opens a \File Browser\ showing the content of the virtual file-system in the left window. Selecting and opening a generated file in the latter lets jEdit display it in a new buffer, which gives the possibility to export this file via ``\File \ Save As\\'' into the real file-system. \ section \Case Study: Mapping on the Parsed AST\ text \ In this section, we give a concrete example of a situation where one is interested to do some automated transformations on the parsed AST, such as changing the type of every encountered variables from \<^C>\int _;\ to \<^C>\int _ [];\. The main theory of interest here is \<^theory>\Isabelle_C.C_Parser_Language\, where the C grammar is loaded, in contrast to \<^theory>\Isabelle_C.C_Lexer_Language\ which is only dedicated to build a list of C tokens. As another example, \<^theory>\Isabelle_C.C_Parser_Language\ also contains the portion of the code implementing the report to the user of various characteristics of encountered variables during parsing: if a variable is bound or free, or if the declaration of a variable is made in the global topmost space or locally declared in a function. \ subsection \Prerequisites\ text \ Even if \<^file>\generated/c_grammar_fun.grm.sig\ and \<^file>\generated/c_grammar_fun.grm.sml\ are files written in ML syntax, we have actually modified \<^dir>\../src_ext/mlton/lib/mlyacc-lib\ in such a way that at run time, the overall loading and execution of \<^theory>\Isabelle_C.C_Parser_Language\ will mimic all necessary features of the Haskell parser generator Happy \<^footnote>\\<^url>\https://www.haskell.org/happy/doc/html/index.html\\, including any monadic interactions between the lexing (\<^theory>\Isabelle_C.C_Lexer_Language\) and parsing part (\<^theory>\Isabelle_C.C_Parser_Language\). This is why in the remaining part, we will at least assume a mandatory familiarity with Happy (e.g., the reading of ML-Yacc's manual can happen later if wished \<^footnote>\\<^url>\https://www.cs.princeton.edu/~appel/modern/ml/ml-yacc/manual.html\\). In particular, we will use the term \<^emph>\rule code\ to designate \<^emph>\a Haskell expression enclosed in braces\ \<^footnote>\\<^url>\https://www.haskell.org/happy/doc/html/sec-grammar.html\\. \ subsection \Structure of \<^theory>\Isabelle_C.C_Parser_Language\\ text \ In more detail, \<^theory>\Isabelle_C.C_Parser_Language\ can be seen as being principally divided into two parts: \<^item> a first part containing the implementation of \<^ML_structure>\C_Grammar_Rule_Lib\, which provides the ML implementation library used by any rule code written in the C grammar \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ (\<^file>\generated/c_grammar_fun.grm.sml\). \<^item> a second part implementing \<^ML_structure>\C_Grammar_Rule_Wrap\, providing one wrapping function for each rule code, for potentially complementing the rule code with an additional action to be executed after its call. The use of wrapping functions is very optional: by default, they are all assigned as identity functions. The difference between \<^ML_structure>\C_Grammar_Rule_Lib\ and \<^ML_structure>\C_Grammar_Rule_Wrap\ relies in how often functions in the two structures are called: while building subtree pieces of the final AST, grammar rules are free to call any functions in \<^ML_structure>\C_Grammar_Rule_Lib\ for completing their respective tasks, but also free to not use \<^ML_structure>\C_Grammar_Rule_Lib\ at all. On the other hand, irrespective of the actions done by a rule code, the function associated to the rule code in \<^ML_structure>\C_Grammar_Rule_Wrap\ is retrieved and always executed (but a visible side-effect will likely mostly happen whenever one has provided an implementation far different from \<^ML>\I\). \ text \ Because the grammar \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ (\<^file>\generated/c_grammar_fun.grm.sml\) has been defined in such a way that computation of variable scopes are completely handled by functions in \<^ML_structure>\C_Grammar_Rule_Lib\ and not in rule code (which are just calling functions in \<^ML_structure>\C_Grammar_Rule_Lib\), it is enough to overload functions in \<^ML_structure>\C_Grammar_Rule_Lib\ whenever it is wished to perform new actions depending on variable scopes, for example to do a specific PIDE report at the first time when a C variable is being declared. In particular, functions in \<^ML_structure>\C_Grammar_Rule_Lib\ are implemented in monadic style, making a subsequent modification on the parsing environment \<^theory>\Isabelle_C.C_Environment\ possible (whenever appropriate) as this last is carried in the monadic state. Fundamentally, this is feasible because the monadic environment fulfills the property of being always properly enriched with declared variable information at any time, because we assume \<^item> working with a language where a used variable must be at most declared or redeclared somewhere before its actual usage, \<^item> and using a parser scanning tokens uniquely, from left to right, in the same order as the execution of rule code actions. \ subsubsection \Example\ text \ As illustration, \<^ML>\C_Grammar_Rule_Lib.markup_var o C_Ast.Left\ is (implicitly) called by a rule code while a variable being declared is encountered. Later, a call to \<^ML>\C_Grammar_Rule_Lib.markup_var o C_Ast.Right\ in \<^ML_structure>\C_Grammar_Rule_Wrap\ (actually, in \<^ML_structure>\C_Grammar_Rule_Wrap_Overloading\) is made after the execution of another rule code to signal the position of a variable in use, together with the information retrieved from the environment of the position of where it is declared. \ text \ In more detail, the second argument of \<^ML>\C_Grammar_Rule_Lib.markup_var\ is among other of the form: \<^ML_type>\Position.T * {global: bool}\, where particularly the field \<^ML>\#global : C_Env.markup_ident -> bool\ of the record is informing \<^ML>\C_Grammar_Rule_Lib.markup_var\ if the variable being reported (at either first declaration time, or first use time) is global or local (inside a function for instance). Because once declared, the property \<^ML>\#global : C_Env.markup_ident -> bool\ of a variable does not change afterwards, it is enough to store that information in the monadic environment: \<^item> \<^bold>\Storing the information at declaration time\ The part deciding if a variable being declared is global or not is implemented in \<^ML>\C_Grammar_Rule_Lib.doDeclIdent\ and \<^ML>\C_Grammar_Rule_Lib.doFuncParamDeclIdent\. The two functions come from \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ (so do any functions in \<^ML_structure>\C_Grammar_Rule_Lib\). Ultimately, they are both calling \<^ML>\C_Grammar_Rule_Lib.markup_var o C_Ast.Left\ at some point. \<^item> \<^bold>\Retrieving the information at use time\ \<^ML>\C_Grammar_Rule_Lib.markup_var o C_Ast.Right\ is only called by \<^ML>\C_Grammar_Rule_Wrap.primary_expression1\, while treating a variable being already declared. In particular the second argument of \<^ML>\C_Grammar_Rule_Lib.markup_var\ is just provided by what has been computed by the above point when the variable was declared (e.g., the globality versus locality information). \ subsection \Rewriting of AST node\ text \ For the case of rewriting a specific AST node, from subtree \T1\ to subtree \T2\, it is useful to zoom on the different parsing evaluation stages, as well as make precise when the evaluation of semantic back-ends are starting. \<^enum> Whereas annotations in Isabelle/C code have the potential of carrying arbitrary ML code (as in \<^theory>\Isabelle_C.C1\), the moment when they are effectively evaluated will not be discussed here, because to closely follow the semantics of the language in embedding (so C), we suppose comments --- comprising annotations --- may not affect any parsed tokens living outside comments. So no matter when annotations are scheduled to be future evaluated in Isabelle/C, the design decision of Isabelle/C is to not let a code do directive-like side-effects in annotations, such as changing \T1\ to \T2\ inside annotations. \<^enum> To our knowledge, the sole category of code having the capacity to affect incoming stream of tokens are directives, which are processed and evaluated before the ``major'' parsing step occurs. Since in Isabelle/C, directives are relying on ML code, changing an AST node from \T1\ to \T2\ can then be perfectly implemented in directives. \<^enum> After the directive (pre)processing step, the main parsing happens. But since what are driving the parsing engine are principally rule code, this step means to execute \<^ML_structure>\C_Grammar_Rule_Lib\ and \<^ML_structure>\C_Grammar_Rule_Wrap\, i.e., rules in \<^file>\generated/c_grammar_fun.grm.sml\. \<^enum> Once the parsing finishes, we have a final AST value, which topmost root type entry-point constitutes the last node built before the grammar parser \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ ever entered in a stop state. For the case of a stop acceptance state, that moment happens when we reach the first rule code building the type \<^ML_type>\C_Ast.CTranslUnit\, since there is only one possible node making the parsing stop, according to what is currently written in the C grammar. (For the case of a state stopped due to an error, it is the last successfully built value that is returned, but to simplify the discussion, we will assume in the rest of the document the parser is taking in input a fully well-parsed C code.) \<^enum> By \<^emph>\semantic back-ends\, we denote any kind of ``relatively efficient'' compiled code generating Isabelle/HOL theorems, proofs, definitions, and so with the potential of generally generating Isabelle packages. In our case, the input of semantic back-ends will be the type \<^ML_type>\C_Ast.CTranslUnit\ (actually, whatever value provided by the above parser). But since our parser is written in monadic style, it is as well possible to give slightly more information to semantic back-ends, such as the last monadic computed state, so including the last state of the parsing environment. \ text \ Generally, semantic back-ends can be written in full ML starting from \<^ML_type>\C_Ast.CTranslUnit\, but to additionally support formalizing tasks requiring to start from an AST defined in Isabelle/HOL, we provide an equivalent AST in HOL in the project, such as the one obtained after loading \<^url>\https://gitlri.lri.fr/ftuong/citadelle-devel/blob/master/doc/Meta_C_generated.thy\. (In fact, the ML AST is just generated from the HOL one.) \ text \ Based on the above information, there are now several \<^emph>\equivalent\ ways to proceed for the purpose of having an AST node be mapped from \T1\ to \T2\. The next bullets providing several possible solutions to follow are particularly sorted in increasing action time. \<^item> \<^emph>\Before even starting the Isabelle system.\ A first approach would be to modify the C code in input, by adding a directive \<^C>\#define _ _\ performing the necessary rewrite. \<^item> \<^emph>\Before even starting the Isabelle system.\ As an alternative of changing the C code, one can modify \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ by hand, by explicitly writing \T2\ at the specific position of the rule code generating \T1\. However, this solution implies to re-generate \<^file>\generated/c_grammar_fun.grm.sml\. \<^item> \<^emph>\At grammar loading time, while the source of Isabelle/C is still being processed.\ Instead of modifying the grammar, it should be possible to first locate which rule code is building \T1\. Then it would remain to retrieve and modify the respective function of \<^ML_structure>\C_Grammar_Rule_Wrap\ executed after that rule code, by providing a replacement function to be put in \<^ML_structure>\C_Grammar_Rule_Wrap_Overloading\. However, as a design decision, wrapping functions generated in \<^file>\generated/c_grammar_fun.grm.sml\ have only been generated to affect monadic states, not AST values. This is to prevent an erroneous replacement of an end-user while parsing C code. (It is currently left open about whether this feature will be implemented in future versions of the parser...) \<^item> \<^emph>\At directive setup time, before executing any \<^theory_text>\C\ command of interest.\ Since the behavior of directives can be dynamically modified, this solution amounts to change the semantics of any wished directive, appearing enough earlier in the code. (But for the overall code be in the end mostly compatible with any other C preprocessors, the implementation change has to be somehow at least consistent with how a preprocessor is already expected to treat an initial C un(pre)processed code.) For example, the current semantics of \<^C>\#undef _\ depends on what has been registered in \<^ML>\C_Context.directive_update\ (see \<^theory>\Isabelle_C.C_Command\). \<^item> \<^emph>\After parsing and obtaining a constructive value.\ Another solution consists in directly writing a mapping function acting on the full AST, so writing a ML function of type \<^ML_type>\C_Ast.CTranslUnit -> C_Ast.CTranslUnit\ (or a respective HOL function) which has to act on every constructor of the AST (so in the worst case about hundred of constructors for the considered AST, i.e., whenever a node has to be not identically returned). However, as we have already implemented a conversion function from \<^ML_type>\C_Ast.CTranslUnit\ (subset of C11) to a subset AST of C99, it might be useful to save some effort by starting from this conversion function, locate where \T1\ is pattern-matched by the conversion function, and generate \T2\ instead. As example, the conversion function \<^ML>\C_Ast.main\ is particularly used to connect the C11 front-end to the entry-point of AutoCorres in \<^verbatim>\l4v/src/tools/c-parser/StrictCParser.ML\. \<^item> \<^emph>\At semantic back-ends execution time.\ The above points were dealing with the cases where modification actions were all occurring before getting a final \<^ML_type>\C_Ast.CTranslUnit\ value. But this does not mean it is forbidden to make some slight adjustments once that resulting \<^ML_type>\C_Ast.CTranslUnit\ value obtained. In particular, it is the tasks of semantic back-ends to precisely work with \<^ML_type>\C_Ast.CTranslUnit\ as starting point, and possibly translate it to another different type. So letting a semantic back-end implement the mapping from \T1\ to \T2\ would mean here to first understand the back-end of interest's architecture, to see where the necessary minimal modifications must be made. By taking l4v as a back-end example, its integration with Isabelle/C first starts with translating \<^ML_type>\C_Ast.CTranslUnit\ to l4v's default C99 AST. Then various analyses on the obtained AST are performed in \<^url>\https://github.com/seL4/l4v/tree/master/tools/c-parser\ (the reader interested in the details can start by further exploring the ML files loaded by \<^url>\https://github.com/seL4/l4v/blob/master/tools/c-parser/CTranslation.thy\). In short, to implement the mapping from \T1\ to \T2\ in the back-end part, one can either: \<^item> modify the translation from \<^ML_type>\C_Ast.CTranslUnit\ to C99, \<^item> or modify the necessary ML files of interests in the l4v project. \ text \ More generally, to better inspect the list of rule code really executed when a C code is parsed, it might be helpful to proceed as in \<^theory>\Isabelle_C.C1\, by activating \<^theory_text>\declare[[C_parser_trace]]\. Then, the output window will display the sequence of Shift Reduce actions associated to the \<^theory_text>\C\ command of interest. \ section \Known Limitations, Troubleshooting\ subsection \The Document Model of the Isabelle/PIDE (applying for Isabelle 2019)\ subsubsection \Introduction\ text \ Embedding C directives in C code is an act of common practice in numerous applications, as well as largely highlighted in the C standard. As an example of frequently encountered directives, \#include \ is used to insert the content of \some_file.c\ at the place where it is written. In Isabelle/C, we can also write a C code containing directives like \#include\, and generally the PIDE reporting of directives is supported to a certain extent. Yet, the dynamic inclusion of arbitrary file with \#include\ is hurting a certain technological barrier. This is related to how the document model of Isabelle 2019 is functioning, but also to the design decisions behind the implementation of \<^theory_text>\C\ .. \\. Thus, providing a complete semantic implementation of \#include\ might be not as evident as usual, if not more dangerous, i.e. ``something requiring a manual intervention in the source of Isabelle 2019''. In the next part, we show why in our current implementation of Isabelle/C there is no way for user programmed extensions to exploit implicit dependencies between sub-documents in pure ML: a sub-document referred to via \#include \ will not lead to a reevaluation of a \<^theory_text>\C\ .. \\ command whenever modified.\ subsubsection \Embedding a language in Isabelle/PIDE\ text \ To clarify why the way a language being embedded in Isabelle is influencing the interaction between a future parser of the language with the Isabelle's document model, we recall the two ``different'' ways of embedding a language in Isabelle/PIDE. At its most basic form, the general syntactic scope of an Isabelle/Isar document can be seen as being composed of two syntactic alternations of editing space: fragments of the inner syntax language, themselves part of the more general outer syntax (the inner syntax is implemented as an atomic entity of the outer language); see \<^file>\~~/src/Doc/Isar_Ref/Outer_Syntax.thy\. So strictly speaking, when attempting to support a new language \L\ in Isabelle, there is always the question of fine-grain estimating which subsets of \L\ will be represented in the outer syntax part, and if it possibly remains any left subsets to be represented on the more inner (syntactic) part. Generally, to answer this question, there are several criteria to consider: \<^item> Are there any escaping symbols conflicting between \L\ and the outer (syntax) language, including for example the ASCII \<^verbatim>\"\ or \<^verbatim>\`\? \<^item> Is \L\ a realistic language, i.e. more complex than any combinations of outer named tokens that can be ever covered in terms of expressivity power (where the list of outer named tokens is provided in \<^file>\~~/src/Doc/Isar_Ref/Outer_Syntax.thy\)? \<^item> Is it preferable of not altering the outer syntax language with too specific and challenging features of \L\? This is particularly true since in Isabelle 2019, there is no way of modifying the outer syntax without making the modifications irremediably happen on its source code. For the above reasons, we have come up in Isabelle/C with the choice of making the full C language be supported inside the inner syntax allocated space. In particular, this has become all the more syntactically easy with the introduction of cartouches since Isabelle 2014.\<^footnote>\Fortunately, parsing tokens of C do not strongly conflict with cartouche delimiter symbols. For example, it should not be ethically wrong in C to write an opening cartouche symbol (possibly in a C comment) without writing any closing cartouche symbol afterwards. However, we have not encountered such C code in our tested codebase, and it is a functionality implicitly rejected by the current parser of Isabelle/C, as it is relying on Isabelle 2019's parser combinator library for the lexing part.\ However, for the case of the C language, certain C directives like \#include\ are meant to heavily interact with external files. In particular, resources would be best utilized if we were taking advantage of the Isabelle's asynchronous document model for such interaction task. Unfortunately, the inner syntax space only has a minimum interaction with the document model, compared to the outer syntax one. Otherwise said, be it for experimenting the inner syntax layer and see how far it can deal with the document layer, or otherwise reimplementing parts of Isabelle/C in the outer syntax layer, the two solutions are conducting to do modifications in the Isabelle 2019 source code. \ text \ Note that the language embedding space of \<^theory_text>\C\ closely resembles to how ML sources are delimited within a \<^theory_text>\ML\ command. Additionally, in ML, one can use antiquotations to also refer to external files (particularly in formal comments). Still, the problem is still present in ML: referred files are not loaded in the document model. \ subsubsection \Examples\ text \ \<^item> Commands declared as of type \thy_decl\ in the theory header are scheduled to be executed once. Additionally, they are not tracking the content of file names provided in argument, so a change there will not trigger a reevaluation of the associated command. For example, even if the type of \<^theory_text>\ML_file\ is not \thy_decl\, nothing prevents one to set it with \thy_decl\ as type. In particular, by doing so, it is no more possible to CTRL-hover-click on the file name written after \<^theory_text>\ML_file\. \<^item> To make a command \C\ track the content of \file\, whenever the file is changing, setting \C\ to be of type \thy_load\ in the theory header is a first step, but not enough. To be effective, \file\ must also be loaded, by either explicitly opening it, or clicking on its name after the command. Examples of commands in this situation requiring a preliminary one-time-click include: \<^theory_text>\external_file\, \<^theory_text>\bibtex_file\, \<^theory_text>\ML_file\. Internally, the click is bound to a Scala code invoking a request to make an asynchronous dependency to the newly opened document at ML side. \<^item> In terms of recursivity, for the case of a chain of sub-documents of the form (a theory file containing: \<^theory_text>\C_file \file0.c\\) \\\ (C file \<^verbatim>\file0.c\ containing: \<^C>\#include \) \\\ (C file \<^verbatim>\file1.c\ containing: \<^C>\#include \) \\\ (C file \<^verbatim>\file2.c\ containing: \<^C>\#include \), we ideally expect a modification in \<^verbatim>\file3.c\ be taken into account in all ancestor files including the initial theory, provoking the associated command of the theory be reevaluated. However in C, directives resolving might be close to Turing-complete. For instance, one can also include files based on particular conditional situations: \<^C>\#if _ #include #else #include #include #endif\ \<^item> When a theory is depending on other theories (such as \<^theory>\Isabelle_C.C_Eval\ depending on \<^theory>\Isabelle_C.C_Parser_Language\ and \<^theory>\Isabelle_C.C_Parser_Annotation\), modifying the list of theories in importation automatically triggers what the user is expecting: for example, the newly added theories are dynamically imported, any change by another external editor makes everything consequently propagated. Following the internal implementation of the document model engine, we basically distinguish two phases of document importation: either at start-up time, or dynamically on user requests. Although the case of start-up time can be handled in pure ML side, the language dedicated to express which Isabelle theory files to import is less powerful than the close-to-Turing-completeness expressivity of C directives. On the other hand, the dynamic importation of files on user requests seems to be performed (at the time of writing) through a too high level ML protocol, mostly called from Scala side. Due to the fact that Isabelle/C is currently implemented in pure ML, a solution also in pure ML would thus sound more natural (although we are not excluding solutions interacting with Scala, as long as the resulting can be implemented in Isabelle, preferably outside of its own source).\ subsection \Parsing Error versus Parsing Correctness\ text \ When trying to decide if the next parsing action is a Shift or Reduce action to perform, the grammar simulator \<^ML>\LALR_Parser_Eval.parse\ can actually decide to do another action: ignore everything and immediately stop the simulation. If the parser ever decides to stop, this can only be for two reasons: \<^item> The parser is supposed to have correctly finished its parsing task, making it be in an acceptance state. As acceptance states are encoded in the grammar, it is easy to find if this information is correct, or if it has to be adjusted in more detail by inspecting \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ (\<^file>\generated/c_grammar_fun.grm.sml\). \<^item> The parser seems to be unable to correctly finish its parsing task. In this case, the user will see an error be explicitly raised by the prover IDE. However raising an error is just the default behavior of Isabelle/C: the decision to whether raise interruptive errors ultimately depends on how front-end commands are implemented (such as \<^theory_text>\C\, \<^theory_text>\C_file\, etc.). For instance, similarly as to how outer syntax commands are implemented, we can imagine a tool implementing a kind of partial parsing, analyzing the longest sequence of well-formed input, and discarding some strategic next set of faulty tokens with a well suited informative message, so that the parsing process could be maximally repeated on what is coming afterwards. Currently, the default behavior of Isabelle/C is to raise the error defined in \<^ML>\C_Module.err\ at the very first opportunity \<^footnote>\At the time of writing it is: \<^emph>\No matching grammar rule\.\. The possible solutions to make the error disappear at the position the error is indicated can be detailed as follows: \<^item> Modifying the C code in input would be a first solution whenever we suspect something is making it erroneous (and when we have a reason to believe that the grammar is behaving as it should). \<^item> However, we could still get the above error in front of an input where one is usually expecting to see not causing a failure. In particular, there are several C features (such as C directives) explicitly left for semantic back-ends (pre-) processing, so in general not fully semantically processed at parsing time. For example, whereas the code \<^C>\#define i int i a;\ succeeds, replacing its first line with the directive \<^C>\#include \ will not initially work, even if \file.c\ contains \<^C>\#define i int\, as the former directive has been left for semantic back-end treatment. One way of solving this would be to modify the C code in input for it to be already preprocessed (without directives, for example the C example of \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c/blob/C/C11-BackEnds/AutoCorres_wrapper/examples/TestSEL4.thy\ is already provided as preprocessed). Another way would be adding a specific new semantic back-end implementing the automation of the preprocessing task (as done in - \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c/blob/C/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_integrated.thy\, where the + \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c/blob/C/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_TEC.thy\, where the back-end explicitly makes a call to \cpp\ at run-time). \<^item> Ultimately, modifying the grammar with new rules cancelling the exception would only work if the problem really relies on the grammar, as it was mentioned for the acceptance state. \ text \ In terms of parsing correctness, Isabelle/C provides at least two different parsers: \<^item> a parser limited to C99/C11 code provided in \<^dir>\../C11-FrontEnd\ that can parse certain liberal extensions out of the C standard~\<^footnote>\\<^url>\http://hackage.haskell.org/package/language-c\\; \<^item> and another parser accepting C99/C11/C18 code in \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c/tree/C/C18-FrontEnd\ that is close to the C standard while focusing on resolving ambiguities of the standard~\<^footnote>\\<^url>\https://github.com/jhjourdan/C11parser\\~\cite{DBLP:journals/toplas/JourdanP17}. \ text \ Note that the two parsers are not accepting/rejecting the same range of arbitrary C code. We have actually already encountered situations where an error is raised by one parser, while a success is happening with the other parser (and vice-versa). Consequently, in front of a C code, it can be a good recommendation to try out the parsing with all possible parsers of Isabelle/C. In any cases, a failure in one or several activated parsers might not be necessarily harmful: it might also indicate that a wrong parser has been selected, or a semantic back-end not yet supporting aspects of the C code being parsed. \ subsection \Exporting C Files to the File-System\ text \ From the Isabelle/C side, the task is easy, just type:\ C_export_file text \ ... which does the trick and generates a file \<^verbatim>\C_Appendices.c\. But hold on --- where is it? Well, Isabelle/C uses since version Isabelle2019 a virtual file-system. Exporting from it to the real file-system requires a few mouse-clicks (unfortunately). So activating the command \<^theory_text>\C_export_file\ leads to the output \<^verbatim>\See theory exports "C/*/C_Appendices.c"\ (see \autoref{fig:file-bro}), and clicking on the highlighted \<^verbatim>\theory exports\ lets Isabelle display a part of the virtual file-system (see subwidget left). Activating it in the subwidget lets jEdit open it as an editable file, which can be exported via ``\File \ Save As\\'' into the real file-system. \ end diff --git a/thys/Isabelle_C/C11-FrontEnd/document/root.bib b/thys/Isabelle_C/C11-FrontEnd/document/root.bib --- a/thys/Isabelle_C/C11-FrontEnd/document/root.bib +++ b/thys/Isabelle_C/C11-FrontEnd/document/root.bib @@ -1,670 +1,670 @@ @misc{bockenek:hal-02069705, TITLE = {{Using Isabelle/UTP for the Verification of Sorting Algorithms A Case Study}}, AUTHOR = {Bockenek, Joshua A and Lammich, Peter and Nemouchi, Yakoub and Wolff, Burkhart}, URL = {https://easychair.org/publications/preprint/CxRV}, NOTE = {Isabelle Workshop 2018, Colocated with Interactive Theorem Proving. As part of FLOC 2018, Oxford, GB.}, YEAR = {2018}, MONTH = Jul } @inproceedings{Tuong-IsabelleC:2019, author = {Fr{\'{e}}d{\'{e}}ric Tuong and Burkhart Wolff}, title = {{D}eeply {I}ntegrating {C11} {C}ode {S}upport into {I}sabelle/{PIDE}}, booktitle = {Proceedings 5th Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7 October 2019.}, year = {2019}, crossref = {journals/corr/Tuong-IsabelleC:2019}, - url = {https://easychair.org/smart-program/F-IDE2019/F-IDE-19-preprints.pdf}, - doi = {10.4204/EPTCS.999}, + url = {http://dx.doi.org/10.4204/EPTCS.310.3}, + doi = {10.4204/EPTCS.310.3}, pdf = {https://www.lri.fr/~wolff/papers/conf/2019-fide-isabelle_c.pdf} } @proceedings{journals/corr/Tuong-IsabelleC:2019, editor = {Rosemary Monahan and Virgile Prevosto and Jos{\'{e}} Proen{\c{c}}a}, title = {Proceedings 5th Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7 October 2019}, series = {{EPTCS}}, - volume = {999}, + volume = {310}, year = {2019}, - url = {https://easychair.org/smart-program/F-IDE2019/F-IDE-19-preprints.pdf}, - doi = {10.4204/EPTCS.999} + url = {http://dx.doi.org/10.4204/EPTCS.310}, + doi = {10.4204/EPTCS.310} } @book{DBLP:books/sp/NipkowPW02, author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, title = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic}, series = {Lecture Notes in Computer Science}, volume = {2283}, publisher = {Springer}, year = {2002}, url = {https://doi.org/10.1007/3-540-45949-9}, doi = {10.1007/3-540-45949-9}, isbn = {3-540-43376-7}, timestamp = {Tue, 14 May 2019 10:00:35 +0200}, biburl = {https://dblp.org/rec/bib/books/sp/NipkowPW02}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/sosp/KleinEHACDEEKNSTW09, author = {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and June Andronick and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood}, title = {seL4: formal verification of an {OS} kernel}, booktitle = {Proceedings of the 22nd {ACM} Symposium on Operating Systems Principles 2009, {SOSP} 2009, Big Sky, Montana, USA, October 11-14, 2009}, pages = {207--220}, year = {2009}, crossref = {DBLP:conf/sosp/2009}, url = {https://doi.org/10.1145/1629575.1629596}, doi = {10.1145/1629575.1629596}, timestamp = {Tue, 06 Nov 2018 16:59:32 +0100}, biburl = {https://dblp.org/rec/bib/conf/sosp/KleinEHACDEEKNSTW09}, bibsource = {dblp computer science bibliography, https://dblp.org} } @proceedings{DBLP:conf/sosp/2009, editor = {Jeanna Neefe Matthews and Thomas E. Anderson}, title = {Proceedings of the 22nd {ACM} Symposium on Operating Systems Principles 2009, {SOSP} 2009, Big Sky, Montana, USA, October 11-14, 2009}, publisher = {{ACM}}, year = {2009}, url = {https://doi.org/10.1145/1629575}, doi = {10.1145/1629575}, isbn = {978-1-60558-752-3}, timestamp = {Tue, 06 Nov 2018 16:59:32 +0100}, biburl = {https://dblp.org/rec/bib/conf/sosp/2009}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/tphol/CohenDHLMSST09, author = {Ernie Cohen and Markus Dahlweid and Mark A. Hillebrand and Dirk Leinenbach and Michal Moskal and Thomas Santen and Wolfram Schulte and Stephan Tobies}, title = {{VCC:} {A} Practical System for Verifying Concurrent {C}}, booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings}, pages = {23--42}, year = {2009}, url = {https://doi.org/10.1007/978-3-642-03359-9_2}, doi = {10.1007/978-3-642-03359-9_2}, timestamp = {Tue, 23 May 2017 01:12:08 +0200}, biburl = {https://dblp.org/rec/bib/conf/tphol/CohenDHLMSST09}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/cacm/Leroy09, author = {Xavier Leroy}, title = {Formal verification of a realistic compiler}, journal = {Commun. {ACM}}, volume = {52}, number = {7}, pages = {107--115}, year = {2009}, url = {http://doi.acm.org/10.1145/1538788.1538814}, doi = {10.1145/1538788.1538814}, timestamp = {Thu, 02 Jul 2009 13:36:32 +0200}, biburl = {https://dblp.org/rec/bib/journals/cacm/Leroy09}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/itp/Wenzel14, author = {Makarius Wenzel}, title = {Asynchronous User Interaction and Tool Integration in Isabelle/PIDE}, booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 14-17, 2014. Proceedings}, pages = {515--530}, year = {2014}, crossref = {DBLP:conf/itp/2014}, url = {https://doi.org/10.1007/978-3-319-08970-6\_33}, doi = {10.1007/978-3-319-08970-6\_33}, timestamp = {Tue, 14 May 2019 10:00:37 +0200}, biburl = {https://dblp.org/rec/bib/conf/itp/Wenzel14}, bibsource = {dblp computer science bibliography, https://dblp.org} } @proceedings{DBLP:conf/itp/2014, editor = {Gerwin Klein and Ruben Gamboa}, title = {Interactive Theorem Proving - 5th International Conference, {ITP} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 14-17, 2014. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {8558}, publisher = {Springer}, year = {2014}, url = {https://doi.org/10.1007/978-3-319-08970-6}, doi = {10.1007/978-3-319-08970-6}, isbn = {978-3-319-08969-0}, timestamp = {Tue, 14 May 2019 10:00:37 +0200}, biburl = {https://dblp.org/rec/bib/conf/itp/2014}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:journals/corr/Wenzel14, author = {Makarius Wenzel}, title = {System description: Isabelle/jEdit in 2014}, booktitle = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, {UITP} 2014, Vienna, Austria, 17th July 2014.}, pages = {84--94}, year = {2014}, crossref = {DBLP:journals/corr/BenzmullerP14}, url = {https://doi.org/10.4204/EPTCS.167.10}, doi = {10.4204/EPTCS.167.10}, timestamp = {Wed, 12 Sep 2018 01:05:15 +0200}, biburl = {https://dblp.org/rec/bib/journals/corr/Wenzel14}, bibsource = {dblp computer science bibliography, https://dblp.org} } @proceedings{DBLP:journals/corr/BenzmullerP14, editor = {Christoph Benzm{\"{u}}ller and Bruno {Woltzenlogel Paleo}}, title = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, {UITP} 2014, Vienna, Austria, 17th July 2014}, series = {{EPTCS}}, volume = {167}, year = {2014}, url = {https://doi.org/10.4204/EPTCS.167}, doi = {10.4204/EPTCS.167}, timestamp = {Wed, 12 Sep 2018 01:05:15 +0200}, biburl = {https://dblp.org/rec/bib/journals/corr/BenzmullerP14}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/mkm/BarrasGHRTWW13, author = {Bruno Barras and Lourdes Del Carmen Gonz{\'{a}}lez{-}Huesca and Hugo Herbelin and Yann R{\'{e}}gis{-}Gianas and Enrico Tassi and Makarius Wenzel and Burkhart Wolff}, title = {Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems}, booktitle = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of {CICM} 2013, Bath, UK, July 8-12, 2013. Proceedings}, pages = {359--363}, year = {2013}, crossref = {DBLP:conf/mkm/2013}, url = {https://doi.org/10.1007/978-3-642-39320-4\_29}, doi = {10.1007/978-3-642-39320-4\_29}, timestamp = {Sun, 02 Jun 2019 21:17:34 +0200}, biburl = {https://dblp.org/rec/bib/conf/mkm/BarrasGHRTWW13}, bibsource = {dblp computer science bibliography, https://dblp.org} } @proceedings{DBLP:conf/mkm/2013, editor = {Jacques Carette and David Aspinall and Christoph Lange and Petr Sojka and Wolfgang Windsteiger}, title = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of {CICM} 2013, Bath, UK, July 8-12, 2013. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {7961}, publisher = {Springer}, year = {2013}, url = {https://doi.org/10.1007/978-3-642-39320-4}, doi = {10.1007/978-3-642-39320-4}, isbn = {978-3-642-39319-8}, timestamp = {Sun, 02 Jun 2019 21:17:34 +0200}, biburl = {https://dblp.org/rec/bib/conf/mkm/2013}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/afp/LammichW19, author = {Peter Lammich and Simon Wimmer}, title = {{IMP2} - Simple Program Verification in Isabelle/HOL}, journal = {Archive of Formal Proofs}, volume = {2019}, year = {2019}, url = {https://www.isa-afp.org/entries/IMP2.html}, timestamp = {Mon, 20 May 2019 11:45:07 +0200}, biburl = {https://dblp.org/rec/bib/journals/afp/LammichW19}, bibsource = {dblp computer science bibliography, https://dblp.org} } @misc{frama-c-home-page, title = {The Frama-C Home Page}, author = {{CEA}-List}, year = 2019, month = jan, day = 10, url = {https://frama-c.com}, note = {Accessed \DTMdate{2019-03-24}} } @inproceedings{DBLP:conf/fm/LeinenbachS09, author = {Dirk Leinenbach and Thomas Santen}, title = {Verifying the Microsoft Hyper-V Hypervisor with {VCC}}, booktitle = {{FM} 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings}, pages = {806--809}, year = {2009}, url = {https://doi.org/10.1007/978-3-642-05089-3_51}, doi = {10.1007/978-3-642-05089-3_51}, timestamp = {Mon, 22 May 2017 17:11:19 +0200}, biburl = {https://dblp.org/rec/bib/conf/fm/LeinenbachS09}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/tap/Keller18, author = {Chantal Keller}, title = {Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL}, booktitle = {Tests and Proofs - 12th International Conference, {TAP} 2018, Held as Part of {STAF} 2018, Toulouse, France, June 27-29, 2018, Proceedings}, pages = {103--119}, year = {2018}, url = {https://doi.org/10.1007/978-3-319-92994-1\_6}, doi = {10.1007/978-3-319-92994-1\_6}, timestamp = {Mon, 18 Jun 2018 13:57:50 +0200}, biburl = {https://dblp.org/rec/bib/conf/tap/Keller18}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/itp/AissatVW16, author = {Romain A{\"{\i}}ssat and Fr{\'{e}}d{\'{e}}ric Voisin and Burkhart Wolff}, title = {Infeasible Paths Elimination by Symbolic Execution Techniques - Proof of Correctness and Preservation of Paths}, booktitle = {Interactive Theorem Proving - 7th International Conference, {ITP} 2016, Nancy, France, August 22-25, 2016, Proceedings}, pages = {36--51}, year = {2016}, url = {https://doi.org/10.1007/978-3-319-43144-4\_3}, doi = {10.1007/978-3-319-43144-4\_3}, timestamp = {Thu, 17 Aug 2017 16:22:01 +0200}, biburl = {https://dblp.org/rec/bib/conf/itp/AissatVW16}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/tocs/KleinAEMSKH14, author = {Gerwin Klein and June Andronick and Kevin Elphinstone and Toby C. Murray and Thomas Sewell and Rafal Kolanski and Gernot Heiser}, title = {Comprehensive formal verification of an {OS} microkernel}, journal = {{ACM} Trans. Comput. Syst.}, volume = {32}, number = {1}, pages = {2:1--2:70}, year = {2014}, url = {http://doi.acm.org/10.1145/2560537}, doi = {10.1145/2560537}, timestamp = {Tue, 03 Jan 2017 11:51:57 +0100}, biburl = {https://dblp.org/rec/bib/journals/tocs/KleinAEMSKH14}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/pldi/GreenawayLAK14, author = {David Greenaway and Japheth Lim and June Andronick and Gerwin Klein}, title = {Don't sweat the small stuff: formal verification of {C} code without the pain}, booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} '14, Edinburgh, United Kingdom - June 09 - 11, 2014}, pages = {429--439}, year = {2014}, url = {http://doi.acm.org/10.1145/2594291.2594296}, doi = {10.1145/2594291.2594296}, timestamp = {Tue, 20 Dec 2016 10:12:01 +0100}, biburl = {https://dblp.org/rec/bib/conf/pldi/GreenawayLAK14}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/mkm/BruckerACW18, author = {Achim D. Brucker and Idir A{\"{\i}}t{-}Sadoune and Paolo Crisafulli and Burkhart Wolff}, title = {Using the Isabelle Ontology Framework - Linking the Formal with the Informal}, booktitle = {Intelligent Computer Mathematics - 11th International Conference, {CICM} 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings}, pages = {23--38}, year = {2018}, url = {https://doi.org/10.1007/978-3-319-96812-4\_3}, doi = {10.1007/978-3-319-96812-4\_3}, timestamp = {Sat, 11 Aug 2018 00:57:41 +0200}, biburl = {https://dblp.org/rec/bib/conf/mkm/BruckerACW18}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/afp/TuongW15, author = {Fr{\'{e}}d{\'{e}}ric Tuong and Burkhart Wolff}, title = {A Meta-Model for the Isabelle {API}}, journal = {Archive of Formal Proofs}, volume = {2015}, year = {2015}, url = {https://www.isa-afp.org/entries/Isabelle\_Meta\_Model.shtml}, timestamp = {Mon, 07 Jan 2019 11:16:33 +0100}, biburl = {https://dblp.org/rec/bib/journals/afp/TuongW15}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/tphol/WinwoodKSACN09, author = {Simon Winwood and Gerwin Klein and Thomas Sewell and June Andronick and David Cock and Michael Norrish}, title = {Mind the Gap}, booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings}, pages = {500--515}, year = {2009}, crossref = {DBLP:conf/tphol/2009}, url = {https://doi.org/10.1007/978-3-642-03359-9\_34}, doi = {10.1007/978-3-642-03359-9\_34}, timestamp = {Fri, 02 Nov 2018 09:49:05 +0100}, biburl = {https://dblp.org/rec/bib/conf/tphol/WinwoodKSACN09}, bibsource = {dblp computer science bibliography, https://dblp.org} } @proceedings{DBLP:conf/tphol/2009, editor = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel}, title = {Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {5674}, publisher = {Springer}, year = {2009}, url = {https://doi.org/10.1007/978-3-642-03359-9}, doi = {10.1007/978-3-642-03359-9}, isbn = {978-3-642-03358-2}, timestamp = {Tue, 23 May 2017 01:12:08 +0200}, biburl = {https://dblp.org/rec/bib/conf/tphol/2009}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/afp/BruckerTW14, author = {Achim D. Brucker and Fr{\'{e}}d{\'{e}}ric Tuong and Burkhart Wolff}, title = {Featherweight {OCL:} {A} Proposal for a Machine-Checked Formal Semantics for {OCL} 2.5}, journal = {Archive of Formal Proofs}, volume = {2014}, year = {2014}, url = {https://www.isa-afp.org/entries/Featherweight\_OCL.shtml}, timestamp = {Mon, 07 Jan 2019 11:16:33 +0100}, biburl = {https://dblp.org/rec/bib/journals/afp/BruckerTW14}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/tacas/SananZHZTL17, author = {David San{\'{a}}n and Yongwang Zhao and Zhe Hou and Fuyuan Zhang and Alwen Tiu and Yang Liu}, title = {CSimpl: {A} Rely-Guarantee-Based Framework for Verifying Concurrent Programs}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, {TACAS} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}}, pages = {481--498}, year = {2017}, crossref = {DBLP:conf/tacas/2017-1}, url = {https://doi.org/10.1007/978-3-662-54577-5\_28}, doi = {10.1007/978-3-662-54577-5\_28}, timestamp = {Mon, 18 Sep 2017 08:38:37 +0200}, biburl = {https://dblp.org/rec/bib/conf/tacas/SananZHZTL17}, bibsource = {dblp computer science bibliography, https://dblp.org} } @proceedings{DBLP:conf/tacas/2017-1, editor = {Axel Legay and Tiziana Margaria}, title = {Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, {TACAS} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}}, series = {Lecture Notes in Computer Science}, volume = {10205}, year = {2017}, url = {https://doi.org/10.1007/978-3-662-54577-5}, doi = {10.1007/978-3-662-54577-5}, isbn = {978-3-662-54576-8}, timestamp = {Wed, 24 May 2017 08:28:32 +0200}, biburl = {https://dblp.org/rec/bib/conf/tacas/2017-1}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/itp/HouSTL17, author = {Zhe Hou and David San{\'{a}}n and Alwen Tiu and Yang Liu}, title = {Proof Tactics for Assertions in Separation Logic}, booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP} 2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings}, pages = {285--303}, year = {2017}, crossref = {DBLP:conf/itp/2017}, url = {https://doi.org/10.1007/978-3-319-66107-0\_19}, doi = {10.1007/978-3-319-66107-0\_19}, timestamp = {Mon, 18 Sep 2017 08:38:37 +0200}, biburl = {https://dblp.org/rec/bib/conf/itp/HouSTL17}, bibsource = {dblp computer science bibliography, https://dblp.org} } @proceedings{DBLP:conf/itp/2017, editor = {Mauricio Ayala{-}Rinc{\'{o}}n and C{\'{e}}sar A. Mu{\~{n}}oz}, title = {Interactive Theorem Proving - 8th International Conference, {ITP} 2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {10499}, publisher = {Springer}, year = {2017}, url = {https://doi.org/10.1007/978-3-319-66107-0}, doi = {10.1007/978-3-319-66107-0}, isbn = {978-3-319-66106-3}, timestamp = {Wed, 06 Sep 2017 14:53:52 +0200}, biburl = {https://dblp.org/rec/bib/conf/itp/2017}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/sigbed/CarrascosaCMBC14, author = {E. Carrascosa and Javier Coronel and Miguel Masmano and Patricia Balbastre and Alfons Crespo}, title = {XtratuM hypervisor redesign for {LEON4} multicore processor}, journal = {{SIGBED} Review}, volume = {11}, number = {2}, pages = {27--31}, year = {2014}, url = {https://doi.org/10.1145/2668138.2668142}, doi = {10.1145/2668138.2668142}, timestamp = {Tue, 06 Nov 2018 12:51:31 +0100}, biburl = {https://dblp.org/rec/bib/journals/sigbed/CarrascosaCMBC14}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/cacm/Earley70, author = {Jay Earley}, title = {An Efficient Context-Free Parsing Algorithm}, journal = {Commun. {ACM}}, volume = {13}, number = {2}, pages = {94--102}, year = {1970}, url = {https://doi.org/10.1145/362007.362035}, doi = {10.1145/362007.362035}, timestamp = {Wed, 14 Nov 2018 10:22:30 +0100}, biburl = {https://dblp.org/rec/bib/journals/cacm/Earley70}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{DBLP:journals/jfp/Hutton92, author = {Graham Hutton}, title = {Higher-Order Functions for Parsing}, journal = {J. Funct. Program.}, volume = {2}, number = {3}, pages = {323--343}, year = {1992}, url = {https://doi.org/10.1017/S0956796800000411}, doi = {10.1017/S0956796800000411}, timestamp = {Sat, 27 May 2017 14:24:34 +0200}, biburl = {https://dblp.org/rec/bib/journals/jfp/Hutton92}, bibsource = {dblp computer science bibliography, https://dblp.org} } @article{journals/afp/TuongW19, author = {Fr{\'{e}}d{\'{e}}ric Tuong and Burkhart Wolff}, title = {Clean - An Abstract Imperative Programming Language and its Theory}, journal = {Archive of Formal Proofs}, volume = {2019}, year = {2019}, url = {https://www.isa-afp.org/entries/Clean.html}, } @article{DBLP:journals/toplas/JourdanP17, author = {Jacques{-}Henri Jourdan and Fran{\c{c}}ois Pottier}, title = {A Simple, Possibly Correct {LR} Parser for {C11}}, journal = {{ACM} Trans. Program. Lang. Syst.}, volume = {39}, number = {4}, pages = {14:1--14:36}, year = {2017}, url = {https://doi.org/10.1145/3064848}, doi = {10.1145/3064848}, timestamp = {Tue, 06 Nov 2018 12:51:29 +0100}, biburl = {https://dblp.org/rec/bib/journals/toplas/JourdanP17}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{DBLP:conf/ictac/FosterZW16, author = {Simon Foster and Frank Zeyda and Jim Woodcock}, title = {Unifying Heterogeneous State-Spaces with Lenses}, booktitle = {Theoretical Aspects of Computing - {ICTAC} 2016 - 13th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings}, pages = {295--314}, year = {2016}, crossref = {DBLP:conf/ictac/2016}, url = {https://doi.org/10.1007/978-3-319-46750-4\_17}, doi = {10.1007/978-3-319-46750-4\_17}, timestamp = {Tue, 14 May 2019 10:00:38 +0200}, biburl = {https://dblp.org/rec/bib/conf/ictac/FosterZW16}, bibsource = {dblp computer science bibliography, https://dblp.org} } @proceedings{DBLP:conf/ictac/2016, editor = {Augusto Sampaio and Farn Wang}, title = {Theoretical Aspects of Computing - {ICTAC} 2016 - 13th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {9965}, year = {2016}, url = {https://doi.org/10.1007/978-3-319-46750-4}, doi = {10.1007/978-3-319-46750-4}, isbn = {978-3-319-46749-8}, timestamp = {Tue, 14 May 2019 10:00:38 +0200}, biburl = {https://dblp.org/rec/bib/conf/ictac/2016}, bibsource = {dblp computer science bibliography, https://dblp.org} } @phdthesis{Foster2009BidirectionalPL, author = {John Nathan Foster}, title = {Bidirectional programming languages}, school = {University of Pennsylvania}, year = {2009}, url = {https://repository.upenn.edu/edissertations/56/} } @article{DBLP:journals/toplas/FosterGMPS07, author = {J. Nathan Foster and Michael B. Greenwald and Jonathan T. Moore and Benjamin C. Pierce and Alan Schmitt}, title = {Combinators for bidirectional tree transformations: {A} linguistic approach to the view-update problem}, journal = {{ACM} Trans. Program. Lang. Syst.}, volume = {29}, number = {3}, pages = {17}, year = {2007}, url = {https://doi.org/10.1145/1232420.1232424}, doi = {10.1145/1232420.1232424}, timestamp = {Tue, 06 Nov 2018 12:51:29 +0100}, biburl = {https://dblp.org/rec/bib/journals/toplas/FosterGMPS07}, bibsource = {dblp computer science bibliography, https://dblp.org} } @inproceedings{brucker.wolff:isadof-design-impl:2019, author = {Achim D. Brucker and Burkhart Wolff}, title = {Isabelle/{DOF}: Design and Implementation}, booktitle = {Software Engineering and Formal Methods - 17th International Conference, {SEFM} 2019, Oslo, Norway, September 16-20, 2019, Proceedings}, pages = {275--292}, year = {2019}, crossref = {conf/sefm/2019}, url = {https://doi.org/10.1007/978-3-030-30446-1\_15}, doi = {10.1007/978-3-030-30446-1\_15} } @proceedings{conf/sefm/2019, editor = {Peter Csaba {\"{O}}lveczky and Gwen Sala{\"{u}}n}, title = {Software Engineering and Formal Methods - 17th International Conference, {SEFM} 2019, Oslo, Norway, September 16-20, 2019, Proceedings}, series = {Lecture Notes in Computer Science}, volume = {11724}, publisher = {Springer}, year = {2019}, url = {https://doi.org/10.1007/978-3-030-30446-1}, doi = {10.1007/978-3-030-30446-1}, isbn = {978-3-030-30445-4} } diff --git a/thys/Isabelle_C/C11-FrontEnd/examples/C0.thy b/thys/Isabelle_C/C11-FrontEnd/examples/C0.thy --- a/thys/Isabelle_C/C11-FrontEnd/examples/C0.thy +++ b/thys/Isabelle_C/C11-FrontEnd/examples/C0.thy @@ -1,213 +1,228 @@ (****************************************************************************** * Isabelle/C * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) chapter \Example: Lexer Stress Test\ theory C0 imports "../C_Main" begin declare[[C_lexer_trace]] section \Regular C Code\ +subsection \Comments, Keywords and Pragmas\ + C \ \Nesting of comments following the example suite of \<^url>\https://gcc.gnu.org/onlinedocs/cpp/Initial-processing.html\\ \ /* inside /* inside */ int a = "outside"; // inside // inside until end of line int a = "outside"; /* inside // inside inside */ int a = "outside"; // inside /* inside until end of line int a = "outside"; \ C \ \Backslash newline\ \ i\ n\ t a = "/* // /\ *\ fff */\ "; \ C \ \Backslash newline, Directive \<^url>\https://gcc.gnu.org/onlinedocs/cpp/Initial-processing.html\\ \ /\ * */ # /* */ defi\ ne FO\ O 10\ 20\ C \ \Directive: conditional\ \ #ifdef a #elif #else #if #endif #endif \ (* C \ \Directive: pragma\ \# f # "/**/" /**/ # /**/ // # _Pragma /\ **/("a") \ *) C \ \Directive: macro\ \ #define a zz #define a(x1,x2) z erz(( zz #define a (x1,x2) z erz(( zz #undef z #if #define a zz #define a(x1,x2) z erz(( zz #define a (x1,x2) z erz(( zz #endif \ +subsection \Scala/jEdit Latency on Multiple Bindings\ + C \ \Example of obfuscated code \<^url>\https://en.wikipedia.org/wiki/International_Obfuscated_C_Code_Contest\\ \ #define _ -F<00||--F-OO--; int F=00,OO=00;main(){F_OO();printf("%1.3f\n",4.*-F/OO/OO);}F_OO() { _-_-_-_ _-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_-_-_-_-_ _-_-_-_-_-_-_-_ _-_-_-_ } \ +text \ Select inside the ball, experience the latency. +A special keyboard combination ``Ctrl-like key\<^footnote>\on Apple: Cmd\ + Shift + +Enter'' lets Isabelle/Scala/jEdit enter in a mode where the selected bound occurrences can be all +simultaneously replaced by new input characters typed on the keyboard. (The ``select-entity'' action +exists since Isabelle2016-1, see the respective section ``Prover IDE -- Isabelle/Scala/jEdit'' in +the NEWS.)\ + +subsection \Lexing and Parsing Obfuscated Sources\ + +text \Another lexer/parser - stress test: parsing an obfuscated C source.\ + C \ \Example of obfuscated code \<^url>\https://www.ioccc.org/2018/endoh1/prog.c\\ \ #define/*__Int3rn^ti[]n/l_()I3fusc^t3|]_C_C<>I7E_C[]nt3st__*/L/*__MMXVIII__*/for #include/*!"'()*+,-./12357:;<=>?CEFGHIJKLMNSTUVWXYZ[]^_`cfhijklmnrstuvwxyz{|}*/ char*r,F[1<<21]="~T/}3(|+G{>/zUhy;Jx+5wG>u55t.?sIZrC]n.;m+:l+Hk]WjNJi/Sh+2f1>c2H`)(_2(^L\ -]=([1/Z<2Y7/X12W:.VFFU1,T77S+;N?;M/>L..K1+JCCI<+(=3)Z-;*(:*.Y/5(-=)2*-U,\ /+-?5'(,+++***''EE>T,215IEUF:N`2`:?GK;+^`+?>)5?>U>_)5GxG).2K.2};}_235(]:5,S7E1(vTSS,-SSTvU(<-HG\ -2E2/2L2/EE->E:?EE,2XMMMM1Hy`)5rHK;+.T+?[n2/_2{LKN2/_|cK2+.2`;}:?{KL57?|cK:2{NrHKtMMMK2nrH;rH[n" "CkM_E21-E,-1->E(_:mSE/LhLE/mm:2Ul;2M>,2KW-+.-u).5Lm?fM`2`2nZXjj?[nT+?KH~-?f<;G_x2;;2XT7LXIuuVF2X(G(GVV-:-:KjJ]HKLyN7UjJ3.WXjNI2KNx#&#&&$#$;ZXIc###$&$$#>7[LMv{&&&&#&##L,l2TY.&$#$#&&$,(iiii,#&&&#$#$?TY2.$#$1(x###;2EE[t,\ SSEz.SW-k,T&&jC?E-.$## &#&57+$$# &&&W1-&$$7W -J$#$kEN&#& $##C^+$##W,h###n/+L2YE" "2nJk/H;YNs#$[,:TU(#$ ,: &&~H>&# Y; &&G_x ,mT&$YE-#& 5G $#VVF$#&zNs$$&Ej]HELy\ CN/U^Jk71<(#&:G7E+^&# l|?1 $$Y.2$$ 7lzs WzZw>&$E -x; 2zsW/$$#HKt&$$v>+t1(>" "7>S7S,;TT,&$;S7S>7&#>E_::U $$'",op ,*G= F,*I=957+F ;int*t,k,O, i, j,T[+060<<+020];int M( int m,int nop){;;;return+ m%(0+nop );;} int*tOo,w, h,z,W;void(C) (int n){n=putchar(n);}int f,c,H=11,Y=64<<2,Z,pq,X ;void(E/*d */)( int/*RP*/n ){L(Z=k+00; Z; Z/=+2+000)G[000]=*G*!!f |M(n,2)<=13*3?*G-*r?*I++=*G:(*I++=r[1],*I++=r[2]):1;L(j=12,r =I;(*I=i=getchar())>-1;I++)i-7-3?I-=i<32||127<=i,j+=12:(H+=17+3,W=W-1;r++)*r- 7-3?J(),w++:(w=z,h+=17+3);C(71);C(73);V('*'*'1'*7);C(57);C(32*3+1);V(W);V(H);C(122*2);L(V(i=z);i <32*3;)C(i++/3*X/31);C(33);C(X);C(11);L(G="SJYXHFUJ735";*G;)C(*G++-5);C(3);V(1);L(V(j=z);j<21*3; j++){k=257;V(63777);V(k<<2);V(M(j,32)?11:511);V(z);C(22*2);V(i=f=z);V(z);V(W);V(H);V(1<<11);r= G=I+W*H;L(t=T;i<1<<21;i++)T[i]=iX?X:G-r ,C(k),k;)L(;k--;C(*r++/*---#$%&04689@ABDOPQRabdegopq---*/));}C(53+6);return(z);} \ section \Experiments with \<^dir>\../../src_ext/parser_menhir\\ declare[[C_lexer_trace = false]] subsection \Expecting to succeed\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/aligned_struct_c18.c\\ C_file \../../src_ext/parser_menhir/tests/argument_scope.c\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/atomic.c\\ C_file \../../src_ext/parser_menhir/tests/atomic_parenthesis.c\ C_file \../../src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.c\ C_file \../../src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.ok.c\ C_file \../../src_ext/parser_menhir/tests/block_scope.c\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/c11-noreturn.c\\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/c1x-alignas.c\\ C_file \../../src_ext/parser_menhir/tests/char-literal-printing.c\ C_file \../../src_ext/parser_menhir/tests/c-namespace.c\ C_file \../../src_ext/parser_menhir/tests/control-scope.c\ C_file \../../src_ext/parser_menhir/tests/dangling_else.c\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/dangling_else_lookahead.c\\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/dangling_else_lookahead.if.c\\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/declaration_ambiguity.c\\ C_file \../../src_ext/parser_menhir/tests/declarators.c\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/declarator_visibility.c\\ C_file \../../src_ext/parser_menhir/tests/designator.c\ C_file \../../src_ext/parser_menhir/tests/enum.c\ C_file \../../src_ext/parser_menhir/tests/enum_constant_visibility.c\ C_file \../../src_ext/parser_menhir/tests/enum_shadows_typedef.c\ C_file \../../src_ext/parser_menhir/tests/enum-trick.c\ C_file \../../src_ext/parser_menhir/tests/expressions.c\ C_file \../../src_ext/parser_menhir/tests/function-decls.c\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/function_parameter_scope.c\\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/function_parameter_scope_extends.c\\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/if_scopes.c\\ C_file \../../src_ext/parser_menhir/tests/local_scope.c\ C_file \../../src_ext/parser_menhir/tests/local_typedef.c\ C_file \../../src_ext/parser_menhir/tests/long-long-struct.c\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/loop_scopes.c\\ C_file \../../src_ext/parser_menhir/tests/namespaces.c\ C_file \../../src_ext/parser_menhir/tests/no_local_scope.c\ C_file \../../src_ext/parser_menhir/tests/parameter_declaration_ambiguity.c\ C_file \../../src_ext/parser_menhir/tests/parameter_declaration_ambiguity.test.c\ C_file \../../src_ext/parser_menhir/tests/statements.c\ C_file \../../src_ext/parser_menhir/tests/struct-recursion.c\ C_file \../../src_ext/parser_menhir/tests/typedef_star.c\ C_file \../../src_ext/parser_menhir/tests/types.c\ C_file \../../src_ext/parser_menhir/tests/variable_star.c\ subsection \Expecting to fail\ C_file \../../src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.fail.c\ \<^cancel>\C_file \../../src_ext/parser_menhir/tests/dangling_else_misleading.fail.c\\ end diff --git a/thys/Isabelle_C/C11-FrontEnd/examples/C_paper.thy b/thys/Isabelle_C/C11-FrontEnd/examples/C_paper.thy --- a/thys/Isabelle_C/C11-FrontEnd/examples/C_paper.thy +++ b/thys/Isabelle_C/C11-FrontEnd/examples/C_paper.thy @@ -1,200 +1,200 @@ (****************************************************************************** * Isabelle/C * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) chapter \Examples from the F-IDE Paper\ theory C_paper imports "../C_Main" begin text \ This theory contains the examples presented in F-IDE 2019~\cite{Tuong-IsabelleC:2019}. \ section \Setup\ ML\ \ \Annotation Commands Mimicking the \<^theory_text>\setup\ command\ val _ = Theory.setup (C_Inner_Syntax.command C_Inner_Isar_Cmd.setup' C_Parse.ML_source ("\setup", \<^here>, \<^here>)) val C' = C_Module.C' fun C opt = case opt of NONE => C' (C_Module.env (Context.the_generic_context ())) | SOME env => C' env fun C_def dir name _ _ = Context.map_theory (C_Inner_Syntax.command' (C_Inner_Syntax.drop1 (C_Scan.Right ( (fn src => fn context => C' (C_Stack.Data_Lang.get' context |> #2) src context) , dir))) C_Parse.C_source name) \ \Defining the ML Antiquotation \C_def\ to define on the fly new C annotation commands\ local in val _ = Theory.setup (ML_Antiquotation.declaration @{binding "C_def"} (Scan.lift (Parse.sym_ident -- Parse.position Parse.name)) (fn _ => fn (top_down, (name, pos)) => tap (fn ctxt => Context_Position.reports ctxt [(pos, Markup.keyword1)]) #> C_Context.fun_decl "cmd" "x" ( "C_def " ^ (case top_down of "\" => "C_Inner_Syntax.bottom_up" | "\" => "C_Env.Top_down" | _ => error "Illegal symbol") ^ " (\"" ^ name ^ "\", " ^ ML_Syntax.print_position pos ^ ")"))) end \ text \ The next command is predefined here, so that the example below can later refer to the constant. \ definition [simplified]: "UINT_MAX \ (2 :: nat) ^ 32 - 1" section \Defining Annotation Commands\ ML \ \\<^theory>\Isabelle_C.C_Command\\ \ local datatype antiq_hol = Invariant of string (* term *) val scan_colon = C_Parse.$$$ ":" >> SOME fun command cmd scan0 scan f = C_Annotation.command' cmd "" (K (scan0 -- (scan >> f) >> K C_Env.Never)) in val _ = Theory.setup ((* 1 '@' *) command ("INVARIANT", \<^here>) scan_colon C_Parse.term Invariant #> command ("INV", \<^here>) scan_colon C_Parse.term Invariant) end \ text\Demonstrating the Effect of Annotation Command Context Navigation \ C \ int sum1(int a) { while (a < 10) /*@ @ INV: \\\ @ highlight */ { a = a + 1; } return a; }\ C \ int sum2(int a) /*@ ++@ INV: \\\ ++@ highlight */ { while (a < 10) { a = a + 1; } return a; }\ C (*NONE*) \ \starting environment = empty\ \ int a (int b) { return &a + b + c; } /*@ \setup \fn stack_top => fn env => C (SOME env) \int c = &a + b + c;\\ \setup \fn stack_top => fn env => C NONE \int c = &a + b + c;\\ declare [[C_starting_env = last]] C (*SOME*) \int c = &a + b + c;\ */\ section \Proofs inside C-Annotations\ -\ \See also: \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c/blob/C/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_integrated.thy\\ +\ \See also: \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c/blob/C/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_TEC.thy\\ C \ #define SQRT_UINT_MAX 65536 /*@ lemma uint_max_factor [simp]: "UINT_MAX = SQRT_UINT_MAX * SQRT_UINT_MAX - 1" by (clarsimp simp: UINT_MAX_def SQRT_UINT_MAX_def) */\ term SQRT_UINT_MAX section \Scheduling the Effects on the Logical Context\ C \int _; /*@ @ C \//@ C1 \int _; //@ @ \setup\ \@{C_def \ C2}\ \ @ C1 \//* C2 \int _;\\ \ @ C1\ \//* C2 \int _;\\ \\ @ C \//* C2 \int _;\ \ \setup \@{C_def \ (* bottom-up *) C1 }\ \setup \@{C_def \ (* top-down *) "C1\"}\ */\ section \As Summary: A Spaghetti Language --- Bon Appétit!\ text\... with the Bonus of a local C-inside-ML-inside-C-inside-Isar ...\ ML\ fun highlight (_, (_, pos1, pos2)) = tap (fn _ => Position.reports_text [((Position.range (pos1, pos2) |> Position.range_position, Markup.intensify), "")]) \ C (*NONE*) \ \ the command starts with a default empty environment \ \int f (int a) //@ ++& \setup \fn stack_top => fn env => highlight stack_top\ { /*@ @ \setup \fn stack_top => fn env => C (SOME env) (* the command starts with some provided environment *) \int b = a + b; //@ C1' \int c; //@ @ \setup\ \@{C_def \ C2'}\ \ @ C1' \//* C2' \int d;\\ \ @ C1'\ \//* C2' \int d;\\ \ int b = a + b + c + d;\\ @ \setup \fn stack_top => fn env => C NONE \#define int int int b = a + b; //* C2' \int c = b;\\\ \setup \@{C_def \ (* bottom-up *) C1' }\ \setup \@{C_def \ (* top-down *) "C1'\"}\ */ return a + b + c + d; /* explicit highlighting */ }\ text \ Note that in the current design-implementation of Isabelle/C, C directives have a propagation side-effect to any occurring subsequent C annotations, even if C directives are supposed to be all evaluated before any C code. (Making such effect inexistent would be equally easier to implement though, this is what was the default behavior of directives in previous versions of Isabelle/C.)\ end