Skip to content

Commit f69d23a

Browse files
ehildenbrv-auditor
andauthored
Enable thunking #applyUnOp (#595)
A couple of programs were getting stuck at `#applyUnOp` for unimplemented operations, this enables thunking unary operations. In particular: - `#applyUnOp` is put in sort `Evaluation` so that thunking can happen. - `#compute` is renamed to `#applyBinOp`. - The P-token test is limited to 7 iterations of the prover maximum to keep it from running too long (arbitrary limit, still takes about 10 minutes). - Test output is updated: there are 2 tests where the rename `#compute => #applyBinOp` has an effect, and 2 where we get further into execution of programs because we thunk up `#applyUnOp` (including the P-token test). --------- Co-authored-by: devops <[email protected]>
1 parent 0ef9cf8 commit f69d23a

File tree

10 files changed

+2385
-418
lines changed

10 files changed

+2385
-418
lines changed

kmir/pyproject.toml

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

55
[project]
66
name = "kmir"
7-
version = "0.3.172"
7+
version = "0.3.173"
88
description = ""
99
requires-python = "~=3.10"
1010
dependencies = [

kmir/src/kmir/__init__.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
from typing import Final
22

3-
VERSION: Final = '0.3.172'
3+
VERSION: Final = '0.3.173'

kmir/src/kmir/kdist/mir-semantics/rt/data.md

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -894,20 +894,20 @@ This is specific to Stable MIR, the MIR AST instead uses `<OP>WithOverflow` as t
894894

895895
[^checkedbinaryop]: See [description in `stable_mir` crate](https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/enum.Rvalue.html#variant.CheckedBinaryOp) and the difference between [MIR `BinOp`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.BinOp.html) and its [Stable MIR correspondent](https://doc.rust-lang.org/nightly/nightly-rustc/stable_mir/mir/enum.BinOp.html).
896896

897-
For binary operations generally, both arguments have to be read from the provided operands, followed by checking the types and then performing the actual operation (both implemented in `#compute`), which can return a `TypedLocal` or an error. A flag carries the information whether to perform an overflow check through to this function for `CheckedBinaryOp`.
897+
For binary operations generally, both arguments have to be read from the provided operands, followed by checking the types and then performing the actual operation (both implemented in `#applyBinOp`), which can return a `TypedLocal` or an error. A flag carries the information whether to perform an overflow check through to this function for `CheckedBinaryOp`.
898898

899899
```k
900-
syntax Evaluation ::= #compute ( BinOp, Evaluation, Evaluation, Bool) [seqstrict(2,3)]
900+
syntax Evaluation ::= #applyBinOp ( BinOp, Evaluation, Evaluation, Bool) [seqstrict(2,3)]
901901
902-
rule <k> rvalueBinaryOp(BINOP, OP1, OP2) => #compute(BINOP, OP1, OP2, false) ... </k>
902+
rule <k> rvalueBinaryOp(BINOP, OP1, OP2) => #applyBinOp(BINOP, OP1, OP2, false) ... </k>
903903
904-
rule <k> rvalueCheckedBinaryOp(BINOP, OP1, OP2) => #compute(BINOP, OP1, OP2, true) ... </k>
904+
rule <k> rvalueCheckedBinaryOp(BINOP, OP1, OP2) => #applyBinOp(BINOP, OP1, OP2, true) ... </k>
905905
```
906906

907907
There are also a few _unary_ operations (`UnOpNot`, `UnOpNeg`, `UnOpPtrMetadata`) used in `RValue:UnaryOp`. These operations only read a single operand and do not need a `#suspend` helper.
908908

909909
```k
910-
syntax KItem ::= #applyUnOp ( UnOp , Evaluation ) [strict(2)]
910+
syntax Evaluation ::= #applyUnOp ( UnOp , Evaluation ) [strict(2)]
911911
912912
rule <k> rvalueUnaryOp(UNOP, OP1) => #applyUnOp(UNOP, OP1) ... </k>
913913
```
@@ -961,7 +961,7 @@ The arithmetic operations require operands of the same numeric type.
961961
962962
// Checked operations return a pair of the truncated value and an overflow flag
963963
// signed numbers: must check for wrap-around (operation specific)
964-
rule #compute(
964+
rule #applyBinOp(
965965
BOP,
966966
typedValue(Integer(ARG1, WIDTH, true), TY, _), //signed
967967
typedValue(Integer(ARG2, WIDTH, true), TY, _),
@@ -989,7 +989,7 @@ The arithmetic operations require operands of the same numeric type.
989989
[preserves-definedness]
990990
991991
// unsigned numbers: simple overflow check using a bit mask
992-
rule #compute(
992+
rule #applyBinOp(
993993
BOP,
994994
typedValue(Integer(ARG1, WIDTH, false), TY, _), // unsigned
995995
typedValue(Integer(ARG2, WIDTH, false), TY, _),
@@ -1018,7 +1018,7 @@ The arithmetic operations require operands of the same numeric type.
10181018
10191019
// Unchecked operations signal undefined behaviour on overflow. The checks are the same as for the flags above.
10201020
1021-
rule #compute(
1021+
rule #applyBinOp(
10221022
BOP,
10231023
typedValue(Integer(ARG1, WIDTH, true), TY, _), // signed
10241024
typedValue(Integer(ARG2, WIDTH, true), TY, _),
@@ -1030,7 +1030,7 @@ The arithmetic operations require operands of the same numeric type.
10301030
[preserves-definedness]
10311031
10321032
// unsigned numbers: simple overflow check using a bit mask
1033-
rule #compute(
1033+
rule #applyBinOp(
10341034
BOP,
10351035
typedValue(Integer(ARG1, WIDTH, false), TY, _), // unsigned
10361036
typedValue(Integer(ARG2, WIDTH, false), TY, _),
@@ -1079,13 +1079,13 @@ All operations except `binOpCmp` return a `BoolVal`. The argument types must be
10791079
// * arguments must have the same type
10801080
// * arguments must be numbers or Bool
10811081
1082-
rule #compute(OP, typedValue(Integer(VAL1, WIDTH, SIGN), TY, _), typedValue(Integer(VAL2, WIDTH, SIGN), TY, _), _)
1082+
rule #applyBinOp(OP, typedValue(Integer(VAL1, WIDTH, SIGN), TY, _), typedValue(Integer(VAL2, WIDTH, SIGN), TY, _), _)
10831083
=>
10841084
typedValue(BoolVal(cmpOpInt(OP, VAL1, VAL2)), TyUnknown, mutabilityNot)
10851085
requires isComparison(OP)
10861086
[preserves-definedness] // OP known to be a comparison
10871087
1088-
rule #compute(OP, typedValue(BoolVal(VAL1), TY, _), typedValue(BoolVal(VAL2), TY, _), _)
1088+
rule #applyBinOp(OP, typedValue(BoolVal(VAL1), TY, _), typedValue(BoolVal(VAL2), TY, _), _)
10891089
=>
10901090
typedValue(BoolVal(cmpOpBool(OP, VAL1, VAL2)), TyUnknown, mutabilityNot)
10911091
requires isComparison(OP)
@@ -1105,11 +1105,11 @@ The `binOpCmp` operation returns `-1`, `0`, or `+1` (the behaviour of Rust's `st
11051105
rule cmpBool(X, Y) => 0 requires X ==Bool Y
11061106
rule cmpBool(X, Y) => 1 requires X andBool notBool Y
11071107
1108-
rule #compute(binOpCmp, typedValue(Integer(VAL1, WIDTH, SIGN), TY, _), typedValue(Integer(VAL2, WIDTH, SIGN), TY, _), _)
1108+
rule #applyBinOp(binOpCmp, typedValue(Integer(VAL1, WIDTH, SIGN), TY, _), typedValue(Integer(VAL2, WIDTH, SIGN), TY, _), _)
11091109
=>
11101110
typedValue(Integer(cmpInt(VAL1, VAL2), 8, true), TyUnknown, mutabilityNot)
11111111
1112-
rule #compute(binOpCmp, typedValue(BoolVal(VAL1), TY, _), typedValue(BoolVal(VAL2), TY, _), _)
1112+
rule #applyBinOp(binOpCmp, typedValue(BoolVal(VAL1), TY, _), typedValue(BoolVal(VAL2), TY, _), _)
11131113
=>
11141114
typedValue(Integer(cmpBool(VAL1, VAL2), 8, true), TyUnknown, mutabilityNot)
11151115
```
@@ -1197,7 +1197,7 @@ Shifts are valid on integers if the right argument (the shift amount) is strictl
11971197
rule onShift(binOpShlUnchecked, X, Y, WIDTH) => (X <<Int Y) modInt (1 <<Int WIDTH)
11981198
rule onShift(binOpShrUnchecked, X, Y, WIDTH) => (X >>Int Y) modInt (1 <<Int WIDTH)
11991199
1200-
rule #compute(
1200+
rule #applyBinOp(
12011201
BOP,
12021202
typedValue(Integer(ARG1, WIDTH, SIGNED), TY, _),
12031203
typedValue(Integer(ARG2, WIDTH, SIGNED), TY, _),
@@ -1211,7 +1211,7 @@ Shifts are valid on integers if the right argument (the shift amount) is strictl
12111211
requires isBitwise(BOP)
12121212
[preserves-definedness]
12131213
1214-
rule #compute(
1214+
rule #applyBinOp(
12151215
BOP,
12161216
typedValue(BoolVal(ARG1), TY, _),
12171217
typedValue(BoolVal(ARG2), TY, _),
@@ -1225,7 +1225,7 @@ Shifts are valid on integers if the right argument (the shift amount) is strictl
12251225
requires isBitwise(BOP)
12261226
[preserves-definedness]
12271227
1228-
rule #compute(
1228+
rule #applyBinOp(
12291229
BOP,
12301230
typedValue(Integer(ARG1, WIDTH, false), TY, _),
12311231
typedValue(Integer(ARG2, _, _), _, _),
@@ -1239,7 +1239,7 @@ Shifts are valid on integers if the right argument (the shift amount) is strictl
12391239
requires isShift(BOP) andBool ((notBool isUncheckedShift(BOP)) orBool ARG2 <Int WIDTH)
12401240
[preserves-definedness]
12411241
1242-
rule #compute(
1242+
rule #applyBinOp(
12431243
BOP,
12441244
typedValue(Integer(ARG1, WIDTH, true), TY, _),
12451245
typedValue(Integer(ARG2, _, _), _, _),

kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
66
│ (137 steps)
77
├─ 3
8-
│ #expect ( typedValue ( thunk ( #compute ( binOpEq , typedValue ( thunk ( #comput
8+
│ #expect ( typedValue ( thunk ( #applyBinOp ( binOpEq , typedValue ( thunk ( #app
99
│ function: main
1010
1111
┃ (1 step)

kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
66
│ (93 steps)
77
├─ 3
8-
│ #expect ( typedValue ( thunk ( #compute ( binOpEq , typedValue ( thunk ( #comput
8+
│ #expect ( typedValue ( thunk ( #applyBinOp ( binOpEq , typedValue ( thunk ( #app
99
│ function: main
1010
1111
┃ (1 step)

kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.expected

Lines changed: 64 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,38 @@
1515
┃ ├─ 4
1616
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) )
1717
┃ │
18-
┃ │ (16 steps)
19-
┃ └─ 6 (stuck, leaf)
20-
┃ #applyUnOp ( unOpPtrMetadata , typedValue ( Reference ( 0 , place ( ... local: l
21-
┃ span: 59
18+
┃ │ (37 steps)
19+
┃ ├─ 6
20+
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 7 ) )
21+
┃ ┃
22+
┃ ┃ (1 step)
23+
┃ ┣━━┓
24+
┃ ┃ │
25+
┃ ┃ ├─ 8
26+
┃ ┃ │ #execBlockIdx ( basicBlockIdx ( 7 ) ) ~> .K
27+
┃ ┃ │
28+
┃ ┃ │ (4 steps)
29+
┃ ┃ ├─ 14 (terminal)
30+
┃ ┃ │ #EndProgram ~> .K
31+
┃ ┃ │
32+
┃ ┃ ┊ constraint: true
33+
┃ ┃ ┊ subst: ...
34+
┃ ┃ └─ 2 (leaf, target, terminal)
35+
┃ ┃ #EndProgram ~> .K
36+
┃ ┃
37+
┃ ┣━━┓
38+
┃ ┃ │
39+
┃ ┃ ├─ 9
40+
┃ ┃ │ #selectBlock ( switchTargets ( ... branches: .Branches , otherwise: basicBlockId
41+
┃ ┃ │
42+
┃ ┃ │ (85 steps)
43+
┃ ┃ └─ 15 (vacuous, leaf)
44+
┃ ┃ #expect ( typedValue ( BoolVal ( 0 <Int size ( ARG_ARRAY7:List ) ) , ty ( 28 ) ,
45+
┃ ┃
46+
┃ ┗━━┓
47+
┃ │
48+
┃ └─ 10 (stuck, leaf)
49+
┃ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 7 ) )
2250
2351
┗━━┓ subst: .Subst
2452
┃ constraint:
@@ -27,13 +55,38 @@
2755
├─ 5
2856
│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 3 ) )
2957
30-
│ (66 steps)
31-
└─ 7 (stuck, leaf)
32-
#applyUnOp ( unOpPtrMetadata , typedValue ( Reference ( 0 , place ( ... local: l
33-
span: 59
58+
│ (87 steps)
59+
├─ 7
60+
│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 7 ) )
61+
62+
┃ (1 step)
63+
┣━━┓
64+
┃ │
65+
┃ ├─ 11
66+
┃ │ #execBlockIdx ( basicBlockIdx ( 7 ) ) ~> .K
67+
┃ │
68+
┃ │ (4 steps)
69+
┃ ├─ 16 (terminal)
70+
┃ │ #EndProgram ~> .K
71+
┃ │
72+
┃ ┊ constraint: true
73+
┃ ┊ subst: ...
74+
┃ └─ 2 (leaf, target, terminal)
75+
┃ #EndProgram ~> .K
76+
77+
┣━━┓
78+
┃ │
79+
┃ ├─ 12
80+
┃ │ #selectBlock ( switchTargets ( ... branches: .Branches , otherwise: basicBlockId
81+
┃ │
82+
┃ │ (85 steps)
83+
┃ └─ 17 (vacuous, leaf)
84+
┃ #expect ( typedValue ( BoolVal ( 0 <Int size ( ARG_ARRAY7:List ) ) , ty ( 28 ) ,
85+
86+
┗━━┓
87+
88+
└─ 13 (stuck, leaf)
89+
#selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 7 ) )
3490

3591

36-
┌─ 2 (root, leaf, target, terminal)
37-
│ #EndProgram ~> .K
38-
3992

0 commit comments

Comments
 (0)