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
170
171
172
173
174
175
176
177
178
179
180
181
182
183
open Utils
open Dcalc.Ast
module type Backend = sig
val init_backend : unit -> unit
type backend_context
val make_context : decl_ctx -> typ Marked.pos VarMap.t -> backend_context
type vc_encoding
val print_encoding : vc_encoding -> string
type model
type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
val solve_vc_encoding : backend_context -> vc_encoding -> solver_result
val print_model : backend_context -> model -> string
val is_model_empty : model -> bool
val translate_expr :
backend_context -> 'm Dcalc.Ast.marked_expr -> backend_context * vc_encoding
end
module type BackendIO = sig
val init_backend : unit -> unit
type backend_context
val make_context : decl_ctx -> typ Marked.pos VarMap.t -> backend_context
type vc_encoding
val translate_expr :
backend_context -> 'm Dcalc.Ast.marked_expr -> backend_context * vc_encoding
type model
type vc_encoding_result =
| Success of vc_encoding * backend_context
| Fail of string
val print_positive_result : Conditions.verification_condition -> string
val print_negative_result :
Conditions.verification_condition ->
backend_context ->
model option ->
string
val encode_and_check_vc :
Dcalc.Ast.decl_ctx ->
Conditions.verification_condition * vc_encoding_result ->
unit
end
module MakeBackendIO (B : Backend) = struct
let init_backend = B.init_backend
type backend_context = B.backend_context
let make_context = B.make_context
type vc_encoding = B.vc_encoding
let translate_expr = B.translate_expr
type model = B.model
type vc_encoding_result =
| Success of B.vc_encoding * B.backend_context
| Fail of string
let print_positive_result (vc : Conditions.verification_condition) : string =
match vc.Conditions.vc_kind with
| Conditions.NoEmptyError ->
Format.asprintf "%s This variable never returns an empty error"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
| Conditions.NoOverlappingExceptions ->
Format.asprintf "%s No two exceptions to ever overlap for this variable"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
let print_negative_result
(vc : Conditions.verification_condition)
(ctx : B.backend_context)
(model : B.model option) : string =
let var_and_pos =
match vc.Conditions.vc_kind with
| Conditions.NoEmptyError ->
Format.asprintf "%s This variable might return an empty error:\n%s"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
(Pos.retrieve_loc_text (Marked.get_mark vc.vc_variable))
| Conditions.NoOverlappingExceptions ->
Format.asprintf
"%s At least two exceptions overlap for this variable:\n%s"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
(Pos.retrieve_loc_text (Marked.get_mark vc.vc_variable))
in
let counterexample : string option =
if !Cli.disable_counterexamples then
Some "Counterexample generation is disabled so none was generated."
else
match model with
| None ->
Some
"The solver did not manage to generate a counterexample to explain \
the faulty behavior."
| Some model ->
if B.is_model_empty model then None
else
Some
(Format.asprintf
"The solver generated the following counterexample to explain \
the faulty behavior:\n\
%s"
(B.print_model ctx model))
in
var_and_pos
^
match counterexample with
| None -> ""
| Some counterexample -> "\n" ^ counterexample
(** [encode_and_check_vc] spawns a new Z3 solver and tries to solve the
expression [vc] **)
let encode_and_check_vc
(decl_ctx : decl_ctx)
(vc : Conditions.verification_condition * vc_encoding_result) : unit =
let vc, z3_vc = vc in
Cli.debug_print "For this variable:\n%s\n"
(Pos.retrieve_loc_text (pos vc.Conditions.vc_guard));
Cli.debug_format "This verification condition was generated for %a:@\n%a"
(Cli.format_with_style [ANSITerminal.yellow])
(match vc.vc_kind with
| Conditions.NoEmptyError ->
"the variable definition never to return an empty error"
| NoOverlappingExceptions -> "no two exceptions to ever overlap")
(Dcalc.Print.format_expr decl_ctx)
vc.vc_guard;
match z3_vc with
| Success (encoding, backend_ctx) -> (
Cli.debug_print "The translation to Z3 is the following:\n%s"
(B.print_encoding encoding);
match B.solve_vc_encoding backend_ctx encoding with
| ProvenTrue -> Cli.result_print "%s" (print_positive_result vc)
| ProvenFalse model ->
Cli.error_print "%s" (print_negative_result vc backend_ctx model)
| Unknown -> failwith "The solver failed at proving or disproving the VC")
| Fail msg ->
Cli.error_print "%s The translation to Z3 failed:\n%s"
(Cli.with_style [ANSITerminal.yellow] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Var.get (Marked.unmark vc.vc_variable))))
msg
end