why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-06-20T16:19:26+02:00https://gitlab.inria.fr/why3/why3/-/issues/771Capture parsing error of sexp format2023-06-20T16:19:26+02:00Matteo ManighettiCapture parsing error of sexp formatWhen running `why3 session create` on a malformed sexp file, the following fatal error occurs:
```
Fatal error: exception (Of_sexp_error
"src/parser/ptree.ml.term_desc_of_sexp: sum tag \"Teps\" has incorrect number of arguments"
```When running `why3 session create` on a malformed sexp file, the following fatal error occurs:
```
Fatal error: exception (Of_sexp_error
"src/parser/ptree.ml.term_desc_of_sexp: sum tag \"Teps\" has incorrect number of arguments"
```https://gitlab.inria.fr/why3/why3/-/issues/770Improve precision of timings2023-06-20T13:36:30+02:00Matteo ManighettiImprove precision of timingsThis issue is twofold:
- We should increase the precision of timings, moving from millisecond to microsecond, to obtain improved stats in `why3 session info` (see also #762 )
- Alt-Ergo sometimes reports taking zero time. Also, it is the...This issue is twofold:
- We should increase the precision of timings, moving from millisecond to microsecond, to obtain improved stats in `why3 session info` (see also #762 )
- Alt-Ergo sometimes reports taking zero time. Also, it is the only prover for which the reported time is parsed instead of asking the server. This should be uniformed, possibly by using server's times for Alt-Ergo.Matteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/769RAC : Don't filter model global variables in the task2023-06-20T09:22:43+02:00BONNOT PaulRAC : Don't filter model global variables in the taskCurrently when executing the RAC, global variables are filtered from the task when they are not free in the term that is checked.
It was probably done because the generated models can assign inconsistent values to global variables, leadi...Currently when executing the RAC, global variables are filtered from the task when they are not free in the term that is checked.
It was probably done because the generated models can assign inconsistent values to global variables, leading to bad counterexamples.
However, this filter can in several cases make the counterexamples impossible to verify, therefore it should be removed.
To avert the generation of inconsistent values for global variables, the solution is to avoid having abstract declarations of such variables, as done in MR !899.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/768bad postcondition for (=) on machine integers2023-06-17T02:19:10+02:00Andrei Paskevichbad postcondition for (=) on machine integersWhen the first postcondition of `(=) x y` is different from `{ result <-> x = y }`, Why3 cannot convert program expression `x = y` into a logical formula `x = y`, which breaks, e.g., anonymous functions using `(=)` on bounded integers.
...When the first postcondition of `(=) x y` is different from `{ result <-> x = y }`, Why3 cannot convert program expression `x = y` into a logical formula `x = y`, which breaks, e.g., anonymous functions using `(=)` on bounded integers.
See MR !900 (in progress, several sessions still need fixing).https://gitlab.inria.fr/why3/why3/-/issues/766Why3 session create : don't abort when output directory exists but not the se...2023-06-06T08:30:19+02:00BONNOT PaulWhy3 session create : don't abort when output directory exists but not the session filesBONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/764Add the option "--add-provers" to why3 session update2023-06-06T10:13:26+02:00BONNOT PaulAdd the option "--add-provers" to why3 session updateAn example usage :
```why3 session update --add-provers <p1:p2...> <session_dir>```
This would add the prover in the session, and would generate a new proof attempt node for the specified provers for each proof node of the session.An example usage :
```why3 session update --add-provers <p1:p2...> <session_dir>```
This would add the prover in the session, and would generate a new proof attempt node for the specified provers for each proof node of the session.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/763Add a command "why3 bench"2023-06-05T15:01:01+02:00BONNOT PaulAdd a command "why3 bench"Add a subcommand "why3 session create <file...> -P <prover...>" that does the following :
- Creates a new session with all the files specified
- applies for each file the transformation "split_vc" in the session
- for each proof node ge...Add a subcommand "why3 session create <file...> -P <prover...>" that does the following :
- Creates a new session with all the files specified
- applies for each file the transformation "split_vc" in the session
- for each proof node generated by "split_vc" add a proof attempt for each specified prover
- save the session without calling any prover
Also add a command "why3 bench <session-dir>" that plays all proof nodes in a session that have not been attempted. As it is supposed to be called on large sessions, it should save the session every minute. This way one could interrupt a bench then resume it later.
The combination of the 2 commands can be used to generate sessions for batch of files and then gather statistics.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/761Attributes in variant clause with custom order are lost2023-05-23T14:31:51+02:00Guillaume CluzelAttributes in variant clause with custom order are lostThis issue is a follow-up on #587.
```
use int.Int
predicate my_order (x y : int) =
x < y /\ x >= 0
use export why3.WellFounded.WellFounded
lemma my_order_wf : well_founded my_order
meta "vc:proved_wf" predicate my_order, lemma my_o...This issue is a follow-up on #587.
```
use int.Int
predicate my_order (x y : int) =
x < y /\ x >= 0
use export why3.WellFounded.WellFounded
lemma my_order_wf : well_founded my_order
meta "vc:proved_wf" predicate my_order, lemma my_order_wf
let rec f () =
let ref x = 10 in
while x > 0 do
variant { [@variant:x] x with my_order }
x <- x - 1
done
```
In this case, the goal generated for the VC corresponding to the variant clause is does not contains the attributes `[@variant:x]` as shown above:
```
goal f'vc [@expl:VC for f] :
[@vc:annotation] [@expl:loop variant decrease]
my_order ([@hyp_name:Variant] [@variant:x] x)
([@hyp_name:Variant] [@variant:x] x1)
```Guillaume CluzelGuillaume Cluzelhttps://gitlab.inria.fr/why3/why3/-/issues/760Error when using a custom order in variant clause2023-06-27T09:48:25+02:00Guillaume CluzelError when using a custom order in variant clause```
use int.Int
predicate my_order (x y : int) =
x < y /\ x >= 0
let rec f () =
let ref x = 10 in
while x > 0 do
variant { [@variant:x] x with my_order }
x <- x - 1
done
```
With `why3 prove variant.mlw` I get the erro...```
use int.Int
predicate my_order (x y : int) =
x < y /\ x >= 0
let rec f () =
let ref x = 10 in
while x > 0 do
variant { [@variant:x] x with my_order }
x <- x - 1
done
```
With `why3 prove variant.mlw` I get the error:
```
File "variant.mlw", line 6, character 0 to line 11, character 6:
Ident (->) is not yet declared
```
This comes from one of the MRs (probably why3/why3!736 but I didn't test) that changed how VCs for variant are generated.https://gitlab.inria.fr/why3/why3/-/issues/757Add option to hide task comments in the IDE2023-05-26T14:16:31+02:00BONNOT PaulAdd option to hide task comments in the IDEIn the task panel of the IDE, comments are displayed showing where the task declarations come from.
The comments can be too noisy especially for cloning, we should have an option to hide them.In the task panel of the IDE, comments are displayed showing where the task declarations come from.
The comments can be too noisy especially for cloning, we should have an option to hide them.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/756Add support for epsilon in Ptree2023-05-15T11:52:05+02:00BONNOT PaulAdd support for epsilon in PtreeBONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/755Delete useless algebra lemmas for CVCx and Z32023-06-15T17:18:49+02:00BONNOT PaulDelete useless algebra lemmas for CVCx and Z3The lemmas of `algebra.Field` as well as `CompatOrderMult` are passed to CVCx and Z3. They shouldn't be since they are already known by the provers and in the case of Z3 it seems that they make other things harder to prover.
They need t...The lemmas of `algebra.Field` as well as `CompatOrderMult` are passed to CVCx and Z3. They shouldn't be since they are already known by the provers and in the case of Z3 it seems that they make other things harder to prover.
They need to be removed in the drivers of these provers.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/749Why3doc is too fragile in presence of multiple files2023-04-04T09:43:26+02:00Guillaume MelquiondWhy3doc is too fragile in presence of multiple filesConsider a command line `why3 doc -L . ./foo.mlw ./bar.mlw` and assume that `bar.mlw` depends on a theory `foo.Foo` (hence the need for `-L .`). Why3 first reads `./foo.mlw` in isolation; that is fine. Then it reads `./bar.mlw`, which de...Consider a command line `why3 doc -L . ./foo.mlw ./bar.mlw` and assume that `bar.mlw` depends on a theory `foo.Foo` (hence the need for `-L .`). Why3 first reads `./foo.mlw` in isolation; that is fine. Then it reads `./bar.mlw`, which depends on `./foo.mlw` (and it is exactly `./foo.mlw` due to `-L .`). So, Why3 also loads `foo` as a library. But it has already registered tons of definitions in `./foo.mlw`, so all the definition of `foo.Foo` are dropped. As a consequence, any use of a symbol of `foo.Foo` in `bar.mlw` will be assumed to be from the current file, since that is what `foo.mlw` was at the time it was first parsed. All the corresponding links are thus broken.
There are two potential workarounds:
1. Make sure the files are in syntactically different locations, e.g., `why3 doc -L . foo.mlw bar.mlw`.
2. Make sure the files are documented after they have been already used once, e.g., `why3 doc -L . ./bar.mlw ./foo.mlw`.
This breaks hundreds of links in the documentation of Why3's standard library. Workaround 1 will be used there. But this still needs to be fixed properly.https://gitlab.inria.fr/why3/why3/-/issues/748Confusing type error message2023-04-08T19:07:56+02:00Paul PataultConfusing type error messageThe following code
```ocaml
let g = if true then 1
```
produces the error
```
This expression has type (), but is expected to have type int
```
while one could except the opposite as OCaml does:
```
Error: This expression has type int bu...The following code
```ocaml
let g = if true then 1
```
produces the error
```
This expression has type (), but is expected to have type int
```
while one could except the opposite as OCaml does:
```
Error: This expression has type int but an expression was expected of type
unit because it is in the result of a conditional with no else branch
```Jean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/742Attributes before a `let` in a formula are lost2023-04-30T11:09:27+02:00Guillaume CluzelAttributes before a `let` in a formula are lostConsidering the following program
```
let f (ref x : int) : unit
ensures { [@xxxx] [@expl:foo] let a = x in a = 0 }
= x <- 0
```
I would expect to see the attribute `[@expl:foo]` and `[@xxxx]` in the VC that correspond to the goal fo...Considering the following program
```
let f (ref x : int) : unit
ensures { [@xxxx] [@expl:foo] let a = x in a = 0 }
= x <- 0
```
I would expect to see the attribute `[@expl:foo]` and `[@xxxx]` in the VC that correspond to the goal for the ensures. But only the attribute `[@expl:foo]` is kept, the other is lost during the generation of VC as show by the verbatim:
```
goal f'vc [@expl:VC for f] : [@hyp_name:Ensures] [@expl:foo] x = 0
```
It would be better to treat those attributes as the expl ones.https://gitlab.inria.fr/why3/why3/-/issues/737Support millisecond time limits for provers2023-03-07T15:49:04+01:00Xavier DenisSupport millisecond time limits for proversIt would be nice to support strategies that run provers for fractions of a second (like run Alt-Ergo for 0.1s), but this requires generalizing the current timelimit supports and add support for printing different time limit formats for r...It would be nice to support strategies that run provers for fractions of a second (like run Alt-Ergo for 0.1s), but this requires generalizing the current timelimit supports and add support for printing different time limit formats for relevant provers (milliseconds and fractional seconds).https://gitlab.inria.fr/why3/why3/-/issues/725Printer for SMTv2 is broken when using projections of sum types in a non-poly...2023-01-09T14:29:53+01:00Jacques-Henri JourdanPrinter for SMTv2 is broken when using projections of sum types in a non-polymorphic contextWhy3 script:
```
type t =
| A (x : unit)
| B (x : unit)
goal g: forall x:t. x = x
```
When using CVC4, CVC4 complains:
```
(error "Parse Error: x already declared in this datatype")
```
And indeed, the generated SMTLIB type declar...Why3 script:
```
type t =
| A (x : unit)
| B (x : unit)
goal g: forall x:t. x = x
```
When using CVC4, CVC4 complains:
```
(error "Parse Error: x already declared in this datatype")
```
And indeed, the generated SMTLIB type declaration is:
```
(declare-datatypes ((t 0))
(((A (x tuple0)) (B (x tuple0)))))
```
The problem is that the printer for SMTLIB considers that Why3 projections (well-defined, projection has to be repeated in every constructor) have the same semantics than in SMTLIB (defined only if passed the right constructor, projection needs to be unique in the whole SMTLIB type declaration).
This issue does not occur when
- the goal is polymorphic, because algebraic types are eliminated
- using records, because there is only one constructor.
Also, the FIXME comment [here](https://gitlab.inria.fr/why3/why3/-/blob/master/src/printer/smtv2.ml#L810) is related.https://gitlab.inria.fr/why3/why3/-/issues/721Taking the first model element matching an id and a loc is inaccurate2023-07-10T09:16:04+02:00MOREAU SoleneTaking the first model element matching an id and a loc is inaccurateThis ticket comes from investigating a "bad counterexample" classification on a simple test file in SPARK: [main.adb](/uploads/44737dd2eab31ff8054e9adf2c7fad06/main.adb)
This SPARK test contains on a single line `X := 0; SetX(2);`. The ...This ticket comes from investigating a "bad counterexample" classification on a simple test file in SPARK: [main.adb](/uploads/44737dd2eab31ff8054e9adf2c7fad06/main.adb)
This SPARK test contains on a single line `X := 0; SetX(2);`. The model returned by the prover contains two different values for `X` at this line: `X = 0` for the first part, and `X = 4` for the second part which is a "good" value to show the assertion failure (since `X = 4` satisfies the postcondition of `SetX`).
But the giant-step RAC takes the value `X = 0` when trying to evaluate the postcondition of `SetX`.
This problem does not happen if the affectation and the call to `SetX` are split in 2 different lines.
The bug seems to come from `Model_parser.search_model_element_for_id`, which assumes that an id and a loc are enough to find the correct value for the oracle.
I have minimized the `.mlw` generated by SPARK to reproduce the above problem with Why3:
- reproducer file: [same_loc.mlw](/uploads/8de92397fb676547777008d5b7520e68/same_loc.mlw)
- Why3 command: `why3 prove -P "CVC5,1.0.0,counterexamples" --check-ce --rac-prover="CVC5,1.0.0" ~/Work/WIP/same_loc.mlw --debug=vc_sp`
This is not urgent for SPARK since there is a workaround (splitting in different lines). @marche it reminds me of what we discussed this week about filtering duplicated elements in models, so I guess it is worth having a look at it.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/718Remove cannot locate symbols2022-12-02T19:19:49+01:00Guillaume MelquiondRemove cannot locate symbolsCreate a session as follows: Load the following file; apply `split_vc` on the verification condition; run Alt-Ergo (or any other prover) on the resulting goal; run a bisection on the proof attempt.
```whyml
use int.Int
let f (x : int) en...Create a session as follows: Load the following file; apply `split_vc` on the verification condition; run Alt-Ergo (or any other prover) on the resulting goal; run a bisection on the proof attempt.
```whyml
use int.Int
let f (x : int) ensures { result = 2 * x } = x + x
```
The original task contains a useless declaration `constant (+)'result'unused : int = result`, which is properly detected as such by the bisection. Thus, it adds a node for the `remove` transformation to the session, so as to discard this declaration. The transformation, however, fails to locate that symbol, thus complaining: `Symbol '(+)'result'unused' not found, ignored`. The symbol is still present in the final task.
This issue is responsible for hundreds of warning in the `multiprecision/mpz_sub` example.https://gitlab.inria.fr/why3/why3/-/issues/717Error when checking floating point literal2022-12-12T14:30:25+01:00MOREAU SoleneError when checking floating point literalThe error `Invalid floating point literal` is raised when trying to create a Why3 term corresponding to the following floating point constants:
- `0x0.000002p-127`
- `0x0.0000000000001p-1023`
Reproducer file: [bug_float.mlw](/uploads/b9...The error `Invalid floating point literal` is raised when trying to create a Why3 term corresponding to the following floating point constants:
- `0x0.000002p-127`
- `0x0.0000000000001p-1023`
Reproducer file: [bug_float.mlw](/uploads/b936362c71012790634e2de474980217/bug_float.mlw)MARCHE ClaudeMARCHE Claude