why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-02-21T14:50:25+01:00https://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 Claudehttps://gitlab.inria.fr/why3/why3/-/issues/713misalignment of documentation with parser (python)2022-11-17T18:03:48+01:00Yannick Chevaliermisalignment of documentation with parser (python)Hi everyone,
in Section 9.2.1, Syntax of micro-Python, of the manual (https://why3.lri.fr/doc/input_formats.html#syntax-of-micro-python) the logic declaration of a function is defined as:
logic_declaration ::= "#@" "function" iden...Hi everyone,
in Section 9.2.1, Syntax of micro-Python, of the manual (https://why3.lri.fr/doc/input_formats.html#syntax-of-micro-python) the logic declaration of a function is defined as:
logic_declaration ::= "#@" "function" identifier "(" params ")" return_type? ("variant" "{" term "}")? ("=" term)? NEWLINE
However, in the parser (file why3/plugins/python/py_parser.mly on gitlab), the corresponding rule for fp_variant is (line 155):
LEFTBR VARIANT v=term RIGHTBR { v }
i.e., the documentation says to write it variant { n } and the parser awaits { variant n }.
Bests,
YannickJean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/712Reactivate maps_poly and maps_mono tests in check-ce-bench2023-08-29T20:10:21+02:00MOREAU SoleneReactivate maps_poly and maps_mono tests in check-ce-benchThe tests have been disabled because the behaviour was different locally and on the CI machine, even with stepslimit for the provers.
See https://gitlab.inria.fr/why3/why3/-/merge_requests/772 and https://gitlab.inria.fr/why3/why3/-/com...The tests have been disabled because the behaviour was different locally and on the CI machine, even with stepslimit for the provers.
See https://gitlab.inria.fr/why3/why3/-/merge_requests/772 and https://gitlab.inria.fr/why3/why3/-/commit/3310bdd7e873e4f839ce2d9deba602c25f871e4a.
To be investigated.1.7.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/709All warnings should be toggleable2023-09-11T19:12:36+02:00MARCHE ClaudeAll warnings should be toggleableCurrently, a few warnings can be made quiet (eg for unused variables) but most are not. It would be nice to have a systematic way to disable warnings, such as the Ocaml mechanism.Currently, a few warnings can be made quiet (eg for unused variables) but most are not. It would be nice to have a systematic way to disable warnings, such as the Ocaml mechanism.1.7.0Matteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/705Global constant missing in the RAC evaluation context2023-02-17T11:43:08+01:00MOREAU SoleneGlobal constant missing in the RAC evaluation contextIn the test [](https://gitlab.inria.fr/why3/why3/-/blob/master/bench/check-ce/integers.mlw), the verdict for the CE for the goal `g2_lab` is incomplete because the postcondition of the goal cannot be evaluated by the RAC.
The model for ...In the test [](https://gitlab.inria.fr/why3/why3/-/blob/master/bench/check-ce/integers.mlw), the verdict for the CE for the goal `g2_lab` is incomplete because the postcondition of the goal cannot be evaluated by the RAC.
The model for the CE contains a value for `g` and for `x`, but the evaluation context in the RAC does not contain any value for the global constant `g` (use `--debug=rac-values`).https://gitlab.inria.fr/why3/why3/-/issues/703Term size explosion in reduction engine2023-01-31T13:51:15+01:00MOREAU SoleneTerm size explosion in reduction engineWith the attached file (coming from the SPARK testsuite), the transformation `compute_in_goal` called by the RAC is very slow.
The reason is an explosion of the term size when calling `Reduction_engine.normalize` in `Compute.normalize_hy...With the attached file (coming from the SPARK testsuite), the transformation `compute_in_goal` called by the RAC is very slow.
The reason is an explosion of the term size when calling `Reduction_engine.normalize` in `Compute.normalize_hyp_or_goal`.
As discussed with @marche, the goal is to limit the reduction engine by a growth factor. To this goal, we enrich the `cont` field of the `config` type with the size of the given `cont`, and we update this size each time we update the `cont` field in `Reduction_engine.reduce`.
[use_flags.mlw](/uploads/850f230af17d9ea9f6222695cc2d8a07/use_flags.mlw)
[term.txt](/uploads/7778771c59631c77ad47f52b7fbe99c6/term.txt)MOREAU SoleneMOREAU Solenehttps://gitlab.inria.fr/why3/why3/-/issues/702--no-stdlib always crashes2022-10-17T19:00:56+02:00Guillaume Cluzel--no-stdlib always crashesThe option `--no-stdlib` does not correctly works.
```
module M
type t
predicate p (x : t) = true
lemma l: forall x. p x
end
```
with the command line `why3 --no-stdlib prove -P cvc4 test.mlw`.The option `--no-stdlib` does not correctly works.
```
module M
type t
predicate p (x : t) = true
lemma l: forall x. p x
end
```
with the command line `why3 --no-stdlib prove -P cvc4 test.mlw`.https://gitlab.inria.fr/why3/why3/-/issues/700Global directives are ignored in extra drivers2023-02-22T15:51:53+01:00Raphaël Rieu-HelftGlobal directives are ignored in extra driversIn `Driver.load_prover_raw`, when parsing the extra drivers, only the `theory_rules` fields is actually used. Is there a reason why a user shouldn't be allowed to add things to the global prelude? The use case I have in mind is changing ...In `Driver.load_prover_raw`, when parsing the extra drivers, only the `theory_rules` fields is actually used. Is there a reason why a user shouldn't be allowed to add things to the global prelude? The use case I have in mind is changing some options of CVC5 via the `set-option` smtlib command.1.6.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/699bad lexing for separation of commands2022-10-17T11:03:09+02:00MARCHE Claudebad lexing for separation of commandsa command like
```
apply H with id,(f x)
```
wants to split the string at the space between f and x.
On the other hand
```
apply H with id, (f x)
```
worksa command like
```
apply H with id,(f x)
```
wants to split the string at the space between f and x.
On the other hand
```
apply H with id, (f x)
```
worksMARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/698remove_unused:dependency not strong enough with definition given in drivers2022-10-20T11:44:26+02:00Guillaume Cluzelremove_unused:dependency not strong enough with definition given in driversThe transformation `remove_unused` does not remove the axioms that are marked with the meta `remove_unused:dependency` when a symbol in this axiom is defined in a driver.
I have a small repro-case to make it clearer.
```ocaml
(* a.mlw ...The transformation `remove_unused` does not remove the axioms that are marked with the meta `remove_unused:dependency` when a symbol in this axiom is defined in a driver.
I have a small repro-case to make it clearer.
```ocaml
(* a.mlw *)
module A
predicate p (x : int)
axiom p_def: forall x. x <> 0 -> p x
meta "remove_unused:dependency" axiom p_def, predicate p
predicate q (x : int)
axiom q_def: forall x. p x -> q x
meta "remove_unused:dependency" axiom q_def, predicate q
end
```
```ocaml
(* b.mlw *)
module B
use a.A
predicate c (x : int)
lemma l: forall x. c x
end
```
and I use a driver to override the symbol `q`:
```ocaml
(* drv.drv *)
theory a.A
syntax predicate q "(= %1 0)"
end
```
together with the config:
```
[prover_modifiers]
driver = "drv.drv"
name = "CVC4"
```
When I run the IDE, with `why3 ide -L . --extra-config=c.conf`, and I look at the cvc4 smt2 file generated for the task `l`, I get
```smt2
;; produced by cvc4_17.drv ;;
(set-logic ALL_SUPPORTED)
(set-info :smt-lib-version 2.6)
;; p
(declare-fun p (Int) Bool)
;; p_def
(assert (forall ((x Int)) (=> (not (= x 0)) (p x))))
;; q_def
(assert (forall ((x Int)) (=> (p x) (= x 0))))
;; c
(declare-fun c (Int) Bool)
(assert
(not (forall ((x Int)) (c x))))
(check-sat)
(get-info :reason-unknown)
```
As you can see, the axiom `p_def` and `q_def` have not been removed despite the meta `remove_unused`. If I do not define `q` in a driver, both axioms are removed. It seems that this case always happen in the standard library and unfortunately we keep a lot of axioms in the context that should be removed by the transformation `remove_unused` because the axiom is not used in the task.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/697enable profiling with Ocaml >= 4.092022-11-15T12:40:31+01:00MARCHE Claudeenable profiling with Ocaml >= 4.09The `--enable-profiling` option to `./configure` adds the options `-g` and `-p` to Ocaml compilation. Yet, the option `-p` is not supported anymore by Ocaml >= 4.09
The makefile should be patched to add only the option `-g` when profili...The `--enable-profiling` option to `./configure` adds the options `-g` and `-p` to Ocaml compilation. Yet, the option `-p` is not supported anymore by Ocaml >= 4.09
The makefile should be patched to add only the option `-g` when profiling and ocaml version >= 4.09
For the record, profiling can be done with `perf` with
```
perf record --call-graph=dwarf -- why3 <options>
perf report
```
You may need to execute the first command with superuser priviledges.
This information should be given in some doc, say in `CONTRIBUTING.md`MARCHE ClaudeMARCHE Claude