Merge from master.

README.md

@@ -108,6 +108,17 @@ The repository is organised as follows.
 Dependencies
 ------------
 
+### Hardware
+
+Almost all proofs in this repository should work within 4GB of RAM. Proofs
+involving the C refinement, will usually need the 64bit mode of polyml and
+about 16GB of RAM.
+
+The proofs distribute reasonably well over multiple cores, up to about 8
+cores are useful.
+
+### Software
+
 The proofs in this repository use `Isabelle2015`. A copy of Isabelle
 is included in the repository setup.
 
@@ -132,6 +143,13 @@ full build environment for seL4:
   * seL4 [development tool chain][8] on Debian and Ubuntu
   * `make` version 3.81 or higher
 
+You can get away with avoiding a full cross compiler setup form the above,
+but you will need at least these:
+
+    sudo apt-get install python-pip python-dev libxml2-utils
+    sudo pip install tempita
+    sudo pip install psutil
+
 *On MacOS*: here it is harder to get a full cross-compiler setup going. For
 normal proof development, a full setup is not necessary, though. You mostly
 need a gcc-compatible C pre-processor and python. Try the following steps:

camkes/adl-spec/Examples_CAMKES.thy

@@ -41,15 +41,15 @@ text {*
 \begin{verbatim}
   procedure Simple {
     string echo_string(in string s);
-    int echo_int(int int i);
+    int echo_int(in int i);
     void echo_parameter(in int pin, out int pout);
   };
 \end{verbatim}
 
   The representation of this in Isabelle is quite similar:\footnote{The
-  procedure parameter types @{text int} and @{text uint}
+  procedure parameter type @{text int}
-  are synonyms for
+  is a synonym for
-  @{term integer} and @{term "unsigned integer"}, respectively, and are
+  @{term integer} and is
   therefore not modelled in Isabelle.}
 *}
 definition

camkes/adl-spec/Types_CAMKES.thy

@@ -45,37 +45,34 @@ text {*
   Although both symbols map to the same underlying type, these have different
   constraints (e.g. IDL symbols become direct substrings of code-level symbols
   and hence need to respect symbol naming restrictions for the target
-  language(s)) and will be extended to represent these in a future iteration of
+  language(s)).
-  this specification.
 *}
 
 subsection {* \label{subsec:methods}Methods *}
 text {*
-  Methods are the elements that make up a CAmkES trait (described below).
+  Methods are the elements that make up a CAmkES procedure (described below).
-  Each method within a CAmkES trait has a list of parameters defined by a
+  Each method within a CAmkES procedure has a list of parameters defined by a
   type, direction and symbol name. Each method also has an optional return
   value type. The valid types for method parameters and return values include
   a set of high level types designed to abstract the types available in a
-  general programming language. By using only these types in a trait
+  general programming language. By using only these types in a procedure
   description, the interface can be implemented in any valid target language.
 
   When fixed width types are required for an interface there are a set of types
-  available that are C-specific. Using these types in a trait description
+  available that are C-specific. Using these types in a procedure description
-  precludes implementing or using the trait in a component not written in C.
+  precludes implementing or using the procedure in a component not written in C.
   In general the high-level types should be used in preference to the C-specific
   types.
 
-  Array types are supported as method parameters and return types in CAmkES in
+  In high-level languages, arrays may have attached size information, while in
-  two flavours: arrays with a given size and arrays terminated by a
+  C this information is passed as an extra parameter to their containing
-  @{text NULL} (@{text 0})
+  method. Arrays are parameterised with the underlying type of
-  value. Both types of arrays are parameterised with the underlying type of
   their elements. Similar to primitive types, using a high-level type for the
   elementary type of an array allows it to be implemented or used in any
   component, while using a C-specific type prevents implementing or using it in
   a component not written in C. Arrays of arrays and multidimensional arrays are
   not supported.
 *}
