why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-09-25T13:57:21+02:00https://gitlab.inria.fr/why3/why3/-/issues/801color highlighting takes too long time in IDE2023-09-25T13:57:21+02:00MARCHE Claudecolor highlighting takes too long time in IDEColor highlighting seems to take a lot of time.
It seems it tries to colorize much too many terms: it should be limited to the local context.
Limiting to the local context may indeed solve the long time issueColor highlighting seems to take a lot of time.
It seems it tries to colorize much too many terms: it should be limited to the local context.
Limiting to the local context may indeed solve the long time issuehttps://gitlab.inria.fr/why3/why3/-/issues/800RAC : Improve the validation of some CEX2023-11-08T11:42:35+01:00BONNOT PaulRAC : Improve the validation of some CEXWe have some examples of counterexamples in TrustInSoft that should be considered as valid but the Z3 and CVCx are unable to verify them.We have some examples of counterexamples in TrustInSoft that should be considered as valid but the Z3 and CVCx are unable to verify them.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/798Loading error when a transformation is present twice2023-09-20T15:54:42+02:00BONNOT PaulLoading error when a transformation is present twiceIn the IDE, it is possible to have the same transformation present twice at one node.
However, when loading a session where this is the case, we get a failure.
The behavior should be consistent, I think allowing the duplication of a tra...In the IDE, it is possible to have the same transformation present twice at one node.
However, when loading a session where this is the case, we get a failure.
The behavior should be consistent, I think allowing the duplication of a transformation on a node is the better choice here.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/786Improving the Why3 CLI for proving2024-01-12T14:56:18+01:00Xavier DenisImproving the Why3 CLI for provingIn the last GT we saw the new changes to `why3 session-create` and the improved `why3 bench`, during that session I proposed that it would be helpful for Why3 to provide a CLI interface of 'equal' power to the IDE, for the users of Why3 ...In the last GT we saw the new changes to `why3 session-create` and the improved `why3 bench`, during that session I proposed that it would be helpful for Why3 to provide a CLI interface of 'equal' power to the IDE, for the users of Why3 that for various reasons cannot or chose not to use the IDE.
In particular, I'm refering to the ability to run _strategies_ on targetted files, potentially creating the session if necessary.
If such a command were added it could be done as a replacement for the current `why3 prove` which is sort of misleadingly named as it does not use the sessions, even if they are available.
I think the requirements for this new / upgraded command would be:
- Load or create a session for the targeted files
- Ability to apply transformations, provers and **strategies** to goals in the file
- Should run all chosen provers and output a clear ok / reject message.
What does everyone think?https://gitlab.inria.fr/why3/why3/-/issues/781Understand meta "model projection" introduction during parsing2023-08-23T15:59:33+02:00BONNOT PaulUnderstand meta "model projection" introduction during parsingThe meta "model projection" is introduced in `parsing.mly`.
We should investigate if this is the correct way to proceed because it seems a bit hacky.The meta "model projection" is introduced in `parsing.mly`.
We should investigate if this is the correct way to proceed because it seems a bit hacky.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/778Cleaning code2023-07-17T15:06:07+02:00MARCHE ClaudeCleaning codeThis is a minor issue, nothing visible from users, but there are a few possible code reorganization that should be done:
- [ ] module `Model_parser` should be moved from `core` to `driver`
- [ ] attributes and such declared in `Ident` sh...This is a minor issue, nothing visible from users, but there are a few possible code reorganization that should be done:
- [ ] module `Model_parser` should be moved from `core` to `driver`
- [ ] attributes and such declared in `Ident` should be declared in a more appropriate place
- [ ] ?
This issue is a good candidate for hackathon exercises ;-)https://gitlab.inria.fr/why3/why3/-/issues/767RAC checking : Use only 1 debug flag2023-06-14T11:08:10+02:00BONNOT PaulRAC checking : Use only 1 debug flagCurrently, there are 7 flags related to RAC checking, 5 flags of the form `rac:*` and 2 flags of the form `check_ce:*`.
It is not very practical to use these flags when trying to debug RAC issues, it would be easier to have only 1 flag ...Currently, there are 7 flags related to RAC checking, 5 flags of the form `rac:*` and 2 flags of the form `check_ce:*`.
It is not very practical to use these flags when trying to debug RAC issues, it would be easier to have only 1 flag with an associated verbosity level (1/2/3).BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/754CE: variables in concrete terms should be denoted by idents instead of strings2023-07-17T15:07:32+02:00MARCHE ClaudeCE: variables in concrete terms should be denoted by idents instead of stringsThe current implementation is doubtful, see also !862
The "eval" is likely to involve name clashes, that should be avoided by using identsThe current implementation is doubtful, see also !862
The "eval" is likely to involve name clashes, that should be avoided by using identshttps://gitlab.inria.fr/why3/why3/-/issues/751Add support for ocaml-lsp2023-08-29T16:44:12+02:00Xavier DenisAdd support for ocaml-lspI think the only thing we can do here would be to use `dune` instead of `make`, but it would be great to get Why3 working with ocaml-lsp.I think the only thing we can do here would be to use `dune` instead of `make`, but it would be great to get Why3 working with ocaml-lsp.https://gitlab.inria.fr/why3/why3/-/issues/747extend set of axioms annotated with axioms dependencies2023-09-06T13:45:48+02:00MARCHE Claudeextend set of axioms annotated with axioms dependenciesSet of symbols to annotate:
- [ ] int.Exponentiation.power
- [ ] int.NumOf.numof
- [ ] int.Sum.sum
- [ ] int.Fact.fact
- [ ] int.Iter.iter
- [ ] int.Fibonacci.fib
- [ ] int.WFltof.ltof
- [x] bv.Pow2.pow2
- [ ] bv.BVgen.nth_bv
- [x] bv.BV...Set of symbols to annotate:
- [ ] int.Exponentiation.power
- [ ] int.NumOf.numof
- [ ] int.Sum.sum
- [ ] int.Fact.fact
- [ ] int.Iter.iter
- [ ] int.Fibonacci.fib
- [ ] int.WFltof.ltof
- [x] bv.Pow2.pow2
- [ ] bv.BVgen.nth_bv
- [x] bv.BVgen.uge
- [x] bv.BVgen.ugt
- [x] bv.BVgen.ule
- [x] bv.BVgen.ult
- [x] bv.BVgen.sge
- [x] bv.BVgen.sgt
- [x] bv.BVgen.sle
- [x] bv.BVgen.slt
- [ ] option.Option.is_none
- [ ] option.Map.map
- [ ] to be continued, say with `list.mlw`, etc.1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/745Provide a way to specify triggers for lemmas generated by "let function" and ...2023-03-20T23:02:46+01:00Jacques-Henri JourdanProvide a way to specify triggers for lemmas generated by "let function" and friendshttps://gitlab.inria.fr/why3/why3/-/issues/741eliminate_if is not robust enough against if in triggers2023-07-18T19:01:30+02:00Guillaume Cluzeleliminate_if is not robust enough against if in triggersWhen Gappa is called, its driver call the transformation `inline_all` and later `eliminate_if`.
```
module M
function f (x : int) : int = if x = 0 then x else x
predicate p (y : bool) = y
axiom x: forall x, y [f x]. p y -> x = f x...When Gappa is called, its driver call the transformation `inline_all` and later `eliminate_if`.
```
module M
function f (x : int) : int = if x = 0 then x else x
predicate p (y : bool) = y
axiom x: forall x, y [f x]. p y -> x = f x
lemma l: forall y. p y
end
```
The combination of the two transformations fails on a such program and we get a message like:
```
internal failure: Failure in transformation eliminate_if
This expression isn't supported:
if x = 0 then x else x
cannot eliminate 'if-then-else' in trigger terms
```
As the transformation fails, it becomes impossible to use Gappa on any program that uses an axiom with a trigger like exposed in the example.
Wouldn't it be possible to remove the trigger in a such case if it is not possible to do something smarter?https://gitlab.inria.fr/why3/why3/-/issues/740Incorrect error message2023-03-20T14:27:54+01:00Xavier DenisIncorrect error messageWhen using function literals, we can get unexpected error messages like with the following program:
```
let x () = [| 0; |]
```
Giving the following error:
```
File "../dummy2.mlw", line 2, characters 14-15: Logical symbol (=) is used...When using function literals, we can get unexpected error messages like with the following program:
```
let x () = [| 0; |]
```
Giving the following error:
```
File "../dummy2.mlw", line 2, characters 14-15: Logical symbol (=) is used in a non-ghost context
```
The solution is to `use int.Int` but it would be better to output a more actionable error instead.https://gitlab.inria.fr/why3/why3/-/issues/739complete Coq realizations2024-02-13T13:27:51+01:00MARCHE Claudecomplete Coq realizationsCurrently some Coq realizations have some occurrences of `Admitted`. This should be fixed. Here is the list
- [ ] `lib/coq/bv/BV_gen.v`
- [ ] `lib/coq/ieee_float/Float32.v`
- [ ] `lib/coq/ieee_float/Float64.v`
- [ ] `lib/coq/ieee_float/G...Currently some Coq realizations have some occurrences of `Admitted`. This should be fixed. Here is the list
- [ ] `lib/coq/bv/BV_gen.v`
- [ ] `lib/coq/ieee_float/Float32.v`
- [ ] `lib/coq/ieee_float/Float64.v`
- [ ] `lib/coq/ieee_float/GenericFloat.v`
- [ ] `lib/coq/real/Trigonometry.v`
- [ ] `lib/coq/set/Set.v`1.8.0https://gitlab.inria.fr/why3/why3/-/issues/736Provide more statistics when running RAC using prover calls2023-02-17T18:55:00+01:00MARCHE ClaudeProvide more statistics when running RAC using prover callsWhen using `--check-ce` and `--rac-prover` for categorizing CEs using a prover for evaluating assertions, the time and steps spent by the prover should be reported somehow.
In particular this could provide information on why so much tim...When using `--check-ce` and `--rac-prover` for categorizing CEs using a prover for evaluating assertions, the time and steps spent by the prover should be reported somehow.
In particular this could provide information on why so much time is spent on some tests, e.g. `bench/check-ce/floats.mlw`.
On that particular example though, it should be investigated whether the time might be spent by mpfr.https://gitlab.inria.fr/why3/why3/-/issues/735doubtful placement of attributes when introducing proxy symbols2023-02-15T14:24:35+01:00MARCHE Claudedoubtful placement of attributes when introducing proxy symbolsConsider the small code below
```
val ref x : int
let f () = [@attrib] x <- 0
val g (x:int) : int
let h () = x <- [@attrib] g 0
```
when visualising the internal modules using
```
why3 prove --debug=print_modules,print_attributes f.mlw
`...Consider the small code below
```
val ref x : int
let f () = [@attrib] x <- 0
val g (x:int) : int
let h () = x <- [@attrib] g 0
```
when visualising the internal modules using
```
why3 prove --debug=print_modules,print_attributes f.mlw
```
one can see that the attribute `[@attrib]` is placed inside the `let` introducing proxy symbols:
```
[...]
let o [@mlw:proxy_symbol] = 0 in
[@attrib] (x [@mlw:reference_var]:ref int).contents <- o
[...]
let o [@mlw:proxy_symbol] = let o1 [@mlw:proxy_symbol] = 0 in
[@attrib] g o1 in
(x [@mlw:reference_var]:ref int).contents <- o
```
Is it intentional to put the attribute after the introduction of the `let o ...` and not on the `let o ...` expression itself?
For information, the impact is visible when using bddinfer: the abstract state computed before the statements annotated by `[@attrib]` contains a value for the proxy variable, which is meaningless "before" the statement in question.
Changing that could have an impact elsewhere though, e.g. on CE generation. Investigation and clarification needed.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/734Functions in CE models not consistent with axioms in the source code2023-07-17T15:42:04+02:00MOREAU SoleneFunctions in CE models not consistent with axioms in the source codeIn the tests `bench/check-ce/let_function_logic.mlw`, `bench/check-ce/call-val-function.mlw`, `bench/check-ce/vall_function.mlw` (and maybe some others), the SMT solver returns a model with some functions that are not consistent with the...In the tests `bench/check-ce/let_function_logic.mlw`, `bench/check-ce/call-val-function.mlw`, `bench/check-ce/vall_function.mlw` (and maybe some others), the SMT solver returns a model with some functions that are not consistent with the axioms in the `.mlw` file.
The consequence is that we can have CE classified as `good` while it should not be the case.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/732Run strategy from `why3 prove`2023-01-31T15:53:53+01:00Xavier DenisRun strategy from `why3 prove`The command `why3 prove` includes a `--apply-transformation` option which can be used to apply individual transformations before launching provers with `why3 prove`, however, unlike in the IDE we cannot apply strategies as a transformati...The command `why3 prove` includes a `--apply-transformation` option which can be used to apply individual transformations before launching provers with `why3 prove`, however, unlike in the IDE we cannot apply strategies as a transformation.
It would be useful to have this option when recreating large amounts of proof sessions in a mechanical manner (ie: regenerating the Creusot test suite).https://gitlab.inria.fr/why3/why3/-/issues/731The purpose of the "BV" variants of drivers is unclear2023-07-17T15:27:28+02:00Jacques-Henri JourdanThe purpose of the "BV" variants of drivers is unclearI propose to remove them: it's unclear what is their purpose, and they pose a maintenance issue since they are not in sync with the normal drivers.I propose to remove them: it's unclear what is their purpose, and they pose a maintenance issue since they are not in sync with the normal drivers.https://gitlab.inria.fr/why3/why3/-/issues/730improve translation of div and mod for SMT solvers2023-07-24T17:14:31+02:00MARCHE Claudeimprove translation of div and mod for SMT solversA feedback from AdaCore : changing the translation of `div` and `mod` (both euclidean and computer) into what is currently commented out in the driver improves, in particular for counterexamples. It applies to Z3 as well.A feedback from AdaCore : changing the translation of `div` and `mod` (both euclidean and computer) into what is currently commented out in the driver improves, in particular for counterexamples. It applies to Z3 as well.Matteo ManighettiMatteo Manighetti