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