why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-06-15T17:18:49+02:00https://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/753Typing error in smt generated for CVC4/cvc5 with range types2023-05-16T11:24:06+02:00Guillaume CluzelTyping error in smt generated for CVC4/cvc5 with range typesConsider this simple example:
```
module Main_module
type t = < range 0 1 >
type s = { c3 : t }
let f (s0 : s) : int
requires { s0 = { c3 = (0 : t) } }
ensures { true }
= 1
end
```
If I run `why3 prove xxx.mlw -a spli...Consider this simple example:
```
module Main_module
type t = < range 0 1 >
type s = { c3 : t }
let f (s0 : s) : int
requires { s0 = { c3 = (0 : t) } }
ensures { true }
= 1
end
```
If I run `why3 prove xxx.mlw -a split_vc -P cvc4`, CVC4 complains about a typing error on subexpressions. The same problem exists when running cvc5.
I bisected and I found the problematic commit: b1290b921c724ff957a1913e433046c1c4897fa2. It is related to the remove_unused transformation.
cc @marche who wrote this commit.1.6.1MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/752Split VC : Bad session ITP ID2023-07-19T12:09:04+02:00BONNOT PaulSplit VC : Bad session ITP IDWhen performing twice a split_vc on a task in Why3 IDE, trying to delete the 2 splits causes the error :
```
There was an unrecoverable error during treatment of request:
get task(108,true,true)
with exception:
anomaly: Why3.Session_i...When performing twice a split_vc on a task in Why3 IDE, trying to delete the 2 splits causes the error :
```
There was an unrecoverable error during treatment of request:
get task(108,true,true)
with exception:
anomaly: Why3.Session_itp.BadID
```1.7.0BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/750ide should not display the interrupted status as a bomb2023-04-06T17:18:58+02:00MARCHE Claudeide should not display the interrupted status as a bombanother icon should be usedanother icon should be used1.7.0MARCHE ClaudeMARCHE Claudehttps://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/746split_vc fails for Z32023-03-28T11:01:01+02:00Gérald Pointsplit_vc fails for Z3Hi,
``why3prove`` seems to have problems to apply the transformation ``split_vc`` for Z3.
The attached file contains two modules, ``M1`` and ``M2``, that only differ in the order of declaration of two functions. When I execute ``prove...Hi,
``why3prove`` seems to have problems to apply the transformation ``split_vc`` for Z3.
The attached file contains two modules, ``M1`` and ``M2``, that only differ in the order of declaration of two functions. When I execute ``prove`` on M1 the program fail to generate vc files:
```
$ why3 prove -P z3 -a split_vc -o tmp bugz3.mlw -T M1
Failure in transformation encoding_smt_if_poly
Failure in transformation enco_poly:guards
Ident seq is not yet declared
```
[bugz3.mlw](/uploads/8361d79dea9c576c0bc841fbff270929/bugz3.mlw)1.6.1https://gitlab.inria.fr/why3/why3/-/issues/744Resurrect extraction of `prover`2023-03-23T09:21:27+01:00MARCHE ClaudeResurrect extraction of `prover`The code in `examples/prover` is supposed to be extractable to OCaml. However its extraction is not tested by the bench. Even worse, its extraction currently triggers an unexpected error:
```
cd examples/prover
make BENCH=yes
why3 -L . -...The code in `examples/prover` is supposed to be extractable to OCaml. However its extraction is not tested by the bench. Even worse, its extraction currently triggers an unexpected error:
```
cd examples/prover
make BENCH=yes
why3 -L . --debug=ignore_unused_vars extract -D ocaml64 -o prover.ml ProverTest.mlw
File "./Unification.mlw", line 887, character 8 to line 929, character 13:
Compiler error: tuple <> unification_return()
```1.6.1Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/743relative paths in extra config files2023-09-06T13:42:51+02:00MARCHE Clauderelative paths in extra config filesExtra config file (given by `--extra-config`) may contain paths, to extra driver files for example. When these are relative, they are search in the current dir and in the why3 share directory. They should be search also in the directory ...Extra config file (given by `--extra-config`) may contain paths, to extra driver files for example. When these are relative, they are search in the current dir and in the why3 share directory. They should be search also in the directory of the extra config file itself.1.6.1MARCHE ClaudeMARCHE Claudehttps://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/738support CVC5 up to 1.0.4 and Z3 up to 4.122023-02-21T14:50:25+01:00MARCHE Claudesupport CVC5 up to 1.0.4 and Z3 up to 4.121.6.0MARCHE ClaudeMARCHE Claudehttps://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/733recover non-string representation of CE values2023-02-17T11:36:33+01:00MARCHE Clauderecover non-string representation of CE valuesThe former `model_value` datatype for CE values contained, for constants like bitvectors or floats, both a verbatim (of type string) and a specific value. It would be better to have the same in the new `concrete_syntax_value` type.
More...The former `model_value` datatype for CE values contained, for constants like bitvectors or floats, both a verbatim (of type string) and a specific value. It would be better to have the same in the new `concrete_syntax_value` type.
Moreover, the `concrete_syntax_value` type should be documented in the chapter API of Why3 manual1.6.0MOREAU SoleneMOREAU Solenehttps://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/724Regressions with Gappa2023-04-04T15:00:23+02:00Guillaume CluzelRegressions with GappaI found some regression in why3 when I try to use Gappa 1.4.0 to prove some goals.
I join two gappa files that show the regression:
* [problematic_file.gappa](/uploads/a4b34a34caf56000d672b16e3f4ea40a/adtDekker-Main_module-dekkerqtvc_1....I found some regression in why3 when I try to use Gappa 1.4.0 to prove some goals.
I join two gappa files that show the regression:
* [problematic_file.gappa](/uploads/a4b34a34caf56000d672b16e3f4ea40a/adtDekker-Main_module-dekkerqtvc_1.gappa)
* [good_file.gappa](/uploads/5373bd4d005303c860bf504fcf1967e1/adtDekker-Main_module-dekkerqtvc_3.gappa)
Gappa takes about 10s to return on the first file, and less than one second on the second file.
After investigations, it looks like the problem comes from the commit 05a7bc865da957e8a14d6b44891454b96e2c89bd (MR why3/why3!749). In particular, the fact that the definitions of `max_int` and `max_real` are turned into lemmas really makes the proofs harder.1.6.1BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/723Give values to BV constants when cloning2023-06-16T10:44:34+02:00MARCHE ClaudeGive values to BV constants when cloningThe BV constants `one`, `ones`, `zero` and `zeros` should be given values when cloning, e.g. BV32 etc., instead of being given in SMT2 driver.
The impact on proofs and on CEs and CE checking should be carefully checked.The BV constants `one`, `ones`, `zero` and `zeros` should be given values when cloning, e.g. BV32 etc., instead of being given in SMT2 driver.
The impact on proofs and on CEs and CE checking should be carefully checked.1.7.0BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/722Feature wish: restrict allowed debug flags to regular identifiers2023-02-21T17:04:34+01:00MARCHE ClaudeFeature wish: restrict allowed debug flags to regular identifiersNot a bug but it is annoying to have flags sometimes using `-` and sometimes `_`.
A suggestion is to restrict debug flags names to identifiers e.g regexp `[A-Za-z0-9_']+`Not a bug but it is annoying to have flags sometimes using `-` and sometimes `_`.
A suggestion is to restrict debug flags names to identifiers e.g regexp `[A-Za-z0-9_']+`1.6.0MARCHE ClaudeMARCHE Claudehttps://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