Theory C_paper

(******************************************************************************
 * 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 "../main/C_Main"
begin

text ‹ This theory contains the examples presented in F-IDE 2019 paper~cite"Tuong-IsabelleC:2019". ›

section ‹Setup›

ML― ‹Annotation Commands Mimicking the setup command›
val _ = Theory.setup
          (C_Inner_Syntax.command C_Inner_Isar_Cmd.setup' C_Parse.ML_source ("≃setup", , ))

val C = C_Module.C'

fun C_def dir name _ _ =
  Context.map_theory 
    (C_Inner_Syntax.command'
      (C_Inner_Syntax.drop1
        (C_Scan.Right ( (fn src => fn context =>
                          C_Module.C' (SOME (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 ― ‹theoryIsabelle_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", ) scan_colon C_Parse.term Invariant
                      #> command ("INV", ) 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 [[Cenv0 = last]]
    C        (*SOME*)    int c = &a + b + c;
*/

section ‹Proofs inside C-Annotations›

― ‹See also: 🌐‹https://gitlab.lisn.upsaclay.fr/burkhart.wolff/Isabelle_C/-/blob/C/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_linear_CCT.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_defC2} \
                            @ 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 ...›

MLfun 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_defC2'} \
                                                         @ 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