why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2020-03-24T00:35:22Zhttps://gitlab.inria.fr/why3/why3/-/issues/462Detection of non-progressing transformation is broken2020-03-24T00:35:22ZGuillaume MelquiondDetection of non-progressing transformation is brokenThis was presumably caused by e51eff2e0c392bf15f6508b23357a1544bc720fb. CC @paskevycThis was presumably caused by e51eff2e0c392bf15f6508b23357a1544bc720fb. CC @paskevyc1.3.1Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/182Unsound termination check2018-10-05T11:56:19ZGuillaume MelquiondUnsound termination checkConsider the following snippet:
let rec function f () : unit = f ()
let main () = f ()
According to Why3, this is a terminating function, which gets extracted to a non-terminating one:
let rec f (_: unit) : unit = f ()
let main (_: unit) : unit = f ()Consider the following snippet:
let rec function f () : unit = f ()
let main () = f ()
According to Why3, this is a terminating function, which gets extracted to a non-terminating one:
let rec f (_: unit) : unit = f ()
let main (_: unit) : unit = f ()1.1.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/6Error-prone behavior when cloning theories2018-06-15T08:38:42ZGuillaume MelquiondError-prone behavior when cloning theoriesWhen cloning a theory, the behavior is to keep axioms as axioms, unless the user explicitly put a `with lemma foo` clause. This approach is error-prone, as it will cause (possibly inconsistent) facts to never get any proof obligation, due to the user forgetting about them at clone time. I suggest that the default behavior be changed so that any cloned axiom produces a proof obligation, unless the user explicitly put a `with axiom foo` clause. For the sake of conciseness, there should be a special syntax (e.g. `with axiom *`) to skip over all the remaining cloned axioms. Another possibility would be to not turn cloned axioms into lemmas if none of their symbols got instantiated at clone time.When cloning a theory, the behavior is to keep axioms as axioms, unless the user explicitly put a `with lemma foo` clause. This approach is error-prone, as it will cause (possibly inconsistent) facts to never get any proof obligation, due to the user forgetting about them at clone time. I suggest that the default behavior be changed so that any cloned axiom produces a proof obligation, unless the user explicitly put a `with axiom foo` clause. For the sake of conciseness, there should be a special syntax (e.g. `with axiom *`) to skip over all the remaining cloned axioms. Another possibility would be to not turn cloned axioms into lemmas if none of their symbols got instantiated at clone time.1.0.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/60"at" in transformation arguments is silently ignored2018-03-21T08:32:11ZRaphaël Rieu-Helft"at" in transformation arguments is silently ignoredIn transformation arguments, "at" seems to be silently ignored.
```
let a = Array.make 10 0
label L in
a[0] <- 0;
assert { true }
```
If I call cut (a = (a at L)) in the proof of the assertion, the cut indication is "a=a". I have to call "cut (a=a1)" in order to get the desired result.In transformation arguments, "at" seems to be silently ignored.
```
let a = Array.make 10 0
label L in
a[0] <- 0;
assert { true }
```
If I call cut (a = (a at L)) in the proof of the assertion, the cut indication is "a=a". I have to call "cut (a=a1)" in order to get the desired result.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/91Constructor Dlet never used2018-03-02T09:52:30ZDAILLER SylvainConstructor Dlet never usedHello,
In branch new_ide, the parser does not seem to generate the constructor Dlet (defined in src/parser/ptree.ml). I think it was replaced at some point. Is it safe to remove it ? Is it used by the API ?
The problem does not arise in master where Dfun does not exists and Dlet seems to replace it.Hello,
In branch new_ide, the parser does not seem to generate the constructor Dlet (defined in src/parser/ptree.ml). I think it was replaced at some point. Is it safe to remove it ? Is it used by the API ?
The problem does not arise in master where Dfun does not exists and Dlet seems to replace it.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/580Comparing constants2021-09-15T14:04:46ZQuentin GarcheryComparing constantsThe comparison of constants `Constant.compare_const` makes the distinction between structural and semantic comparison. This distinction is not reflected in the way constants are hashed (currently this is done with `Hashtbl.hash c` for any constant `c`, line 452 in `term.ml`). This means that `t_hash_generic` cannot be compatible with `t_equal_generic` when doing a semantic comparison of constants (optional argument `const` set to `false`). This can lead to errors, for example when defining a new hash table with these comparison and hash functions.
Also why is semantic comparison not the default for `t_equal` ? I would expect a call to `t_equal` to return `true` on two terms that are both printed as `42`.The comparison of constants `Constant.compare_const` makes the distinction between structural and semantic comparison. This distinction is not reflected in the way constants are hashed (currently this is done with `Hashtbl.hash c` for any constant `c`, line 452 in `term.ml`). This means that `t_hash_generic` cannot be compatible with `t_equal_generic` when doing a semantic comparison of constants (optional argument `const` set to `false`). This can lead to errors, for example when defining a new hash table with these comparison and hash functions.
Also why is semantic comparison not the default for `t_equal` ? I would expect a call to `t_equal` to return `true` on two terms that are both printed as `42`.https://gitlab.inria.fr/why3/why3/-/issues/558Overzealous positivity checker?2021-03-03T11:24:23ZRaphaël Rieu-HelftOverzealous positivity checker?On the following example, Why3 complains about a non strictly positive occurrence of `t`, but I don't understand why it is problematic.
```
use int.Int
type t = { x : int }
with u = { y : t -> int; }
```
Obviously, in this simplified example, the recursive type definition is not needed, so there is an easy workaround. But in my general usecase (translating C programs to WhyML, including forward struct declarations and structs containing pointers to other structs), I will need recursive type definitions and this workaround will not apply. I don't understand the positivity criterion well enough to understand if what I'm doing is actually problematic or if the checker is being overzealous. @paskevyc maybe you can enlighten me?On the following example, Why3 complains about a non strictly positive occurrence of `t`, but I don't understand why it is problematic.
```
use int.Int
type t = { x : int }
with u = { y : t -> int; }
```
Obviously, in this simplified example, the recursive type definition is not needed, so there is an easy workaround. But in my general usecase (translating C programs to WhyML, including forward struct declarations and structs containing pointers to other structs), I will need recursive type definitions and this workaround will not apply. I don't understand the positivity criterion well enough to understand if what I'm doing is actually problematic or if the checker is being overzealous. @paskevyc maybe you can enlighten me?https://gitlab.inria.fr/why3/why3/-/issues/414Bad contract for local function inside recursive functions2019-11-26T17:51:38ZDAILLER SylvainBad contract for local function inside recursive functionsIn this example, Why3 should force `f` to have `raises {TODO}` in its contract. It should be consistent with the non-recursive case.
```
use int.Int
exception TODO
let rec e (a : int) : int
ensures { result = a }
raises { TODO -> a = 1 }
=
let f (a : int) : int
=
e 1 in
if a = 1 then
raise TODO
else f 2
```In this example, Why3 should force `f` to have `raises {TODO}` in its contract. It should be consistent with the non-recursive case.
```
use int.Int
exception TODO
let rec e (a : int) : int
ensures { result = a }
raises { TODO -> a = 1 }
=
let f (a : int) : int
=
e 1 in
if a = 1 then
raise TODO
else f 2
```https://gitlab.inria.fr/why3/why3/-/issues/396Fix module cloning with respect to effects2021-02-05T13:26:32ZGuillaume MelquiondFix module cloning with respect to effectsAndrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/369Pattern matching gives confusing error messages2019-12-04T12:10:23ZGuillaume MelquiondPattern matching gives confusing error messagesWhile investigating #213, I found the following testcase:
```
type foo = { bar: int } invariant { true }
let baz (v: foo): int = match v with { bar = b } -> b end
```
```
File "foo.mlw", line 2, characters 37-48:
Function mk foo is not a constructor
```
Either removing the invariant from `foo` or using `v.bar` in `baz` avoid the issue.While investigating #213, I found the following testcase:
```
type foo = { bar: int } invariant { true }
let baz (v: foo): int = match v with { bar = b } -> b end
```
```
File "foo.mlw", line 2, characters 37-48:
Function mk foo is not a constructor
```
Either removing the invariant from `foo` or using `v.bar` in `baz` avoid the issue.https://gitlab.inria.fr/why3/why3/-/issues/358Bad error message using `old` inside abstract blocks2019-06-28T09:05:00ZRaphaël Rieu-HelftBad error message using `old` inside abstract blocks```
use int.Int
use mach.int.Int63
use ref.Ref
let test (r: ref int63) : int63 =
begin ensures { !r = old !r + 1 }
r := !r + 1;
assert { !r = old !r + 1 }
end;
42
```
```
> why3 prove test_old.mlw
File "test_old.mlw", line 5, characters 0-129:
Ident r is not yet declared
```
The use of `old` in the assertion is incorrect (should it?), but the error message is imprecise and the localization spans the whole `test` function.```
use int.Int
use mach.int.Int63
use ref.Ref
let test (r: ref int63) : int63 =
begin ensures { !r = old !r + 1 }
r := !r + 1;
assert { !r = old !r + 1 }
end;
42
```
```
> why3 prove test_old.mlw
File "test_old.mlw", line 5, characters 0-129:
Ident r is not yet declared
```
The use of `old` in the assertion is incorrect (should it?), but the error message is imprecise and the localization spans the whole `test` function.https://gitlab.inria.fr/why3/why3/-/issues/314Spurious "unused at/old" warning in lemma function parameters2019-06-05T14:53:25ZRaphaël Rieu-HelftSpurious "unused at/old" warning in lemma function parametersPassing a lemma function parameter in the form (pure { x at L }) seems to trigger a spurious "unused at/old" warning.
In the example below, the `at` operator at line 9 works as expected, but the following warning is emitted:
```
File "atold.mlw", line 9, characters 17-18:
warning: this `at'/`old' operator is never used
```
```
use int.Int
let lemma l (x:int) requires { x <> 0 } ensures { x * x > 0 } = ()
let f () =
let ref x = any int ensures { result <> 0 } in
label L in
x <- -3;
l (pure { x at L });
assert { (x at L) * (x at L) > 0 };
```Passing a lemma function parameter in the form (pure { x at L }) seems to trigger a spurious "unused at/old" warning.
In the example below, the `at` operator at line 9 works as expected, but the following warning is emitted:
```
File "atold.mlw", line 9, characters 17-18:
warning: this `at'/`old' operator is never used
```
```
use int.Int
let lemma l (x:int) requires { x <> 0 } ensures { x * x > 0 } = ()
let f () =
let ref x = any int ensures { result <> 0 } in
label L in
x <- -3;
l (pure { x at L });
assert { (x at L) * (x at L) > 0 };
```Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/261Giving names to requires and ensures2019-06-12T10:29:45ZQuentin GarcheryGiving names to requires and ensuresAllow to give names to the pre/post-conditions, for example using the syntax :
`requires arg_pos { x > 0 }`
This would be helpful because :
* it would make it clear where this axiom comes from when proving VCs
* it would make the proof more robust as the axiom name would not change from `H12` to `H13` when adding another `requires`Allow to give names to the pre/post-conditions, for example using the syntax :
`requires arg_pos { x > 0 }`
This would be helpful because :
* it would make it clear where this axiom comes from when proving VCs
* it would make the proof more robust as the axiom name would not change from `H12` to `H13` when adding another `requires`Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/214Type mismatch when cloning2018-11-09T16:29:59ZGhost UserType mismatch when cloningIf I have the following code:
```
module A
exception E
let f (b: bool): int
raises { E }
=
(if b then return 0);
raise E
end
module B
clone A
end
```
Then I get the following error when I try to prove it:
```
$ why3 prove -P z3 bug.mlw
File "bug.mlw", line 12, characters 8-9:
warning: cloned theory .A does not contain any abstract symbol; it should be used instead
File "bug.mlw", line 12, characters 2-9:
Type mismatch between int and ()
```
However, if I comment out the "clone A" line, I don't get the "type mismatch" error anymore.
Is this expected?
If so, how am I supposed to fix `f` to avoid this error when cloning?
Thanks in advance.If I have the following code:
```
module A
exception E
let f (b: bool): int
raises { E }
=
(if b then return 0);
raise E
end
module B
clone A
end
```
Then I get the following error when I try to prove it:
```
$ why3 prove -P z3 bug.mlw
File "bug.mlw", line 12, characters 8-9:
warning: cloned theory .A does not contain any abstract symbol; it should be used instead
File "bug.mlw", line 12, characters 2-9:
Type mismatch between int and ()
```
However, if I comment out the "clone A" line, I don't get the "type mismatch" error anymore.
Is this expected?
If so, how am I supposed to fix `f` to avoid this error when cloning?
Thanks in advance.1.1.1https://gitlab.inria.fr/why3/why3/-/issues/184Improve the "diverges" effect2018-10-04T12:22:49ZGuillaume MelquiondImprove the "diverges" effectThis is a followup on !19 . After a long brainstorming session with @paskevyc , here is the system we have devised to improve the `diverges` effect, so that it covers a lot more cases.
Regarding the implementation, divergence is currently encoded by a boolean named `Ity.eff_oneway`. We propose to replace this boolean by a tristate value that says ghostifiable (1) or non-ghostifiable terminating (2) or possibly non-terminating (3). State 2 is the new one; the semantics of the other two is left unchanged. The ordering is from left to right, i.e., combining a state-`i` expression with a state-`j` expression gives an expression with state `max i j`. Moreover, a `val` declaration with a given state can only be refined with a `let` definition with a state lower or equal. A `val diverges` declaration has state 3, and so has a non-terminating `let` expression. A `ghost` expression can only have state 1. A `let` definition with state 3 must be explicitly specified as `diverges`. So, the two critical points are that a `let` definition with state 2 does not need to be specified as such, and that it can be declared neither `ghost` nor `function`.
Regarding the surface language, we just need a new effect keyword to specify that a `val` declaration has state 2. For now, we do not give any way for the user to split state 2 into several subcategories for the sake of documentation; this can come later.
Applications of this new state are:
- `peano.Int63.to_in63` @bobot ;
- `alloca` and `c_assert` @rrieuhel ;
- `read`, `write`, `random`, etc.
Note that, in the later applications, e.g. `random`, we no longer need a dummy `writes` specification (if we are not interested in a bit-precise modeling). Note also that state 2 has been described as terminating, but it should be understood as terminating if the environment is cooperating. For example, a WhyML program with state 2 can end up being killed by `SIGPIPE` during a `write` call.
I am assigning this report to @rrieuhel . But @bobot, if you need it soon, do not hesitate to take over.This is a followup on !19 . After a long brainstorming session with @paskevyc , here is the system we have devised to improve the `diverges` effect, so that it covers a lot more cases.
Regarding the implementation, divergence is currently encoded by a boolean named `Ity.eff_oneway`. We propose to replace this boolean by a tristate value that says ghostifiable (1) or non-ghostifiable terminating (2) or possibly non-terminating (3). State 2 is the new one; the semantics of the other two is left unchanged. The ordering is from left to right, i.e., combining a state-`i` expression with a state-`j` expression gives an expression with state `max i j`. Moreover, a `val` declaration with a given state can only be refined with a `let` definition with a state lower or equal. A `val diverges` declaration has state 3, and so has a non-terminating `let` expression. A `ghost` expression can only have state 1. A `let` definition with state 3 must be explicitly specified as `diverges`. So, the two critical points are that a `let` definition with state 2 does not need to be specified as such, and that it can be declared neither `ghost` nor `function`.
Regarding the surface language, we just need a new effect keyword to specify that a `val` declaration has state 2. For now, we do not give any way for the user to split state 2 into several subcategories for the sake of documentation; this can come later.
Applications of this new state are:
- `peano.Int63.to_in63` @bobot ;
- `alloca` and `c_assert` @rrieuhel ;
- `read`, `write`, `random`, etc.
Note that, in the later applications, e.g. `random`, we no longer need a dummy `writes` specification (if we are not interested in a bit-precise modeling). Note also that state 2 has been described as terminating, but it should be understood as terminating if the environment is cooperating. For example, a WhyML program with state 2 can end up being killed by `SIGPIPE` during a `write` call.
I am assigning this report to @rrieuhel . But @bobot, if you need it soon, do not hesitate to take over.Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/165Variants for lemma functions2018-10-05T11:56:20ZGuillaume MelquiondVariants for lemma functions```
type nat = O | S nat
let rec function plus (x y : nat) : nat =
match x with
| O -> y
| S x' -> plus x' (S y)
end
let rec lemma plus_S (x y : nat) : unit
variant { x }
= match x with
| O -> ()
| S x' -> plus_S x' (S y)
end
```
Why3 rejects the `let rec lemma` definition if `variant` is not specified. It would be more user-friendly if it could use the same heuristic as for the `let rec function` definition. Moreover, that would avoid an especially dumb proof obligation:
```
goal VC plus_S :
forall x:nat.
match x with
| O -> true
| S x' -> match x with
| O -> false
| S f -> f = x'
end
end
``````
type nat = O | S nat
let rec function plus (x y : nat) : nat =
match x with
| O -> y
| S x' -> plus x' (S y)
end
let rec lemma plus_S (x y : nat) : unit
variant { x }
= match x with
| O -> ()
| S x' -> plus_S x' (S y)
end
```
Why3 rejects the `let rec lemma` definition if `variant` is not specified. It would be more user-friendly if it could use the same heuristic as for the `let rec function` definition. Moreover, that would avoid an especially dumb proof obligation:
```
goal VC plus_S :
forall x:nat.
match x with
| O -> true
| S x' -> match x with
| O -> false
| S f -> f = x'
end
end
```Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/123Divergence error message arrives too early2018-06-19T10:02:03ZGuillaume MelquiondDivergence error message arrives too earlyWhen running `why3 execute foo.mlw Top.f` on
```
let f () =
while false do () done;
42
```
I expect
```
Execution of Top.f ():
type: int
result: 42
globals:
```
but I get
```
File "foo.mlw", line 2, characters 2-26:
this expression may diverge, but this is not stated in the specification
```
Having to litter the code with `diverges` or `variant` before being able to test it is a bit frustrating.When running `why3 execute foo.mlw Top.f` on
```
let f () =
while false do () done;
42
```
I expect
```
Execution of Top.f ():
type: int
result: 42
globals:
```
but I get
```
File "foo.mlw", line 2, characters 2-26:
this expression may diverge, but this is not stated in the specification
```
Having to litter the code with `diverges` or `variant` before being able to test it is a bit frustrating.https://gitlab.inria.fr/why3/why3/-/issues/111Impossible to reload the ide after parsing error2018-05-01T15:35:26ZDAILLER SylvainImpossible to reload the ide after parsing errorHello,
In master, when starting the IDE on a malformed .mlw (having a syntax error: I tried an lident in module name) and then reloading it, I fall in an assert failure from Typing.open_file.
I think the reason for this behavior is that when I get the parsing error, the "typing file Stack" is never closed through Typing.close_file: it is normally called in parser.mly on rule "mlw_file".
I suggest replacing the following code in lexer.mll:
``let mm = Loc.with_location (mlw_file token) lb in``
with something along the lines of:
``let mm = try Loc.with_location (mlw_file token) lb with | e -> ignore (Typing.close_file ()); raise e in``
so that the stack is "cleared" even when a parsing error is raised.
I am not sure this is the way you would like to solve this problem: thats why I opened an issue.
Copying @paskevycHello,
In master, when starting the IDE on a malformed .mlw (having a syntax error: I tried an lident in module name) and then reloading it, I fall in an assert failure from Typing.open_file.
I think the reason for this behavior is that when I get the parsing error, the "typing file Stack" is never closed through Typing.close_file: it is normally called in parser.mly on rule "mlw_file".
I suggest replacing the following code in lexer.mll:
``let mm = Loc.with_location (mlw_file token) lb in``
with something along the lines of:
``let mm = try Loc.with_location (mlw_file token) lb with | e -> ignore (Typing.close_file ()); raise e in``
so that the stack is "cleared" even when a parsing error is raised.
I am not sure this is the way you would like to solve this problem: thats why I opened an issue.
Copying @paskevycDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/87Cannot use a type variable absent from the function arguments2018-05-23T07:37:59ZMARCHE ClaudeCannot use a type variable absent from the function argumentsThe following is an excerpt of a code that was working in the 'old' system.
It is not well-typed anymore: `Unbound type variable: 'c`
```
function compose (g:'b -> 'c) (f:'a -> 'b) : 'a -> 'c
axiom compose_def : forall g:'b -> 'c,f:'a -> 'b,x:'a.
compose g f x = g (f x)
function const (x: 'b) : 'a -> 'b
axiom const_def : forall x:'b,z:'a. const x z = x
predicate extensionalEqual (f g:'a -> 'b) =
forall x:'a. f x = g x
let lemma const_compose_right (f:'a -> 'b) (x:'a) : unit
ensures { compose f (const x) = (const (f x): 'c -> 'b) }
=
assert { extensionalEqual (const (f x) : 'c -> 'b) (compose f (const x)) }
```The following is an excerpt of a code that was working in the 'old' system.
It is not well-typed anymore: `Unbound type variable: 'c`
```
function compose (g:'b -> 'c) (f:'a -> 'b) : 'a -> 'c
axiom compose_def : forall g:'b -> 'c,f:'a -> 'b,x:'a.
compose g f x = g (f x)
function const (x: 'b) : 'a -> 'b
axiom const_def : forall x:'b,z:'a. const x z = x
predicate extensionalEqual (f g:'a -> 'b) =
forall x:'a. f x = g x
let lemma const_compose_right (f:'a -> 'b) (x:'a) : unit
ensures { compose f (const x) = (const (f x): 'c -> 'b) }
=
assert { extensionalEqual (const (f x) : 'c -> 'b) (compose f (const x)) }
```1.0.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/72Coercion and Higher-Order2018-03-06T17:32:38ZCLOCHARD MartinCoercion and Higher-OrderCoercions are not applied under implicit higher-order application.
Examples:
```
module Foo1
type t
type u
function f t : u
meta coercion function f
constant g : u -> bool
goal G : forall x:t. g x
end
```
```
module Foo2
type t
type u
function f t : u -> u
meta coercion function f
goal G : forall x:t,y:u. x y = y
end
```
In both modules, the occurrence of "x" within the goal is not coerced as one would expect, leading to a type error. However, when one explicit the higher-order application (operator (@)), those occurrences are coerced as expected.Coercions are not applied under implicit higher-order application.
Examples:
```
module Foo1
type t
type u
function f t : u
meta coercion function f
constant g : u -> bool
goal G : forall x:t. g x
end
```
```
module Foo2
type t
type u
function f t : u -> u
meta coercion function f
goal G : forall x:t,y:u. x y = y
end
```
In both modules, the occurrence of "x" within the goal is not coerced as one would expect, leading to a type error. However, when one explicit the higher-order application (operator (@)), those occurrences are coerced as expected.1.0.0Andrei PaskevichAndrei Paskevich