Too complex counterexample
When I have a VC that cannot be proved by a prover, I try to get a counterexample.
module Memory
use int.Int
type base = Absolute | Address int
type loc = { base_addr : base ; offset : int }
type value = | VInt int
type permission = | Freeable
type value_map =
| Update value_map int int value
| Uninitialized
type memory = { mem_contents : base -> value_map; }
type t = { mutable contents : memory }
end
module Main
use Memory
val global_memory : Memory.t
let constant null : loc = { base_addr = Absolute ; offset = 0 }
val loc_eq (m : Memory.t) (l1 l2 : loc) : bool
requires { [@expl:pointer comparable]
match l1.base_addr, l2.base_addr with
| Absolute, Absolute -> true
| Absolute, _ -> l1.offset = 0
| _, Absolute -> l2.offset = 0
| _ -> true
end }
let rec invalid_cmp (p : Memory.loc) : int =
if (loc_eq global_memory p null) then 0 else 1
end
If I want a counter-example on this example wiht Why3 1.4 and CVC4 1.6, I get a stack overflow with this backtrace:
Fatal error: exception Stack overflow
Raised by primitive operation at Collect_data_model.model_value_of_tree.(fun) in file "src/driver/collect_data_model.ml", line 401, characters 27-68
Called from Collect_data_model.model_value_of_tree in file "src/driver/collect_data_model.ml", line 405, characters 40-73
And something similar if I test on master.
I suspect the counter-example generated to be too big (by too big I mean that it contains too much constructors Update
: Update (Update (Update ...)))
) but I am not sure. If the counter-example is too big, I would rather have no counterexample than a failure.
Maybe the pattern matching is the problem. If I remove the pattern matching in the function loc_eq
to replace it with a simpler formula, I do not have a backtrace anymore.
The command line that I ran is why3 --debug=stack_trace prove file.mlw -P "CVC4,,counterexamples"
.