Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 4c99984c authored by Leon Gondelman's avatar Leon Gondelman

Merge branch 'coercions' into new_system

parents d4c766eb db0d6501
...@@ -169,7 +169,7 @@ LIB_UTIL = config bigInt util opt lists strings \ ...@@ -169,7 +169,7 @@ LIB_UTIL = config bigInt util opt lists strings \
hashcons stdlib exn_printer pp json debug loc lexlib print_tree \ hashcons stdlib exn_printer pp json debug loc lexlib print_tree \
cmdline warning sysutil rc plugin bigInt number pqueue cmdline warning sysutil rc plugin bigInt number pqueue
LIB_CORE = ident ty term pattern decl theory \ LIB_CORE = ident ty term pattern decl coercion theory \
task pretty dterm env trans printer model_parser task pretty dterm env trans printer model_parser
LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \ LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \
...@@ -1748,7 +1748,7 @@ MODULESTODOC = \ ...@@ -1748,7 +1748,7 @@ MODULESTODOC = \
util/util util/opt util/lists util/strings \ util/util util/opt util/lists util/strings \
util/extmap util/extset util/exthtbl \ util/extmap util/extset util/exthtbl \
util/weakhtbl util/stdlib util/rc util/debug \ util/weakhtbl util/stdlib util/rc util/debug \
core/ident core/ty core/term core/decl core/theory \ core/ident core/ty core/term core/decl core/coercion core/theory \
core/env core/task \ core/env core/task \
driver/whyconf driver/call_provers driver/driver \ driver/whyconf driver/call_provers driver/driver \
session/session session/session_tools session/session_scheduler session/session session/session_tools session/session_scheduler
......
type a
type b
type c
function b_to_c b : c
meta coercion function b_to_c
function a_to_b a : b
meta coercion function a_to_b
function a_to_c a : c
meta coercion function a_to_c
type a
type b
function f a : b
meta coercion function f
function g a : b
meta coercion function g
type a
type b
type c
function f a : c
meta coercion function f
function g b : c
meta coercion function g
function h a : b
meta coercion function h
type a
type b
function f a : b
meta coercion function f
function g b : a
meta coercion function g
type a
type b
type c
function f a : b
meta coercion function f
function g b : c
meta coercion function g
function h c : a
meta coercion function h
type a
type b
type c
function g b : c
meta coercion function g
function f a : b
meta coercion function f
function h c : a
meta coercion function h
type t
function f t : int
meta coercion function f
goal G: forall x: t. 42 = x
type a
type b
type c
function b_to_c b : c
meta coercion function b_to_c
function a_to_b a : b
meta coercion function a_to_b
predicate is_c c
goal G2: forall x: a. is_c x
function is_zero int : bool
meta coercion function is_zero
goal G3: if 42 then 1=2 else 3=4
...@@ -18,7 +18,7 @@ module Heap ...@@ -18,7 +18,7 @@ module Heap
type heap type heap
function size heap : int val function size heap : int
function occ elt heap : int function occ elt heap : int
...@@ -39,9 +39,6 @@ module Heap ...@@ -39,9 +39,6 @@ module Heap
val is_empty (h: heap) : bool val is_empty (h: heap) : bool
ensures { result <-> size h = 0 } ensures { result <-> size h = 0 }
val size (h: heap) : int
ensures { result = size h }
val merge (h1 h2: heap) : heap val merge (h1 h2: heap) : heap
ensures { forall x. occ x result = occ x h1 + occ x h2 } ensures { forall x. occ x result = occ x h1 + occ x h2 }
ensures { size result = size h1 + size h2 } ensures { size result = size h1 + size h2 }
...@@ -74,7 +71,7 @@ module Size ...@@ -74,7 +71,7 @@ module Size
use import TreeRank use import TreeRank
use import int.Int use import int.Int
function size (t: tree 'a) : int = match t with let rec function size (t: tree 'a) : int = match t with
| E -> 0 | E -> 0
| N _ l _ r -> 1 + size l + size r | N _ l _ r -> 1 + size l + size r
end end
...@@ -105,7 +102,7 @@ end ...@@ -105,7 +102,7 @@ end
module LeftistHeap module LeftistHeap
type elt type elt
predicate le elt elt val predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le clone relations.TotalPreOrder with type t = elt, predicate rel = le
use import TreeRank use import TreeRank
...@@ -117,7 +114,7 @@ module LeftistHeap ...@@ -117,7 +114,7 @@ module LeftistHeap
type t = tree elt type t = tree elt
(* [e] is no greater than the root of [h], if any *) (* [e] is no greater than the root of [h], if any *)
predicate le_root (e: elt) (h: t) = match h with let predicate le_root (e: elt) (h: t) = match h with
| E -> true | E -> true
| N _ _ x _ -> le e x | N _ _ x _ -> le e x
end end
...@@ -144,8 +141,8 @@ module LeftistHeap ...@@ -144,8 +141,8 @@ module LeftistHeap
= match h with = match h with
| E -> absurd | E -> absurd
| N _ l _ r -> | N _ l _ r ->
if l <> E then root_is_miminum l; match l with E -> root_is_miminum l | _ -> () end;
if r <> E then root_is_miminum r match r with E -> root_is_miminum r | _ -> () end
end end
function rank (h: t) : int = match h with function rank (h: t) : int = match h with
...@@ -172,11 +169,7 @@ module LeftistHeap ...@@ -172,11 +169,7 @@ module LeftistHeap
let is_empty (h: t) : bool let is_empty (h: t) : bool
ensures { result <-> size h = 0 } ensures { result <-> size h = 0 }
= h = E = match h with E -> true | N _ _ _ _ -> false end
let size (h: t) : int
ensures { result = size h }
= size h
let rank (h: t) : int let rank (h: t) : int
requires { leftist_heap h } requires { leftist_heap h }
......
...@@ -155,19 +155,19 @@ module NQueens63 ...@@ -155,19 +155,19 @@ module NQueens63
predicate is_board (board: array int63) (pos: int) = predicate is_board (board: array int63) (pos: int) =
forall q: int. 0 <= q < pos -> forall q: int. 0 <= q < pos ->
0 <= to_int board[q] < to_int (length board) 0 <= board[q] < (length board)
exception MInconsistent exception MInconsistent
let check_is_consistent (board: array int63) (pos: int63) let check_is_consistent (board: array int63) (pos: int63)
requires { 0 <= to_int pos < to_int (length board) } requires { 0 <= pos < (length board) }
requires { is_board board (to_int pos + 1) } requires { is_board board (pos + 1) }
= try = try
let q = ref (of_int 0) in let q = ref (of_int 0) in
while !q < pos do while !q < pos do
invariant { 0 <= to_int !q <= to_int pos } invariant { 0 <= !q <= pos }
invariant { is_board board (to_int pos + 1) } invariant { is_board board (pos + 1) }
variant { to_int pos - to_int !q } variant { pos - !q }
let bq = board[!q] in let bq = board[!q] in
let bpos = board[pos] in let bpos = board[pos] in
if bq = bpos then raise MInconsistent; if bq = bpos then raise MInconsistent;
...@@ -184,20 +184,20 @@ module NQueens63 ...@@ -184,20 +184,20 @@ module NQueens63
let rec count_bt_queens let rec count_bt_queens
(solutions: ref P.t) (board: array int63) (n: int63) (pos: int63) (solutions: ref P.t) (board: array int63) (n: int63) (pos: int63)
requires { to_int (length board) = to_int n } requires { (length board) = n }
requires { 0 <= to_int pos <= to_int n } requires { 0 <= pos <= n }
requires { is_board board (to_int pos) } requires { is_board board (pos) }
variant { to_int n - to_int pos } variant { n - pos }
ensures { is_board board (to_int pos) } ensures { is_board board (pos) }
= =
if eq pos n then if eq pos n then
solutions := P.succ !solutions solutions := P.succ !solutions
else else
let i = ref (of_int 0) in let i = ref (of_int 0) in
while !i < n do while !i < n do
invariant { 0 <= to_int !i <= to_int n } invariant { 0 <= !i <= n }
invariant { is_board board (to_int pos) } invariant { is_board board (pos) }
variant { to_int n - to_int !i } variant { n - !i }
board[pos] <- !i; board[pos] <- !i;
if check_is_consistent board pos then if check_is_consistent board pos then
count_bt_queens solutions board n (pos + of_int 1); count_bt_queens solutions board n (pos + of_int 1);
...@@ -205,7 +205,7 @@ module NQueens63 ...@@ -205,7 +205,7 @@ module NQueens63
done done
let count_queens (n: int63) : P.t let count_queens (n: int63) : P.t
requires { to_int n >= 0 } requires { n >= 0 }
ensures { true } ensures { true }
= =
let solutions = ref (P.zero ()) in let solutions = ref (P.zero ()) in
......
...@@ -2,147 +2,97 @@ ...@@ -2,147 +2,97 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="20" steplimit="0" memlimit="0"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="3.2" timelimit="8" steplimit="0" memlimit="1000"/> <prover id="3" name="Z3" version="3.2" timelimit="8" steplimit="0" memlimit="1000"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../vstte10_queens.mlw" expanded="true"> <file name="../vstte10_queens.mlw" expanded="true">
<theory name="NQueens" sum="bd54a466f42b418faffacb9470dabda3" expanded="true"> <theory name="NQueens" sum="409b3951ae957384bbb25de0839f6b15" expanded="true">
<goal name="eq_board_set"> <goal name="eq_board_set">
<proof prover="6" timelimit="5"><result status="valid" time="0.00" steps="7"/></proof> <proof prover="4"><result status="valid" time="0.00" steps="12"/></proof>
</goal> </goal>
<goal name="eq_board_sym"> <goal name="eq_board_sym">
<proof prover="6" timelimit="20" memlimit="0"><result status="valid" time="0.01" steps="7"/></proof> <proof prover="4" timelimit="20" memlimit="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal> </goal>
<goal name="eq_board_trans"> <goal name="eq_board_trans">
<proof prover="6" timelimit="20" memlimit="0"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="4" timelimit="20" memlimit="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="eq_board_extension"> <goal name="eq_board_extension">
<proof prover="6" timelimit="20" memlimit="0"><result status="valid" time="0.01" steps="10"/></proof> <proof prover="4" timelimit="20" memlimit="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="consistent_row_eq"> <goal name="consistent_row_eq">
<proof prover="6" timelimit="20" memlimit="0"><result status="valid" time="0.06" steps="37"/></proof> <proof prover="4" timelimit="20" memlimit="0"><result status="valid" time="0.06" steps="32"/></proof>
</goal> </goal>
<goal name="WP_parameter check_is_consistent" expl="VC for check_is_consistent"> <goal name="VC check_is_consistent" expl="VC for check_is_consistent" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="62"/></proof>
</goal> </goal>
<goal name="solution_eq_board"> <goal name="solution_eq_board">
<proof prover="3"><result status="valid" time="0.06"/></proof> <proof prover="3"><result status="valid" time="0.06"/></proof>
</goal> </goal>
<goal name="WP_parameter bt_queens" expl="VC for bt_queens"> <goal name="VC bt_queens" expl="VC for bt_queens" expanded="true">
<proof prover="1"><result status="valid" time="1.42"/></proof> <transf name="split_goal_wp" expanded="true">
</goal> <goal name="VC bt_queens.1" expl="1. exceptional postcondition">
<goal name="WP_parameter queens" expl="VC for queens"> <proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="6" timelimit="20" memlimit="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter test8" expl="VC for test8">
<proof prover="6" timelimit="5"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens" expl="VC for count_bt_queens">
<proof prover="0" timelimit="5" memlimit="4000"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="WP_parameter count_queens" expl="VC for count_queens">
<proof prover="6"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter test_count_8" expl="VC for test_count_8">
<proof prover="6"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
</theory>
<theory name="NQueens63" sum="f2313c3331066814cd7f4f7313021e3c" expanded="true">
<goal name="WP_parameter check_is_consistent" expl="VC for check_is_consistent">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens" expl="VC for count_bt_queens">
<transf name="split_goal_wp">
<goal name="WP_parameter count_bt_queens.1" expl="1. postcondition">
<proof prover="6"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.2" expl="2. integer overflow">
<proof prover="6"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.3" expl="3. loop invariant init">
<proof prover="6"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.4" expl="4. loop invariant init">
<proof prover="6"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.5" expl="5. type invariant">
<proof prover="6"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.6" expl="6. index in array63 bounds">
<proof prover="6"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.7" expl="7. precondition">
<proof prover="6"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.8" expl="8. precondition">
<proof prover="6"><result status="valid" time="0.17" steps="115"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.9" expl="9. integer overflow">
<proof prover="6"><result status="valid" time="0.02" steps="21"/></proof>
</goal> </goal>
<goal name="WP_parameter count_bt_queens.10" expl="10. integer overflow"> <goal name="VC bt_queens.2" expl="2. loop bounds">
<proof prover="6"><result status="valid" time="0.04" steps="48"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
</goal> </goal>
<goal name="WP_parameter count_bt_queens.11" expl="11. variant decrease"> <goal name="VC bt_queens.3" expl="3. loop invariant init">
<proof prover="6"><result status="valid" time="0.02" steps="22"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
</goal> </goal>
<goal name="WP_parameter count_bt_queens.12" expl="12. precondition"> <goal name="VC bt_queens.4" expl="4. index in array bounds">
<proof prover="6"><result status="valid" time="0.02" steps="22"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter count_bt_queens.13" expl="13. precondition"> <goal name="VC bt_queens.5" expl="5. precondition">
<proof prover="6"><result status="valid" time="0.02" steps="22"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter count_bt_queens.14" expl="14. precondition"> <goal name="VC bt_queens.6" expl="6. variant decrease">
<proof prover="0"><result status="valid" time="0.05"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="13"/></proof>
<proof prover="6"><result status="valid" time="0.00" steps="22"/></proof>
</goal> </goal>
<goal name="WP_parameter count_bt_queens.15" expl="15. integer overflow"> <goal name="VC bt_queens.7" expl="7. precondition">
<proof prover="6"><result status="valid" time="0.02" steps="26"/></proof> <proof prover="0"><result status="valid" time="0.16"/></proof>
</goal> </goal>
<goal name="WP_parameter count_bt_queens.16" expl="16. integer overflow"> <goal name="VC bt_queens.8" expl="8. loop invariant preservation">
<proof prover="6"><result status="valid" time="0.13" steps="62"/></proof> <proof prover="4"><result status="valid" time="0.06" steps="236"/></proof>
</goal> </goal>
<goal name="WP_parameter count_bt_queens.17" expl="17. loop invariant preservation"> <goal name="VC bt_queens.9" expl="9. exceptional postcondition">
<proof prover="6"><result status="valid" time="0.02" steps="30"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="15"/></proof>
</goal> </goal>
<goal name="WP_parameter count_bt_queens.18" expl="18. loop invariant preservation"> <goal name="VC bt_queens.10" expl="10. loop invariant preservation">
<proof prover="6"><result status="valid" time="0.02" steps="58"/></proof> <proof prover="4"><result status="valid" time="0.51" steps="895"/></proof>
</goal> </goal>
<goal name="WP_parameter count_bt_queens.19" expl="19. loop variant decrease"> <goal name="VC bt_queens.11" expl="11. postcondition">
<proof prover="6"><result status="valid" time="0.02" steps="30"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.20" expl="20. integer overflow">
<proof prover="6"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.21" expl="21. integer overflow">
<proof prover="6"><result status="valid" time="0.02" steps="48"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.22" expl="22. loop invariant preservation">
<proof prover="6"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.23" expl="23. loop invariant preservation">
<proof prover="6"><result status="valid" time="0.11" steps="46"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.24" expl="24. loop variant decrease">
<proof prover="6"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.25" expl="25. type invariant">
<proof prover="0"><result status="valid" time="0.05"/></proof>
<proof prover="6"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter count_bt_queens.26" expl="26. postcondition">
<proof prover="6"><result status="valid" time="0.01" steps="14"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter count_queens" expl="VC for count_queens"> <goal name="VC queens" expl="VC for queens" expanded="true">
<proof prover="6"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="4"><result status="valid" time="0.00" steps="24"/></proof>
</goal>
<goal name="VC test8" expl="VC for test8" expanded="true">
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC count_bt_queens" expl="VC for count_bt_queens" expanded="true">
<proof prover="4"><result status="valid" time="1.26" steps="438"/></proof>
</goal>
<goal name="VC count_queens" expl="VC for count_queens" expanded="true">
<proof prover="4"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC test_count_8" expl="VC for test_count_8" expanded="true">
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
</theory>
<theory name="NQueens63" sum="8c5fcf08811dad3a40f6c343ffc3660e" expanded="true">
<goal name="VC check_is_consistent" expl="VC for check_is_consistent" expanded="true">
<proof prover="4"><result status="valid" time="0.09" steps="287"/></proof>
</goal>
<goal name="VC count_bt_queens" expl="VC for count_bt_queens" expanded="true">
<proof prover="4"><result status="valid" time="0.32" steps="1264"/></proof>
</goal>
<goal name="VC count_queens" expl="VC for count_queens" expanded="true">
<proof prover="4"><result status="valid" time="0.01" steps="11"/></proof>
</goal> </goal>
<goal name="WP_parameter test_count_8" expl="VC for test_count_8"> <goal name="VC test_count_8" expl="VC for test_count_8" expanded="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="6"><result status="valid" time="0.00" steps="2"/></proof>
</goal> </goal>
</theory> </theory>
</file> </file>
......
...@@ -45,6 +45,7 @@ module Bounded_int ...@@ -45,6 +45,7 @@ module Bounded_int
constant max : int constant max : int
val function to_int (n:t) : int val function to_int (n:t) : int
meta coercion function to_int
predicate in_bounds (n:int) = min <= n <= max predicate in_bounds (n:int) = min <= n <= max
......
open Ident
open Ty
open Term
type coercion_kind =
| CRCleaf of lsymbol
| CRCcomp of coercion_kind * coercion_kind
type coercion = {
crc_kind: coercion_kind;
crc_src : Ty.tysymbol;
crc_tar : Ty.tysymbol;
crc_len : int;
}
type t = (coercion Mts.t) Mts.t
(** invariant: transitively closed *)
let empty = Mts.empty
exception NotACoercion of lsymbol
exception CoercionCycle of coercion
exception CoercionAlreadyDefined of coercion
let create_crc ls =
match ls.ls_args, ls.ls_value with
| [{ty_node = Tyapp (ty1,_)}], Some {ty_node = Tyapp (ty2,_)} ->
if ts_equal ty1 ty2 then raise (NotACoercion ls);
{ crc_kind = CRCleaf ls; crc_src = ty1; crc_tar = ty2; crc_len = 1 }
| _ -> raise (NotACoercion ls)
let mem crcmap ts1 ts2 =
try let m = Mts.find ts1 crcmap in Mts.mem ts2 m
with Not_found -> false
let find crcmap ts1 ts2 =
Mts.find ts2 (Mts.find ts1 crcmap)
(* replace an old coercion by a new one, or fail *)
let replace c_old c_new _m1 m =
match c_old.crc_kind, c_new.crc_kind with
| CRCleaf ls_old, CRCleaf ls_new when ls_equal ls_old ls_new -> m
| _ -> raise (CoercionAlreadyDefined c_old)
(* add a new coercion c, without making the transitive closure *)
let insert crc m =
let put crc m1 m2 = Mts.add crc.crc_src (Mts.add crc.crc_tar crc m1) m2 in