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/

Documentation about the inference of loop invariants using the API

parent 99b36f3b
......@@ -501,7 +501,10 @@ directly build the typed declaration. The first choice use concepts
similar to the WhyML language but errors in the generation are harder to
debug since they are lost inside the typing phase, the second choice use
more internal notions but it is easier to pinpoint the functions wrongly
used.
used. :numref:`sec.build_untyped` and :numref:`sec.build_untyped_attr`
follow choice one and :numref:`sec.build_typed` choice two.
.. _sec.build_untyped:
Untyped syntax tree
~~~~~~~~~~~~~~~~~~~
......@@ -647,6 +650,59 @@ OCaml functions that were already introduced before.
:start-after: BEGIN{checkingvcs}
:end-before: END{checkingvcs}
.. _sec.build_untyped_attr:
Use attributes to infer loop invariants
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In this section we build a module containing a let declaration with a
while loop and an attribute that triggers the inference of loop
invariants during VC generation. For more information about the
inference of loop invariants refer to :numref:`sec.installinferloop`
and :numref:`sec.runwithinferloop`. The examples shown below are
available in the file :file:`examples/use_api/mlw_tree1.ml`.
We build an environment and define the some helper functions exactly
as in :numref:`sec.build_untyped`. Additionally we create two other
helper functions as follows:
.. literalinclude:: ../examples/use_api/mlw_tree1.ml
:language: ocaml
:start-after: BEGIN{helper2}
:end-before: END{helper2}
Our goal is now to build a program equivalent to the following. Note
that the let declaration contains an attribute ``[@infer]`` which will
trigger the inference of loop invariants during VC generation (make
sure that the why3 library was compiled with support for `infer-loop`,
see :numref:`sec.installinferloop` for more information).
.. literalinclude:: ../examples/use_api/mlw_tree1.ml
:language: ocaml
:start-after: BEGIN{source1}
:end-before: END{source1}
The OCaml code that builds such a module is shown below.
.. literalinclude:: ../examples/use_api/mlw_tree1.ml
:language: ocaml
:start-after: BEGIN{code1}
:end-before: END{code1}
The debugging flags mentioned in :numref:`sec.runwithinferloop` can be
enabled using the API as follows:
.. literalinclude:: ../examples/use_api/mlw_tree1.ml
:language: ocaml
:start-after: BEGIN{flags}
:end-before: END{flags}
Finally the code for closing the modules, printing it to the standard
output, typing it, and so on is exactly the same as in the previous
section, thus we omit it in here.
.. _sec.build_typed:
Typed declaration
~~~~~~~~~~~~~~~~~
......
......@@ -46,12 +46,9 @@ let mk_expr e = { expr_desc = e; expr_loc = Loc.dummy_position }
let mk_term t = { term_desc = t; term_loc = Loc.dummy_position }
let mk_pat p = { pat_desc = p; pat_loc = Loc.dummy_position }
let pat_wild = mk_pat Pwild
let pat_var id = mk_pat (Pvar id)
let mk_var id = mk_term (Tident (Qident id))
let param0 = [Loc.dummy_position, None, false, Some (PTtuple [])]
let param1 id ty = [Loc.dummy_position, Some id, false, Some ty]
let mk_const i =
......@@ -67,7 +64,12 @@ let mk_eapp f l = mk_expr (Eidapp(f,l))
let mk_evar x = mk_expr(Eident(Qident x))
(*BEGIN{helper2}*)
(* ... *)
let pat_wild = mk_pat Pwild
let mk_ewhile e1 i v e2 = mk_expr (Ewhile (e1,i,v,e2))
(*END{helper2}*)
(* END{helper1} *)
(* declaration of
......@@ -101,33 +103,38 @@ let eq_symb = mk_qualid [Ident.op_infix "="]
let mod_M1 =
(* use int.Int *)
let use_int_Int = use_import (["int";"Int"]) in
let use_int_Int = use_import (["int";"Int"]) in
let use_ref_Refint = use_import (["ref";"Refint"]) in
(* f *)
let f =
let id_x = mk_ident "x" in
let id_x = mk_ident "x" in
let var_x = mk_var id_x in
let t_x = mk_tapp ref_access [var_x] in
let pre = mk_tapp le_int [t_x; mk_tconst 100] in
let post = mk_tapp eq_symb [t_x; mk_tconst 100] in
let spec = {
sp_pre = [pre];
sp_post = [Loc.dummy_position,[pat_wild, post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
let pre = mk_tapp le_int [t_x; mk_tconst 100] in
let post = mk_tapp eq_symb [t_x; mk_tconst 100] in
let spec = {
sp_pre = [pre];
sp_post = [Loc.dummy_position,[pat_wild, post]];
sp_xpost = [];
sp_reads = [];
sp_writes = [];
sp_alias = [];
sp_variant = [];
sp_checkrw = false;
sp_diverge = false;
sp_partial = false;
}
in
let vare_x = mk_evar id_x in
let e_x = mk_eapp ref_access [vare_x] in
let var_x = mk_evar id_x in
(* !x *)
let e_x = mk_eapp ref_access [var_x] in
(* !x < 100 *)
let while_cond = mk_eapp l_int [e_x; mk_econst 100] in
(* 100 - !x *)
let while_vari = mk_tapp minus_int [mk_tconst 100; t_x], None in
let incr = mk_eapp ref_int_incr [vare_x] in
(* incr x *)
let incr = mk_eapp ref_int_incr [var_x] in
(* while (!x < 100) do variant { 100 - !x } incr x done *)
let while_loop = mk_ewhile while_cond [] [while_vari] incr in
let f =
Efun(param1 id_x ref_int_type, None, mk_pat Pwild,
......@@ -140,6 +147,12 @@ let mod_M1 =
(mk_ident "M1",[use_int_Int; use_ref_Refint; f])
(* END{code1} *)
(*BEGIN{flags}*)
let () = Debug.set_flag Infer_cfg.infer_print_ai_result;
Debug.set_flag Infer_cfg.infer_print_cfg;
Debug.set_flag Infer_loop.print_inferred_invs
(*END{flags}*)
(* BEGIN{getmodules} *)
let mlw_file = Modules [ mod_M1 ]
(* END{getmodules} *)
......
......@@ -4,6 +4,9 @@ open Term
open Expr
open Ity
val infer_print_cfg : Debug.flag
val infer_print_ai_result : Debug.flag
module type INFERCFG = sig
module QDom : Domain.TERM_DOMAIN
......
......@@ -14,5 +14,7 @@ open Ity
open Expr
open Term
val print_inferred_invs : Debug.flag
val infer_loops : Sattr.t -> Env.env -> Decl.known_map ->
Pdecl.known_map -> expr -> cty -> (expr * term) list
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment