cvc4-models.mlw 5.82 KB
Newer Older
1
module M
David Hauzar's avatar
David Hauzar committed
2
  use import ref.Ref
3
  use import list.List
David Hauzar's avatar
David Hauzar committed
4
  use import int.Int
5

6
7
  type int_type = Integer int

8
9
10
11
  (**********************************************************
   ** Getting counterexamples for terms of primitive types **
   **********************************************************)
  val y "model" "model_trace:y" :ref int
12

13
  let incr ( x23 "model" "model_trace:x23" : ref int ): unit
14
  ensures { "model_vc" "model_func" !x23 = old !x23 + 2 + !y }
15
  =
16
  (*#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#*)
17
18
19
  y := !y + 1;
  x23 := !x23 + 1;
  x23 := !x23 + 1
20

David Hauzar's avatar
David Hauzar committed
21
22
23
24
  let test_loop ( x "model" "model_trace:x" : ref int ): unit
  ensures { !x < old !x }
  =
  incr x;
25
  while "model" "model_trace:cond" !x > 0 do invariant { !x >= 0 } variant { !x } x := !x - 1 done
26

27
28
29
  (**************************************
   ** Getting counterexamples for maps **
   **************************************)
30
  use import map.Map
31
  let test_map (x "model" : ref (map int int)) : unit
32
  ensures { "model_vc" !x[0] <> !x[1] }
33
  =
34
  x := Map.set !x 0 3
35

36
  (* Multi-dimensional maps *)
37
38
  let test_map_multidim1 (x "model" : ref (map int (map int int))) : unit
  ensures { "model_vc" !x[0][0] <> !x[1][1] }
39
40
  =
  x := Map.set !x 0 (Map.get !x 1)
41

42
43
44
45
46
47
48
49
50
51
52
53
54
55
  let test_map_multidim2 (x "model" : ref (map int (map int int))) : unit
  ensures { "model_vc" !x[0][0] <> !x[1][1] }
  =
  let x0 = Map.get !x 0 in
  let x0 = Map.set x0 0 3 in
  x := Map.set !x 0 x0


  (*****************************************
   ** Getting counterexamples for records **
   *****************************************)

  (*** In all cases, records are decomposed using match eval ***)

56
  type r = {f "model_trace:field_f" :int; g:bool}
57
58
59
60
61
62
63
64
65
66
67
68
69
70

  (* Projection functions *)
  function projf_r_f "model_trace:.f" (x : r) : int
  =
  x.f
  function projf_r_g "model_trace:.g" (x : r) : bool
  =
  x.g
  meta "inline : no" function projf_r_f
  meta "model_projection" function projf_r_f
  meta "inline : no" function projf_r_g
  meta "model_projection" function projf_r_g

  let record_match_eval_test1 (x "model" "model_trace:x" : r) : int
71
72
73
74
75
76
77
  ensures { "model_vc" "model_func" result = 1 }
  =
  if x.g then
    x.f
  else
    1

78
79
80
81
82
83
  let record_match_eval_test2 (x "model_projected" : r ) : int
  ensures { result = 1 }
  =
  x.f

  let record_match_eval_test3 (x "model" "model_trace:x" : ref r) : unit
84
85
  ensures { !x.g }
  =
86
  x := { !x with f = 6}
87

88
  let record_match_eval_test4 (x "model" "model_trace:x" : ref r) : r
89
90
91
92
93
  ensures { "model_vc" "model_func" result.g }
  =
  x := { !x with f = 6 };
  !x

94
  val re "model_projected" : ref r
95

96
  let test_record_match_eval_test5 (x "model" "model_trace:x" : ref r) : r
97
98
99
100
101
  ensures { "model_vc" "model_func" result = !re }
  =
  x := { !x with f = 6 };
  !x

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
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204

  (***********************************************************
   ** Getting counterexamples for records and maps together **
   ***********************************************************)
  (*** Records and maps together ***)
  type r_map = {f_map:map bool int; g_bool:bool}

  function projf_r_map_f_map "model_trace:.f_map" (rec_map : r_map) : map bool int
  =
  rec_map.f_map
  function projf_r_map_g "model_trace:.g_map" (rec_map : r_map) : bool
  =
  rec_map.g_bool
  meta "inline : no" function projf_r_map_f_map
  meta "model_projection" function projf_r_map_f_map

  meta "inline : no" function projf_r_map_g
  meta "model_projection" function projf_r_map_g

  (* Tests *)
  (* Warning: does not terminate *)
  let map_record_proj_test1 (map_rec "model_projected" : map bool r)
  ensures { result = 0 }
  =
  map_rec[true].f

  let record_map_proj_test2 (rec_map "model_projected" : r_map)
  ensures { result = 0 }
  =
  rec_map.f_map[true]

  val re_rec_map "model_projected" : r_map

  let record_map_proj_test3 (rec_map "model_projected" : r_map)
  ensures { result = re_rec_map }
  =
  rec_map

  (*******************************************
   ** Definitions of projections used below **
   *******************************************)
  function projfi "model_trace:.projfi" (l : int) : int
  = l
  meta "inline : no" function projfi
  meta "model_projection" function projfi

  function projf1 "model_trace:.projf1" (l : int) : bool
  =
  l > 0
  function projf2 "model_trace:.projf2" (l : int) : bool
  =
  l <= 0
  meta "inline : no" function projf1
  meta "model_projection" function projf1
  meta "inline : no" function projf2
  meta "model_projection" function projf2

  (*******************************************************
   ** Getting counterexamples for maps with projections **
   ******************************************************)

  (* Both indices and range of map will be projected using
     projfi, projf1, and projf2
     Warning: cvc4 is not able to handle projections there  *)
  let proj_map_test1 (x "model_projected" : ref (map int int)) : unit
  ensures { "model_vc" !x[0] <> !x[1] }
  =
  x := Map.set !x 0 3

  (* No projection function for bool -> the array should be
     present in counterexample as it is. *)
  let proj_map_test2 (x "model_projected" : ref (map int bool)) : unit
  ensures { "model_vc" !x[0] <> !x[1] }
  =
  x := Map.set !x 0 true

  (*********************************
   ** Non-terminating projections **
   *********************************)
   (* Warning: if definition of the following projections are present,
      the proof of everything below will not terminate. *)
  function projfl "model_trace:.projfl" (l : list int_type) : int
  =
  match l with
  | Nil -> 0
  | Cons (Integer n) _ -> n
  | _ -> 0
  end
  meta "inline : no" function projfl
  meta "model_projection" function projfl

  (* list int_type will be projected using projfl to int,
     int will be projected using projfi, projf1, and projf2
     Warning: does not terminate. *)
  let proj_test ( l "model_projected" : list int_type) : int
  ensures { result > 0  }
  =
  match l with
  | Nil -> 1
  | Cons (Integer n) _ -> n
  | _ -> 1
  end

205
end