1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
|
(**************************************************************************)
(* Sail *)
(* *)
(* Copyright (c) 2013-2017 *)
(* Kathyrn Gray *)
(* Shaked Flur *)
(* Stephen Kell *)
(* Gabriel Kerneis *)
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
(* Alasdair Armstrong *)
(* Brian Campbell *)
(* Thomas Bauereiss *)
(* Anthony Fox *)
(* Jon French *)
(* Dominic Mulligan *)
(* Stephen Kell *)
(* Mark Wassell *)
(* *)
(* All rights reserved. *)
(* *)
(* This software was developed by the University of Cambridge Computer *)
(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
(* *)
(* Redistribution and use in source and binary forms, with or without *)
(* modification, are permitted provided that the following conditions *)
(* are met: *)
(* 1. Redistributions of source code must retain the above copyright *)
(* notice, this list of conditions and the following disclaimer. *)
(* 2. 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. *)
(* *)
(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR 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 AUTHOR 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. *)
(**************************************************************************)
open Ast
open Ast_defs
open Ast_util
open Jib
open Jib_util
open Jib_ssa
open Smtlib
val opt_ignore_overflow : bool ref
val opt_auto : bool ref
val opt_debug_graphs : bool ref
val opt_propagate_vars : bool ref
val zencode_name : name -> string
module IntSet : Set.S with type elt = int
module EventMap : Map.S with type key = Property.event
(** These give the default bounds for various SMT types, stored in the
initial_ctx. *)
val opt_default_lint_size : int ref
val opt_default_lbits_index : int ref
val opt_default_vector_index : int ref
type ctx = {
lbits_index : int;
(** Arbitrary-precision bitvectors are represented as a (BitVec lbits_index, BitVec (2 ^ lbits_index)) pair. *)
lint_size : int;
(** The size we use for integers where we don't know how large they are statically. *)
vector_index : int;
(** A generic vector, vector('a) becomes Array (BitVec vector_index) 'a.
We need to take care that vector_index is large enough for all generic vectors. *)
register_map : id list CTMap.t;
(** A map from each ctyp to a list of registers of that ctyp *)
tuple_sizes : IntSet.t ref;
(** A set to keep track of all the tuple sizes we need to generate types for *)
tc_env : Type_check.Env.t;
(** tc_env is the global type-checking environment *)
pragma_l : Ast.l;
(** A location, usually the $counterexample or $property we are
generating the SMT for. Used for error messages. *)
arg_stack : (int * string) Stack.t;
(** Used internally to keep track of function argument names *)
ast : Type_check.tannot ast;
(** The fully type-checked ast *)
shared : ctyp Bindings.t;
(** Shared variables. These variables do not get renamed by
Smtlib.suffix_variables_def, and their SSA number is
omitted. They should therefore only ever be read and never
written. Used by sail-axiomatic for symbolic values in the
initial litmus state. *)
preserved : IdSet.t;
(** icopy instructions to an id in preserved will generated a
define-const (by using Smtlib.Preserved_const) that will not be
simplified away or renamed. It will also not get a SSA
number. Such variables can therefore only ever be written to
once, and never read. They are used by sail-axiomatic to
extract information from the generated SMT. *)
events : smt_exp Stack.t EventMap.t ref;
(** For every event type we have a stack of boolean SMT
expressions for each occurance of that event. See
src/property.ml for the event types *)
node : int;
pathcond : smt_exp Lazy.t;
(** When generating SMT for an instruction pathcond will contain
the global path conditional of the containing block/node in the
control flow graph *)
use_string : bool ref;
use_real : bool ref
(** Set if we need to use strings or real numbers in the generated
SMT, which then requires set-logic ALL or similar depending on
the solver *)
}
(** Compile an AST into Jib suitable for SMT generation, and initialise a context. *)
val compile : Type_check.Env.t -> Type_check.tannot ast -> cdef list * Jib_compile.ctx * ctx
(* TODO: Currently we internally use mutable stacks and queues to
avoid any issues with stack overflows caused by some non
tail-recursive list functions, as the generated SMT can be very
long, especially without any optimization. Not clear that this is
really better than just using lists. *)
val smt_header : ctx -> cdef list -> smt_def list
val smt_query : ctx -> Property.query -> smt_exp
val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t * int * (ssa_elem list * cf_node) Jib_ssa.array_graph
module type Sequence = sig
type 'a t
val create : unit -> 'a t
val add : 'a -> 'a t -> unit
end
(** Optimize SMT generated by smt_instr_list. SMT definitions are
added to the result sequence in the order they should appear in the
final SMTLIB file. Depending on the order in which we want to
process the results we can either use a FIFO queue or a LIFO
stack, or any other structure. *)
module Make_optimizer(S : Sequence) : sig
val optimize : smt_def Stack.t -> smt_def S.t
end
val serialize_smt_model :
string -> Type_check.Env.t -> Type_check.tannot ast -> unit
val deserialize_smt_model :
string -> cdef list * ctx
(** Generate SMT for all the $property and $counterexample pragmas in
an AST, and write it to appropriately named files. *)
val generate_smt :
(string * string * l * 'a val_spec) Bindings.t (* See Property.find_properties *)
-> (string -> string) (* Applied to each function name to generate the file name for the smtlib file *)
-> Type_check.Env.t
-> Type_check.tannot ast
-> unit
|
