1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11signature USER_TYPE_DECL_CHECKING =
12sig
13
14  type t
15  type csenv = ProgramAnalysis.csenv
16  val initial_state : t
17  val finalise : t -> theory -> theory
18
19  val struct_type :
20      csenv ->
21      { struct_type : string * (string * typ * int Absyn.ctype) list,
22        state : t } ->
23      theory -> t * theory
24  val array_type : csenv ->
25                   {element_type : typ, array_size : int, state : t} ->
26                   theory -> t * theory
27end
28
29
30
31signature MEMORY_MODEL_EXTRAS =
32sig
33
34  val extended_heap_ty : typ
35
36  val check_safety : {heap: term, ptrval:term} -> term * term
37  val dereference_ptr : {heap:term, ptrval:term} -> term
38  val mk_heap_update_extended : term -> term
39
40  val mk_aux_guard : term -> term
41  val mk_aux_update : term -> term
42  val mk_aux_type : typ -> typ
43
44  val check_global_record_type : string -> theory -> theory
45
46  val mk_lookup_proc_pair : term -> term -> term -> term * term
47
48  structure UserTypeDeclChecking : USER_TYPE_DECL_CHECKING
49end (* sig *)
50(*
51  [extended_heap_ty] is the Isabelle type of heaps that are to be manipulated
52  by the StrictC programs.  It will include (some way or another) the underlying
53  heap (mapping addresses to bytes), but may also include other stuff.
54
55  [check_safety{heap,ptrval}] generates a pair of terms that will be
56  used to guard an assignment if the ms ("memory safety") flag is set.
57  (By default it is not set.)  The ptrval is a term of pointer type
58  pointing to the address that is about to be written to; the heap is
59  the term of the current (extended) heap.  A result (t1,t2) should
60  have t1 of type state-predicate (i.e., state -> bool), and t2 of type
61  error.  That is, t1 will be the guard of the checked assignment, and t2 will
62  be the error a failing guard would cause.
63
64  If you don't ever intend to use the 'ms' flag, this function could
65  just raise an exception.
66
67  [dereference_ptr{heap,ptrval}] returns the value stored in (extended)
68  heap at address ptrval.  The value ptrval will be of type Ptr sometype, the
69  result should be a term of type sometype.
70
71  [mk_heap_update_extended t] lifts t, an update on an underlying
72  primitive heap (a term of type `primheap -> primheap`), returning an
73  update on the extended_heap_ty (extended_heap_ty -> extended_heap_ty`)
74
75  [mk_aux_guard t] The term t is of the form (predicate $ var), where var is
76  of type `state`.  The predicate has come from text entered as part of an
77  "aux update".  This is a statement form such as
78
79     /** AUXUPD: "some term" */
80
81  The string "some term" is actually mangled to become
82    "antiquoteParseTranslation (some term)" and it is this that is
83  parsed.  My understanding of apt is that makes a normal term
84  implicit on a state.
85
86  This term should have type   mk_aux_type statetype, which has to be a
87  function type because it is applied to a var (corresponding to the current
88  state).
89
90  mk_aux_guard is applied to the value to generate a boolean that corresponds
91  to a guard.
92
93  [mk_aux_update t] is applied to the same sort of term as mk_aux_guard, and
94  returns an updator for the extended heap.
95
96  [mk_aux_type ty] turns the type corresponding to machine states into the type
97  used to implement auxiliary guards and updators.
98
99  [check_global_record_type s thy] takes the current theory and the
100  name of the global variable record (containing the heap, the c_exn
101  variable, the global variable struct and the phantom state).  It
102  then does whatever proving is necessary to confirm the global
103  variable record is OK.
104
105  [UserTypeDeclChecking]
106  This structure implements additional checks on new C types that arise in the
107  analysed program.  The model allows for additional data to be passed through
108  all successive calls using the type UserTypeDeclChecking.t.  Once the
109  initial value of this is to hand, calls will be made to
110    struct_type     with details of new struct types
111                     - the Isabelle record type that corresponds to
112                       the struct type will already have been defined,
113                       along with appropriate accessor and updator
114                       functions.
115    array_type      with details of new array types
116                     - there is already a binary array type operator
117                       in the background theory, so the array type
118                       already exists.  However, the particular
119                       combination required by the user may still need
120                       things proved of it.
121    arraysize_type  to establish properties of number types
122  The calls are made in appropriate topological order.  Calls for the same
123  type may be repeated.
124
125*)
126