-(* Based on camkes-templates/v4nicta_generic/* *)
 
 datatype number =
     -- "High level types"
@@ -102,12 +99,6 @@ datatype textual =
   | String
     -- "C-specific types"
   | char
-text {*
-  Note that a string in C is a @{text NULL}-terminated character array.
-  If a C-specific
-  string is required in a trait it is best to specify it manually (i.e. as
-  a @{text "TerminatedArray (Textual char)"}).
-*}
 
 datatype primitive =
     Numerical number
@@ -122,17 +113,16 @@ datatype param_type =
   | Array array
 
 text {*
-  Rather than having a single return value per trait method, each
+  Rather than having a single return value per procedure method, each
   method parameter can be an input parameter, an output parameter, or both.
 *}
-(* Better than representing in/out separately because \<not>in \<and> \<not>out is not valid. *)
 datatype param_direction =
-    InParameter
+    InParameter (* also covers 'refin' *)
   | OutParameter
   | InOutParameter
 
 text {*
-  Each trait comprises a collection of methods that each have an
+  Each procedure comprises a collection of methods that each have an
   optional return type,
   identifier and a list of parameters. Each parameter has a type and an
   identifier.
@@ -147,7 +137,7 @@ record method =
   m_name        :: idl_symbol
   m_parameters  :: "parameter list"
 text {*
-  The translation from trait methods in IDL to their representation in
+  The translation from procedure methods in IDL to their representation in
   Isabelle is straightforward. The CAmkES method
 
 \begin{verbatim}
@@ -175,10 +165,10 @@ text {*
   interfaces that consist of a list of function calls and interfaces
   that have other patterns of interaction.
 
-  There are three basic types of supported interfaces. The first, @{text trait},
+  There are three basic types of supported interfaces. The first, @{text procedure},
   is used for modelling traditional caller-callee semantics of interaction. The
-  second, @{text event} is used for asynchronous notifications such as interrupts.
+  second, @{text event}, is used for asynchronous notifications such as interrupts.
-  Finally, @{text dataport} is used to model shared memory communication.
+  Finally, @{text dataport}, is used to model shared memory communication.
 *}
 type_synonym procedure = "method list"
 type_synonym event     = nat -- "ID"
@@ -196,19 +186,13 @@ text {*
 
   Native connectors map directly to implementation mechanisms. These are the
   types of connectors that are found in almost all component platform models. The
-  event-style connectors, @{text AsynchronousEvent} and @{text RPCEvent} are
+  event-style connector, @{text AsynchronousEvent}, is
   used to model communication consisting of an identifier with no associated message
   data.
 *}
-(* Based on camkes-generator/include/std_connector.camkes. *)
 datatype native_connector_type =
     AsynchronousEvent -- "an asynchronous notification"
-  | RPCEvent -- "a synchronous notification"
   | RPC -- "a synchronous channel"
-  | DirectCall -- "a synchronous channel to a component in the same address space"
-(* FIXME: This is the first mention of address spaces. This should be introduced
- * somewhere earlier.
- *)
   | SharedData -- "a shared memory region"
 
 text {*

camkes/adl-spec/Wellformed_CAMKES.thy

@@ -108,7 +108,7 @@ definition
 where
   "wellformed_connector c \<equiv> (case c of
     SyncConnector t \<Rightarrow> (case t of
-      Native n \<Rightarrow> n \<in> {RPCEvent, RPC, DirectCall}
+      Native n \<Rightarrow> n \<in> {RPC}
      |Hardware h \<Rightarrow> h \<in> {HardwareIOPort}
      |Export e \<Rightarrow> e \<in> {ExportRPC})
    |AsyncConnector t \<Rightarrow> (case t of

camkes/adl-spec/document/root.tex

@@ -175,7 +175,7 @@ the Defense Advanced Research Projects Agency or the U.S.Government.}
 {\large \authors 
 
 \vspace{2ex}
-October 2012}
+April 2014}
 
 \vfill
 {\small

spec/cspec/README.md

@@ -47,5 +47,5 @@ Remarks
 To speed up interactive development, the bitfield code generator can be
 configured to skip the corresponding proofs and produce sorried
 (unproven) property statements only. To achieve this, set the
-environment variable `SORRY_BITFIELD_PROOFS` to `yes`.
+environment variable `SORRY_BITFIELD_PROOFS` to `1`.
 

tools/autocorres/program_info.ML

@@ -152,8 +152,9 @@ fun get_prog_info ctxt filename : prog_info =
     (* Get the gamma variable, mapping function numbers to function bodies in
      * SIMPL. *)
     val gamma =
-      Const (Consts.intern (Proof_Context.consts_of ctxt) "\<Gamma>", dummyT)
+      (Const (Consts.intern (Proof_Context.consts_of ctxt) "\<Gamma>", dummyT)
-      |> Syntax.check_term ctxt
+       |> Syntax.check_term ctxt)
+      handle TERM _ => error "autocorres: could not find any functions -- \<Gamma> is not defined."
 
     (*
      * Return a Const term of the local-variable getters/setters for the given

tools/c-parser/Absyn-Expr.ML

@@ -59,7 +59,7 @@ and designator =
 
 
 datatype ecenv =
-         CE of {enumenv : (int * string option) Symtab.table,
+         CE of {enumenv : (IntInf.int * string option) Symtab.table,
                           (* lookup is from econst name to value and the
                              name of the type it belongs to, if any
                              (they can be anonymous) *)
@@ -111,7 +111,7 @@ sig
 
 
   datatype ecenv = datatype ExprDatatype.ecenv (* "enumerated constant environment" *)
-  val eclookup : ecenv -> string -> (int * string option) option
+  val eclookup : ecenv -> string -> (IntInf.int * string option) option
   val constify_abtype : ecenv -> expr CType.ctype -> int CType.ctype
   val consteval : ecenv -> expr -> IntInf.int
 
@@ -428,7 +428,7 @@ in
     in
       case Symtab.lookup enumenv s of
         NONE => Fail ("Variable "^s^ " can't appear in a constant expression")
-      | SOME (v, _) => (fi v, Signed Int)
+      | SOME (v, _) => (v, Signed Int)
     end
   | StructDot _ =>
     Fail "Can't evaluate fieldref in constant expression"

tools/c-parser/calculate_state.ML

@@ -315,8 +315,7 @@ end
  *)
 fun get_sorted_structs cse =
 let
-  val global_rcd = get_globals_rcd cse
+  val rcds = get_senv cse
-  val rcds = get_senv cse @ global_rcd
   val sorted_structs =
       if null rcds then []
       else let
@@ -420,8 +419,7 @@ fun mk_thy_types cse install thy = let
      for consumption by later phases of the translation.
 
   *)
-  val global_rcd = get_globals_rcd cse
+  val rcds = get_senv cse
-  val rcds = get_senv cse @ global_rcd
   val sorted_structs = get_sorted_structs cse
 
   open MemoryModelExtras

tools/c-parser/program_analysis.ML

@@ -261,7 +261,7 @@ datatype csenv (* CalculateState environment *) =
                  scope : var_info Symtab.table list,
                  array_mentions : (int ctype * int) Binaryset.set,
                  enumenv : string wrap list *
-                           (int * string option) Symtab.table,
+                           (IntInf.int * string option) Symtab.table,
                  globinits : Absyn.expr MSymTab.table,
                  heaptypes : int ctype Binaryset.set,
                  call_info : fncall_type Binaryset.set Symtab.table,
@@ -769,7 +769,7 @@ fun process_enumdecl (enameopt_w,econsts) env = let
       | NONE => let
           val e_val = case eopt of
                         NONE => i
-                      | SOME e => IntInf.toInt (consteval (cse2ecenv env) e)
+                      | SOME e => consteval (cse2ecenv env) e
           val tab' = Symtab.update(node ecn_w, (e_val, node enameopt_w)) alist
         in
           (e_val + 1, ecn_w::set, tab')

tools/c-parser/testfiles/globals_in_record.thy

@@ -18,13 +18,11 @@ install_C_file "globals_in_record.c"
 context globals_in_record begin
 
 thm globals.equality
-thm adglobs_struct_idupdates adglobs_struct_tag_def
 
 find_theorems "zuzu_'"
 thm globals.zuzu_'_def
 
 find_theorems "zozo"
-thm adglobs_struct.zozo.zozo_def
 
 find_theorems "zyzy"
 thm zyzy_def

tools/c-parser/testfiles/jiraver443.thy

@@ -0,0 +1,22 @@
+theory jiraver443
+  imports "../CTranslation"
+begin
+
+  declare [[allow_underscore_idents=true]]
+  (* 3014 lines, with  78 globals:  works ;
+     3498 lines, with  96 globals:  works ;
+     3719 lines, with 108 globals:  fails
+     3719 lines, (down to _camkes_call_tls_var_to_465_2),
+      with following functions removed:
+         get__camkes_call_tls_var_to_465
+         get_echo_int_4_l_to
+                                    fails
+  *)
+  install_C_file "jiraver443.c"
+
+  context jiraver443
+  begin
+    thm get__camkes_ret_tls_var_from_244_body_def
+  end
+
+end

tools/c-parser/testfiles/jiraver443a.c

@@ -0,0 +1,23 @@
+struct foo {
+  int x, thread_index;
+} glob;
+struct foo* camkes_get_tls(void)
+{
+  return &glob;
+}
+_Noreturn void abort(void);
+
+static int a1;
+static int a2;
+static int *get(void) __attribute__((__unused__));
+static int *get(void) {
+  switch (camkes_get_tls()->thread_index) {
+  case 1:
+    return &a1;
+  case 2:
+    return &a2;
+  default:
+    (void)0;
+    abort();
+  }
+}

tools/c-parser/testfiles/jiraver443a.thy

@@ -0,0 +1,15 @@
+theory jiraver443a
+  imports "../CTranslation"
+begin
+
+  install_C_file "jiraver443a.c"
+  
+context jiraver443a
+begin
+
+term "symbol_table"
+thm get_body_def
+
+end (* context *)
+
+end

tools/c-parser/testfiles/void_ptr_init.c

@@ -0,0 +1,21 @@
+/*
+ * Copyright 2015, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ */
+
+/*
+ * Initialiser for void*; fixed in git-aa162a0.
+ */
+
+struct A {
+  void *p;
+};
+
+void f(void) {
+  struct A a = { 0 };
+}

tools/c-parser/testfiles/void_ptr_init.thy

@@ -0,0 +1,17 @@
+(*
+ * Copyright 2015, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+theory void_ptr_init
+imports "../CTranslation"
+begin
+
+install_C_file "void_ptr_init.c"
+
+end