Skip to content

Commit b215e3f

Browse files
dkcummingrv-auditor
dkcumming
and
rv-auditor
authored
Enable more proofs on CI (#319)
* Add forgotten underscores for Local * Changed `Local` to `LocalToken` in `verify.k` * Added missing cells for proof to pass * Removed `add.k`from prove fail list * Set Version: 0.2.24 * Added proof containing assert * Add forgotten underscores for Local * Changed `Local` to `LocalToken` in `verify.k` * Added missing cells for proof to pass * Removed `add.k`from prove fail list * Added proof containing assert * Set Version: 0.2.24 * Set Version: 0.2.26 * lockfile * mypy pathing * Added proof with another function call. Also tried to minimise the amount of output required information for the proof to go through. It appears the type and value information cannot be ommited as it has a default expected value. * Set Version: 0.2.44 --------- Co-authored-by: devops <devops@runtimeverification.com>
1 parent 9577fbf commit b215e3f

File tree

16 files changed

+278
-12
lines changed

16 files changed

+278
-12
lines changed

‎kmir/poetry.lock‎

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎kmir/pyproject.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "kmir"
7-
version = "0.2.43"
7+
version = "0.2.44"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <contact@runtimeverification.com>",

‎kmir/src/kmir/__init__.py‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,5 @@
11
from typing import Final
22

33
from .kmir import KMIR
4-
from .parse import parse
5-
from .prove import prove, show_proof, view_proof
6-
from .run import run
74

8-
VERSION: Final = '0.2.43'
5+
VERSION: Final = '0.2.44'

‎kmir/src/tests/integration/test-data/handwritten-prove-fail.tsv‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1 @@
11
prove-rs/verify.k 1
2-
prove-rs/add.k 1

‎kmir/src/tests/integration/test-data/prove-rs/add.k‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,13 @@ module ADD
2020
<localDecls>
2121
<localDecl>
2222
<index> _0 </index>
23+
<ty> ( ) </ty>
24+
<value> Unit </value>
2325
...
2426
</localDecl>
2527
<localDecl>
2628
<index> _1 </index>
29+
<ty> i32 </ty>
2730
<value> 42 </value>
2831
...
2932
</localDecl>

‎kmir/src/tests/integration/test-data/prove-rs/assert.k‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
requires "verify.k"
2+
3+
module ASSERT
4+
imports VERIFY
5+
6+
claim
7+
<k>
8+
fn main :: .FunctionPath ( .ParameterList ) -> ( ) { .DebugList let mut _0 : ( ) ; let _1 : i32 ; let mut _2 : bool ; let mut _3 : bool ; let mut _4 : ! ; .BindingList scope 1 { debug num => _1 ; .DebugList .BindingList .ScopeList } .ScopeList bb0 : { _1 = Add ( const 20_i32 , const 22_i32 ) ; _3 = Eq ( _1 , const 42_i32 ) ; _2 = Not ( move _3 ) ; .Statements switchInt ( move _2 ) -> [ 0 : bb2 , .SwitchTargets , otherwise : bb1 ] ; } bb1 : { .Statements _4 = core :: panicking :: panic :: .ExpressionPathList ( const "assertion failed: num == 42" , .OperandList ) ; } bb2 : { .Statements return ; } .BasicBlockList } .Mir
9+
=>
10+
#halt ~> .
11+
</k>
12+
<callStack> .List </callStack>
13+
<returncode> 4 => 0 </returncode>
14+
<phase> Initialization => Finalization </phase>
15+
<functions>
16+
.Bag
17+
=>
18+
<function>
19+
<fnKey> Fn(main) </fnKey>
20+
<localDecls>
21+
<localDecl>
22+
<index> _0 </index>
23+
<ty> ( ) </ty>
24+
<value> Unit </value>
25+
...
26+
</localDecl>
27+
<localDecl>
28+
<index> _1 </index>
29+
<ty> i32 </ty>
30+
<value> 42 </value>
31+
...
32+
</localDecl>
33+
<localDecl>
34+
<index> _2 </index>
35+
<ty> bool </ty>
36+
<value> false </value>
37+
...
38+
</localDecl>
39+
<localDecl>
40+
<index> _3 </index>
41+
<ty> bool </ty>
42+
<value> true </value>
43+
...
44+
</localDecl>
45+
<localDecl>
46+
<index> _4 </index>
47+
<ty> ! </ty>
48+
<value> Never </value>
49+
...
50+
</localDecl>
51+
...
52+
</localDecls>
53+
<basicBlocks>
54+
<basicBlock>
55+
<bbName> 0 </bbName>
56+
<bbBody> ?_ </bbBody>
57+
</basicBlock>
58+
<basicBlock>
59+
<bbName> 1 </bbName>
60+
<bbBody> ?_ </bbBody>
61+
</basicBlock>
62+
<basicBlock>
63+
<bbName> 2 </bbName>
64+
<bbBody> ?_ </bbBody>
65+
</basicBlock>
66+
</basicBlocks>
67+
</function>
68+
</functions>
69+
70+
endmodule

‎kmir/src/tests/integration/test-data/prove-rs/assert.mir‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
// WARNING: This output format is intended for human consumers only
2+
// and is subject to change without notice. Knock yourself out.
3+
fn main() -> () {
4+
let mut _0: ();
5+
let _1: i32;
6+
let mut _2: bool;
7+
let mut _3: bool;
8+
let mut _4: !;
9+
scope 1 {
10+
debug num => _1;
11+
}
12+
13+
bb0: {
14+
_1 = Add(const 20_i32, const 22_i32);
15+
_3 = Eq(_1, const 42_i32);
16+
_2 = Not(move _3);
17+
switchInt(move _2) -> [0: bb2, otherwise: bb1];
18+
}
19+
20+
bb1: {
21+
_4 = core::panicking::panic(const "assertion failed: num == 42");
22+
}
23+
24+
bb2: {
25+
return;
26+
}
27+
}

‎kmir/src/tests/integration/test-data/prove-rs/assert.rs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
fn main() {
2+
let num = 20 + 22;
3+
assert!(num == 42);
4+
}

‎kmir/src/tests/integration/test-data/prove-rs/functions.k‎

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
requires "verify.k"
2+
3+
module FUNCTIONS
4+
imports VERIFY
5+
6+
claim [function]:
7+
<k>
8+
fn add :: .FunctionPath ( _1 : i32 , _2 : i32 , .ParameterList ) -> i32 { debug a => _1 ; debug b => _2 ; .DebugList let mut _0 : i32 ; .BindingList .ScopeList bb0 : { _0 = Add ( _1 , _2 ) ; .Statements return ; } .BasicBlockList } fn main :: .FunctionPath ( .ParameterList ) -> ( ) { .DebugList let mut _0 : ( ) ; let _1 : i32 ; let mut _2 : bool ; let mut _3 : bool ; let mut _4 : i32 ; let mut _5 : ! ; .BindingList scope 1 { debug ans => _1 ; .DebugList .BindingList .ScopeList } .ScopeList bb0 : { .Statements _1 = add :: .ExpressionPathList ( const 20_i32 , const 22_i32 , .OperandList ) -> bb1 ; } bb1 : { _4 = _1 ; _3 = Eq ( const 42_i32 , move _4 ) ; _2 = Not ( move _3 ) ; .Statements switchInt ( move _2 ) -> [ 0 : bb3 , .SwitchTargets , otherwise : bb2 ] ; } bb2 : { .Statements _5 = core :: panicking :: panic :: .ExpressionPathList ( const "assertion failed: 42 == ans" , .OperandList ) ; } bb3 : { .Statements return ; } .BasicBlockList } .Mir
9+
=>
10+
#halt ~> .
11+
</k>
12+
<callStack> .List </callStack>
13+
<returncode> 4 => 0 </returncode>
14+
<phase> Initialization => Finalization </phase>
15+
<functions>
16+
.Bag
17+
=>
18+
<function>
19+
<fnKey> Fn(main) </fnKey>
20+
<localDecls>
21+
<localDecl>
22+
<index> _0 </index>
23+
<ty> ( ) </ty>
24+
<value> Unit </value>
25+
...
26+
</localDecl>
27+
<localDecl>
28+
<index> _1 </index>
29+
<ty> i32 </ty>
30+
<value> 42 </value>
31+
...
32+
</localDecl>
33+
<localDecl>
34+
<index> _2 </index>
35+
<ty> bool </ty>
36+
<value> ?_ </value>
37+
...
38+
</localDecl>
39+
<localDecl>
40+
<index> _3 </index>
41+
<ty> bool </ty>
42+
<value> true </value>
43+
...
44+
</localDecl>
45+
<localDecl>
46+
<index> _4 </index>
47+
<ty> i32 </ty>
48+
<value> 42 </value>
49+
...
50+
</localDecl>
51+
<localDecl>
52+
<index> _5 </index>
53+
<ty> ! </ty>
54+
<value> ?_ </value>
55+
...
56+
</localDecl>
57+
</localDecls>
58+
<basicBlocks>
59+
<basicBlock>
60+
<bbName> 0 </bbName>
61+
<bbBody> ?_ </bbBody>
62+
</basicBlock>
63+
<basicBlock>
64+
<bbName> 1 </bbName>
65+
<bbBody> ?_ </bbBody>
66+
</basicBlock>
67+
<basicBlock>
68+
<bbName> 2 </bbName>
69+
<bbBody> ?_ </bbBody>
70+
</basicBlock>
71+
<basicBlock>
72+
<bbName> 3 </bbName>
73+
<bbBody> ?_ </bbBody>
74+
</basicBlock>
75+
</basicBlocks>
76+
</function>
77+
<function>
78+
<fnKey> Fn(add :: .FunctionPath) </fnKey>
79+
<localDecls>
80+
<localDecl>
81+
<index> _0 </index>
82+
<ty> i32 </ty>
83+
<value> 42 </value>
84+
...
85+
</localDecl>
86+
<localDecl>
87+
<index> _1 </index>
88+
<ty> i32 </ty>
89+
<value> ?_ </value>
90+
...
91+
</localDecl>
92+
<localDecl>
93+
<index> _2 </index>
94+
<ty> ?_ </ty>
95+
<value> ?_ </value>
96+
...
97+
</localDecl>
98+
</localDecls>
99+
<basicBlocks>
100+
<basicBlock>
101+
<bbName> 0 </bbName>
102+
<bbBody> ?_ </bbBody>
103+
</basicBlock>
104+
</basicBlocks>
105+
</function>
106+
</functions>
107+
108+
endmodule

‎kmir/src/tests/integration/test-data/prove-rs/functions.mir‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
// WARNING: This output format is intended for human consumers only
2+
// and is subject to change without notice. Knock yourself out.
3+
fn add(_1: i32, _2: i32) -> i32 {
4+
debug a => _1;
5+
debug b => _2;
6+
let mut _0: i32;
7+
8+
bb0: {
9+
_0 = Add(_1, _2);
10+
return;
11+
}
12+
}
13+
14+
fn main() -> () {
15+
let mut _0: ();
16+
let _1: i32;
17+
let mut _2: bool;
18+
let mut _3: bool;
19+
let mut _4: i32;
20+
let mut _5: !;
21+
scope 1 {
22+
debug ans => _1;
23+
}
24+
25+
bb0: {
26+
_1 = add(const 20_i32, const 22_i32) -> bb1;
27+
}
28+
29+
bb1: {
30+
_4 = _1;
31+
_3 = Eq(const 42_i32, move _4);
32+
_2 = Not(move _3);
33+
switchInt(move _2) -> [0: bb3, otherwise: bb2];
34+
}
35+
36+
bb2: {
37+
_5 = core::panicking::panic(const "assertion failed: 42 == ans");
38+
}
39+
40+
bb3: {
41+
return;
42+
}
43+
}

0 commit comments

Comments
 (0)