why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-07-11T17:21:12+02:00https://gitlab.inria.fr/why3/why3/-/issues/782Questions on TPTP parser in Why32023-07-11T17:21:12+02:00Frédéric BlanquiQuestions on TPTP parser in Why3Hi. I have a number of questions concerning TPTP and Why3. Where is the source code of the TPTP parser used by Why3? Can it parse any TPTP file? Is it part of the Why3 library? Best regards, Frédéric.Hi. I have a number of questions concerning TPTP and Why3. Where is the source code of the TPTP parser used by Why3? Can it parse any TPTP file? Is it part of the Why3 library? Best regards, Frédéric.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/780get rid of meta "model_record"2023-08-23T17:29:30+02:00MARCHE Claudeget rid of meta "model_record"There is a very dirty code in `parser.mly`, function `add_record_projections`, which adds metas `model_record`. This should not be used anymore for CE checking, so this code should be removed.
This code is very dirty because it adds dat...There is a very dirty code in `parser.mly`, function `add_record_projections`, which adds metas `model_record`. This should not be used anymore for CE checking, so this code should be removed.
This code is very dirty because it adds data after typing, an action that is not done when typing from another source than `parser.mly` but say typing a Ptree generated from elsewhere. For example from a parsing of a sexp file.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/779Answer "Valid" should always have priority over other answers of provers in i...2023-07-19T15:37:29+02:00MARCHE ClaudeAnswer "Valid" should always have priority over other answers of provers in incremental modeThe current code in `src/driver/call_provers.ml`, function `analyse`, should always take answer "Valid" when it occurs in a list of answersThe current code in `src/driver/call_provers.ml`, function `analyse`, should always take answer "Valid" when it occurs in a list of answers1.7.0MARCHE ClaudeMARCHE Claudehttps://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/777Simplification of record types with only one field2023-11-23T15:13:38+01:00Gérald PointSimplification of record types with only one fieldWhile working on the Java driver I discovered that record types with only one field are replaced by an alias type. For instance
> type t = { a : bool }
becomes
> type t = bool
Is there a way to disable this behaviour ? It would ease t...While working on the Java driver I discovered that record types with only one field are replaced by an alias type. For instance
> type t = { a : bool }
becomes
> type t = bool
Is there a way to disable this behaviour ? It would ease the compilation of such type into a class with only one instance variable.https://gitlab.inria.fr/why3/why3/-/issues/776`why3 session info` should have a mandatory argument2023-07-19T18:06:38+02:00Xavier Denis`why3 session info` should have a mandatory argumentToday, `why3 session info path` produces _no_ output if no flag is passed. Either this should be changed so that there is a default output (maybe `session-stats`?) or an error should be returned telling you to pick flag. As a new user th...Today, `why3 session info path` produces _no_ output if no flag is passed. Either this should be changed so that there is a default output (maybe `session-stats`?) or an error should be returned telling you to pick flag. As a new user the current behavior is unintuitive.1.7.0https://gitlab.inria.fr/why3/why3/-/issues/775why3server incorrect when client disconnects early2023-08-29T11:38:22+02:00Johannes Kanigwhy3server incorrect when client disconnects earlyThis is an issue that we encountered after the recent why3 merge in SPARK. Matteo wanted to open a ticket about this but I haven't seen it, so I am opening it myself.
The why3server identifies clients via the file descriptor (just an in...This is an issue that we encountered after the recent why3 merge in SPARK. Matteo wanted to open a ticket about this but I haven't seen it, so I am opening it myself.
The why3server identifies clients via the file descriptor (just an integer) of the unix domain socket that is used to communicate between the client and server. The integer is potentially reused when a client disconnects and another one connects later. This can lead to messages "leaking" from one client to the next.
The problematic scenario is where a client disconnects while there are still pending requests in the server for this client. Then a new client connects and receives notifications for the requests of the old client. This usually results in a crash in the new client (as it receives notifications for requests it didn't make).
I was half aware of this problem and took care to program why3 in such a way that it always reads all requests from the server before disconnecting. Claude wasn't aware of this and broke this behavior with patch 8f6b6c6bbc91689b60eb451c86e7c9488cccba93. (At least that's my current understanding).
What do people think of moving away from why3server? The code is very complex and error-prone. To replace its functionality, three things are required:
1. a "limiting" wrapper similar to previous "why3cpulimit"
2. a way to limit number of provers across multiple instances of why3
3. a way to spawn processes from why3 that doesn't introduce small delays (this was the original reason for the why3server, together with (2). When forking from a process that takes a lot of memory, just marking the memory pages as COW takes some small amount of time, which adds up if hundreds of provers are spawned).
For (1), ideally we could reuse a lot of code from the why3server. And from the old why3cpulimit. This is the most complex part IMO, as
For (2), we already have code for Windows and Linux in SPARK that uses semaphores.
For (3), we were hoping that the ocaml spawn library doesn't have this issue (uses vfork).
If that's not an option, we should probably improve the why3server. It's a bit tedious but doable to drop pending requests when a client disconnects.
Yet another option is to live with this and make sure why3 reads the answers for all requests before disconnecting.
Any opinions?1.7.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/774Unused axioms introduced by transformations2023-07-06T01:08:29+02:00Johannes KanigUnused axioms introduced by transformationsMotivating example is this small code:
```
module Test
use ref.Ref
use int.Int
use int.ComputerDivision
let s (x: int)
requires { 0 <= x <= 65535 }
=
let ref y: int = 42 in
assert { [@expl:check 1] 0 <= y * y <= 6...Motivating example is this small code:
```
module Test
use ref.Ref
use int.Int
use int.ComputerDivision
let s (x: int)
requires { 0 <= x <= 65535 }
=
let ref y: int = 42 in
assert { [@expl:check 1] 0 <= y * y <= 65535 };
y <- y * y;
assert { [@expl:check 2] x <> 0 };
y <- div y x;
assert { [@expl:check 3] 0 <= y - 100000 <= 65535 };
y <- y - 2 * y;
end
```
When generating VCs for this file using
```
why3 prove -P cvc5 test.mlw -a split_goal_right -o out
```
We can see that there are useless axioms about references in the VC. My guess is these axioms are introduced by transformations that run after the "remove_unused" transformation, or the transformations don't add the necessary "meta" information to attach axioms to symbols.
It doesn't seem easy to fix, but maybe I'm wrong. Opinions?https://gitlab.inria.fr/why3/why3/-/issues/773dequantification transformation introduces unsoundness2023-06-29T16:08:27+02:00Matteo Manighettidequantification transformation introduces unsoundnessWith the following `bomb.mlw`:
```
axiom test:
forall x:int.
(let y = (not x = 42) in true)
goal foo: false
```
If we run for example `why3 prove bomb.mlw -P CVC5,1.0.4` we correctly get `Prover result is: Unknown (sat)`...With the following `bomb.mlw`:
```
axiom test:
forall x:int.
(let y = (not x = 42) in true)
goal foo: false
```
If we run for example `why3 prove bomb.mlw -P CVC5,1.0.4` we correctly get `Prover result is: Unknown (sat)`.
However running:
`why3 prove bomb.mlw -P CVC5,1.0.4 -a dequantification` gives
```
File "example.mlw", line 5, characters 10-15:
Goal foo.
Prover result is: Valid (0.01s, 213 steps).
```1.7.0Matteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/772Session API should export `merge_file_section`2023-09-12T13:19:02+02:00MARCHE ClaudeSession API should export `merge_file_section`The use case is using Why3 API to build sessions in a context where the parsing of source files is not done by the internal language mechanism. Currently the function `merge_file` of `Session_itp` is calling `Env.read_file`, making impos...The use case is using Why3 API to build sessions in a context where the parsing of source files is not done by the internal language mechanism. Currently the function `merge_file` of `Session_itp` is calling `Env.read_file`, making impossible to workaround the internal language mechanism.
A possible solution would be to export the function `merge_file_section` in the interface, so that the user could feed it with another set of theories coming from its own source.
Another possibility to investigate would be to make `merge_files` more generic by allowing the caller to provide its own function to produce theories.
Yet a problem is that currently a so-called "file" in a session is something identified with a path name (relative to the session directory). In a general context this might be too restrictive. For example one may want to consider that in a session each "file" section correspond to a particular function in a source file. A more general point of view would be to replace this notion of file with a notion of "package" identified with a qualified identifier, which could be interpreted at will, say `like dir1.dir2.filename.Package.Module.function`. The current mechanism enforcing the path name to be relative to the session dir should be relaxed though.MARCHE ClaudeMARCHE Claudehttps://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/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/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/765Export warning ids2023-05-30T13:26:58+02:00MARCHE ClaudeExport warning idsWith the new machinery for warnings, it appears that some warnings are not exported, so not easy to disable via API. Indeed it is possible by calling `Loc.register_warning` with the appropriate string to recover to right warning id, bit ...With the new machinery for warnings, it appears that some warnings are not exported, so not easy to disable via API. Indeed it is possible by calling `Loc.register_warning` with the appropriate string to recover to right warning id, bit this is fragile since it depends on the string given.
Here is a list of warning variables to export:
- [ ] Typing.warn_useless_at1.7.0Matteo ManighettiMatteo Manighettihttps://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 Paul