Commit fc1b4fe5 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'new_ide'

# Conflicts:
#	bench/ce/
parents 091f023c 52e6f5e9
......@@ -267,10 +267,11 @@ src/coq-tactic/why3tac.cmx: WARNINGS:=$(WARNINGS)-58
# build targets
byte: lib/why3/why3.cma
opt: lib/why3/why3.cmxa
opt: lib/why3/why3.cmxa lib/why3/why3.cmxs
lib/why3/why3.cma: lib/why3/why3.cmo
lib/why3/why3.cmxa: lib/why3/why3.cmx
lib/why3/why3.cmxs: lib/why3/why3.cmx
lib/why3/why3.cmo: $(LIBCMO)
$(SHOW) 'Linking $@'
......@@ -1443,10 +1444,11 @@ byte: $(OCAMLLIBS_CMO)
opt: $(OCAMLLIBS_CMX)
byte: lib/why3/why3extract.cma
opt: lib/why3/why3extract.cmxa
opt: lib/why3/why3extract.cmxa lib/why3/why3extract.cmxs
lib/why3/why3extract.cma: lib/why3/why3extract.cmo
lib/why3/why3extract.cmxa: lib/why3/why3extract.cmx
lib/why3/why3extract.cmxs: lib/why3/why3extract.cmx
lib/why3/why3extract.cmo: $(OCAMLLIBS_CMO)
$(SHOW) 'Linking $@'
......
......@@ -2,42 +2,52 @@
dir=`dirname $0`
updateoracle=false
files=""
while test $# != 0; do
case "$1" in
"-update-oracle")
updateoracle=true;;
"")
updateoracle=false;;
*)
echo "$0: Unknown option '$1'"
exit 2
files="$files $1"
esac
shift
done
if test "$files" = "" ; then
files="ce/*.mlw"
fi
cd $dir
run_cvc4_15 () {
printf " $1... "
../bin/why3prove.opt -P "CVC4,1.5" --timelimit 1 --get-ce $1 | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)/ (time hidden)/' > $1.out
if cmp $1.oracle $1.out > /dev/null 2>&1 ; then
# $1 = prover, $2 = file
run () {
printf " $2 ($1)... "
f="$2_$1"
../bin/why3prove.opt -P "$1" --timelimit 1 --get-ce "$2.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)/ (time hidden)/' > "$f.out"
if cmp "$f.oracle" "$f.out" > /dev/null 2>&1 ; then
echo "ok"
else
if $updateoracle; then
echo "Updating oracle for $1"
mv $1.out $1.oracle
echo "Updating oracle for $2, prover $1"
mv "$f.out" "$f.oracle"
else
echo "FAILED!"
echo "diff is the following:"
diff $1.oracle $1.out
diff "$f.oracle" "$f.out"
fi
fi
}
for f in ce/*.mlw; do
run_cvc4_15 $f
for file in $files; do
filebase=`basename $file .mlw`
run CVC4,1.5 ce/$filebase
run Z3,4.5.0 ce/$filebase
run Z3,4.6.0 ce/$filebase
done
module M
use import int.Int
type int_type = Integer int
goal G : forall x : int_type. match x with Integer y -> y > 0 end
(*
(*********************************
** 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
*)
end
ce/algebraic_type.mlw M G : Unknown (other)
ce/algebraic_type.mlw M G : Unknown (other)
ce/algebraic_type.mlw M G : Unknown (other)
theory T
use import int.Int
goal g_no_lab : forall x:int. x >= 42 -> x + 3 <= 50
goal g_lab0 : forall x:int. (x >= 42) ->
(x + 3 <= 50)
constant g : int
goal g2_lab : forall x:int. (g >= x)
goal newgoal : forall x1 [@model_trace:X] x2 x3 x4 x5 x6 x7 x8.
(x1 + 1 = 2) ->
(x2 + 1 = 2) ->
(x3 + 1 = 2) ->
(x4 + 1 = 2) ->
(x5 + 1 = 2) ->
(x6 + 1 = 2) ->
(x7 + 1 = 2) ->
(x8 + 1 = 2) ->
(x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 = 2)
end
module Ce_int32
use import ref.Ref
use export mach.int.Int32
let dummy_update (r: ref int32)
requires { to_int !r = 22}
ensures {to_int !r = 42} =
r := of_int 42;
r := !r + !r;
end
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
Counter-example model:File int32.mlw:
Line 6:
r = {"type" : "Integer" , "val" : "22" }
Line 9:
r = {"type" : "Integer" ,
"val" : "42" }
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Timeout
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Timeout
ce/logic.mlw T g0: Unknown (other) (time hidden)
Counter-example model:File logic.mlw:
Line 6:
ce/int.mlw T g_no_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 5:
x = {"type" : "Integer" ,
"val" : "48" }
ce/logic.mlw T g1: Unknown (other) (time hidden)
Counter-example model:File logic.mlw:
Line 10:
ce/int.mlw T g_lab0 : Unknown (other)
Counter-example model:File int.mlw:
Line 7:
x = {"type" : "Integer" ,
"val" : "0" }
"val" : "48" }
ce/logic.mlw T g2: Unknown (other) (time hidden)
Counter-example model:File logic.mlw:
ce/int.mlw T g2_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 12:
X = {"type" : "Integer" , "val" : "1" }
x2 = {"type" : "Integer" ,
"val" : "1" }
x = {"type" : "Integer" ,
"val" : "0" }
ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
x3 = {"type" : "Integer" ,
"val" : "1" }
x4 = {"type" : "Integer" ,
......
ce/int.mlw T g_no_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 5:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g_lab0 : Unknown (other)
Counter-example model:File int.mlw:
Line 7:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g2_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 12:
x = {"type" : "Integer" ,
"val" : "1" }
ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
x3 = {"type" : "Integer" ,
"val" : "1" }
x4 = {"type" : "Integer" ,
"val" : "1" }
x5 = {"type" : "Integer" ,
"val" : "1" }
x6 = {"type" : "Integer" ,
"val" : "1" }
x7 = {"type" : "Integer" ,
"val" : "1" }
x8 = {"type" : "Integer" ,
"val" : "1" }
ce/int.mlw T g_no_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 5:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g_lab0 : Unknown (other)
Counter-example model:File int.mlw:
Line 7:
x = {"type" : "Integer" ,
"val" : "48" }
ce/int.mlw T g2_lab : Unknown (other)
Counter-example model:File int.mlw:
Line 12:
x = {"type" : "Integer" ,
"val" : "1" }
ce/int.mlw T newgoal : Unknown (other)
Counter-example model:File int.mlw:
Line 14:
x2 = {"type" : "Integer" , "val" : "1" }
x3 = {"type" : "Integer" ,
"val" : "1" }
x4 = {"type" : "Integer" ,
"val" : "1" }
x5 = {"type" : "Integer" ,
"val" : "1" }
x6 = {"type" : "Integer" ,
"val" : "1" }
x7 = {"type" : "Integer" ,
"val" : "1" }
x8 = {"type" : "Integer" ,
"val" : "1" }
......@@ -3,59 +3,59 @@ theory ModelInt
use import int.Int
(* PASS *)
goal test0 : forall x [@model]:int. not (0 < x < 1)
goal test0 : forall x:int. not (0 < x < 1)
(* CE *)
goal test1 : forall x [@model]:int. not (0 <= x <= 1)
goal test1 : forall x:int. not (0 <= x <= 1)
use import int.EuclideanDivision
(* CE *)
goal test2 : forall x [@model]:int. div x x = 1
goal test2 : forall x:int. div x x = 1
(* CE *)
goal test_overflow:
forall x [@model] y [@model] : int.
forall x y : int.
0 <= x <= 65535 /\ 0 <= y <= 65535 -> 0 <= x + y <= 65535
(* CE *)
goal test_overflow2:
forall x [@model] y [@model] : int.
forall x y : int.
-2 <= x <= 65535 /\ -2 <= y <= 65535 -> -2 <= x + y <= 65535
predicate is_int16 (x:int) = -65536 <= x <= 65535
(* CE *)
goal test_overflow_int16:
forall x [@model] y [@model] : int.
forall x y : int.
is_int16 x /\ is_int16 y -> is_int16 (x + y)
(* CE *)
goal test_overflow_int16_alt:
forall x [@model] y [@model] : int.
forall x y : int.
-65536 <= x <= 65535 /\ -65536 <= y <= 65535 -> -65536 <= x+y <= 65535
(* CE *)
goal test_overflow_int16_bis:
forall x [@model] y [@model] : int.
forall x y : int.
is_int16 x /\ is_int16 y /\
([@model] 0 <= x) /\ (x <= y) -> is_int16 (x + y)
(0 <= x) /\ (x <= y) -> is_int16 (x + y)
predicate is_int32 (x:int) = -2147483648 <= x <= 2147483647
(* CE *)
goal test_overflow_int32:
forall x [@model] y [@model] : int.
forall x y : int.
is_int32 x /\ is_int32 y -> is_int32 (x + y)
(* CE *)
goal test_overflow_int32_bis:
forall x [@model] y [@model] : int.
forall x y : int.
is_int32 x /\ is_int32 y /\ 0 <= x <= y -> is_int32 (x + y)
(* CE *)
goal test_overflow_int32_bis_inline:
forall x [@model] y [@model] : int.
forall x y : int.
-2147483648 <= x <= 2147483647 /\ -2147483648 <= y <= 2147483647 /\ 0 <= x <= y -> -2147483648 <= x + y <= 2147483647
end
ce/int_overflow.mlw ModelInt test0 : Valid
ce/int_overflow.mlw ModelInt test1 : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 9:
x = {"type" : "Integer" ,
"val" : "0" }
ce/int_overflow.mlw ModelInt test2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Timeout
ce/int_overflow.mlw ModelInt test0 : Valid
ce/int_overflow.mlw ModelInt test1 : Unknown (other)
Counter-example model:File int_overflow.mlw:
Line 9:
x = {"type" : "Integer" ,
"val" : "0" }
ce/int_overflow.mlw ModelInt test2 : Unknown (other)
ce/int_overflow.mlw ModelInt test_overflow : Timeout
ce/int_overflow.mlw ModelInt test_overflow2 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_alt : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int16_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32 : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis : Timeout
ce/int_overflow.mlw ModelInt test_overflow_int32_bis_inline : Timeout
module M
use import int.Int
use import ref.Ref
val a : ref int
let p1 (b : ref int)
requires { 0 <= !a <= 10 /\ 3 <= !b <= 17 }
ensures { 17 <= !a <= 42 }
= a := !a + !b;
assert { 5 <= !a <= 15 };
if !a >= 10 then a := !a - 1
val c : ref int
let p2 ()
requires { 0 <= !a <= 10 }
ensures { 7 <= !a <= 42 }
= c := 1;
while !c <= 10 do
invariant { 2 <= !c <= 11 }
invariant { 3 <= !a <= 10 }
variant { !c }
a := !a + !c;
c := !c + 2
done
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../jlamp0.mlw">
<theory name="M">
<goal name="WP_parameter p1" expl="VC for p1">
<transf name="split_goal_wp" >
<goal name="WP_parameter p1.0" expl="assertion">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="WP_parameter p1.1" expl="postcondition">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="WP_parameter p1.2" expl="postcondition">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
</transf>
<transf name="split_intros_goal_wp" >
<goal name="WP_parameter p1.0" expl="assertion">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="WP_parameter p1.1" expl="postcondition">
<proof prover="0"><result status="unknown" time="0.02"/></proof>
</goal>
<goal name="WP_parameter p1.2" expl="postcondition">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter p2" expl="VC for p2">
<transf name="split_goal_wp" >
<goal name="WP_parameter p2.0" expl="loop invariant init">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="WP_parameter p2.1" expl="loop invariant init">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="WP_parameter p2.2" expl="loop invariant preservation">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="WP_parameter p2.3" expl="loop invariant preservation">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="WP_parameter p2.4" expl="loop variant decrease">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="WP_parameter p2.5" expl="postcondition">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
</transf>
<transf name="split_intros_goal_wp" >
<goal name="WP_parameter p2.0" expl="loop invariant init">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="WP_parameter p2.1" expl="loop invariant init">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="WP_parameter p2.2" expl="loop invariant preservation">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="WP_parameter p2.3" expl="loop invariant preservation">
<proof prover="0"><result status="unknown" time="0.01"/></proof>
</goal>
<goal name="WP_parameter p2.4" expl="loop variant decrease">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="WP_parameter p2.5" expl="postcondition">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
ce/jlamp0.mlw M WP_parameter p1 : Unknown (other)
Counter-example model:File ref.mlw:
Line 24:
the check fails with all inputs
File jlamp0.mlw:
Line 6:
a = {"type" : "Integer" , "val" : "7" }
Line 8:
b = {"type" : "Integer" , "val" : "3" }
Line 10:
a = {"type" : "Integer" , "val" : "10" }
Line 11:
a = {"type" : "Integer" ,
"val" : "10" }
ce/jlamp0.mlw M WP_parameter p2 : Unknown (other)
Counter-example model:File ref.mlw:
Line 24:
c = {"type" : "Integer" ,
"val" : "0" }
File jlamp0.mlw:
Line 6:
a = {"type" : "Integer" , "val" : "0" }
Line 19:
a = {"type" : "Integer" , "val" : "0" }
Line 20:
c = {"type" : "Integer" , "val" : "1" }
Line 21:
a = {"type" : "Integer" , "val" : "0" }
c = {"type" : "Integer" ,
"val" : "0" }
Line 22:
the check fails with all inputs
ce/jlamp0.mlw M WP_parameter p1 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/jlamp0.mlw M WP_parameter p1 : Timeout
ce/jlamp0.mlw M WP_parameter p2 : Timeout
theory T
use import int.Int
goal g0 : forall x [@model]:int. ([@model] x >= 42) -> ([@model] x + 3 <= 50)
constant g : int
goal g1 : forall x [@model]:int. ([@model] g >= x)
goal g2 : forall x1 [@model] [@model_trace:X] x2 [@model] x3 [@model] x4 [@model] x5 [@model] x6 [@model] x7 [@model] x8 [@model].
([@model] [@model_trace: X1 + 1 = 2] x1 + 1 = 2) ->
([@model] x2 + 1 = 2) ->
([@model] x3 + 1 = 2) ->
([@model] x4 + 1 = 2) ->
([@model] x5 + 1 = 2) ->
([@model] x6 + 1 = 2) ->
([@model] x7 + 1 = 2) ->
([@model] x8 + 1 = 2) ->
([@model] x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 = 2)
end
theory ModelMap
use import map.Map
goal t1 : forall t:map int int, i : int.
get (set t 0 42) i = get t i
end
module M
use import ref.Ref
use import list.List
use import int.Int
use import ref.Ref
(**************************************
** Getting counterexamples for maps **
**************************************)
use import map.Map
let ghost test_map (ghost x : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* Multi-dimensional maps *)
let ghost test_map_multidim1 (ghost x : ref (map int (map int int))) : unit
ensures { !x[0][0] <> !x[1][1] }
=
x := Map.set !x 0 (Map.get !x 1)
let ghost test_map_multidim2 (ghost x : ref (map int (map int int))) : unit
ensures { !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
(*******************************************
** Definitions of projections used below **
*******************************************)
function projfi [@model_trace:.projfi] (l : int) : int
= l
meta "inline:no" function projfi
meta "model_projection" function projfi
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
val y [@model] [@model_trace:Y] :ref int
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 **
******************************************************)
let incr ( x23 [@model] [@model_trace:X2] : ref int ): unit
ensures { [@model_vc_post] !x23 = old !x23 + 2 + !y }
(* Both indices and range of map will be projected using
projfi, projf1, and projf2
Warning: cvc4 is not able to handle projections there *)
let ghost proj_map_test1 (ghost x [@model_projected] : ref (map int int)) : unit
ensures { !x[0] <> !x[1] }
=
(*#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#*)
y := !y + 1;
x23 := !x23 + 1;
x23 := !x23 + 1
x := Map.set !x 0 3
let test_loop ( x [@model] [@model_trace:x] : ref int ): unit
ensures { [@model_vc_post] !x < old !x }
(* No projection function for bool -> the array should be
present in counterexample as it is. *)
let ghost proj_map_test2 (ghost x [@model_projected] : ref (map int bool)) : unit
ensures { !x[0] <> !x[1] }
=
label L in
incr x;
label M in
while !x > 0 do
invariant { [@model_vc] !x > !x at L + !x at M }
variant { !x }
x := !x - 1
done
x := Map.set !x 0 true
end
ce/map.mlw M VC incr: Unknown (other) (time hidden)
Counter-example model:File map.mlw:
Line 10:
Y = {"type" : "Integer" , "val" : "0" }
Line 12:
X2 = {"type" : "Integer" ,
"val" : "0" }
Line 13:
old X2 = {"type" : "Integer" , "val" : "0" }
old Y = {"type" : "Integer" ,
"val" : "-1" }
ce/map.mlw M VC test_loop: Unknown (other) (time hidden)
Counter-example model:File map.mlw: