Skip to content

Commit 21261b0

Browse files
tothtamas28tothtamas28
authored
Seed the pseudorandom number generator for random execution (#783)
Blocked on: * ~runtimeverification/k#4874~
1 parent 65c6476 commit 21261b0

23 files changed

+48
-41
lines changed

‎kmir/src/kmir/kast.py‎

Lines changed: 24 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,13 @@
22

33
import logging
44
from itertools import count
5+
from random import Random
56
from typing import TYPE_CHECKING, NamedTuple
67

7-
from pyk.kast.inner import KApply, KSort, KVariable, Subst, build_cons
8+
from pyk.kast.inner import KApply, KSequence, KSort, KVariable, Subst, build_cons
89
from pyk.kast.manip import free_vars, split_config_from
910
from pyk.kast.prelude.collections import list_empty, list_of
10-
from pyk.kast.prelude.kint import eqInt, leInt
11+
from pyk.kast.prelude.kint import eqInt, intToken, leInt
1112
from pyk.kast.prelude.ml import mlEqualsTrue
1213
from pyk.kast.prelude.utils import token
1314

@@ -29,7 +30,6 @@
2930

3031
if TYPE_CHECKING:
3132
from collections.abc import Iterable, Iterator, Mapping, Sequence
32-
from random import Random
3333
from typing import Any, Final
3434

3535
from pyk.kast import KInner
@@ -56,7 +56,7 @@ class SymbolicMode(NamedTuple): ...
5656

5757

5858
class RandomMode(NamedTuple):
59-
random: Random
59+
seed: int
6060

6161

6262
CallConfigMode = ConcreteMode | SymbolicMode | RandomMode
@@ -89,12 +89,12 @@ def make_call_config(
8989
types=smir_info.types,
9090
)
9191
return CallConfig(config=config, constraints=tuple(constraints))
92-
case RandomMode(random):
92+
case RandomMode(seed):
9393
config = _make_random_call_config(
9494
definition=definition,
9595
fn_data=fn_data,
9696
types=smir_info.types,
97-
random=random,
97+
seed=seed,
9898
)
9999
return CallConfig(config=config, constraints=())
100100

@@ -148,6 +148,7 @@ def _make_concrete_call_config(
148148
definition=definition,
149149
fn_data=fn_data,
150150
localvars=[],
151+
seed=None,
151152
)
152153

153154

@@ -156,13 +157,14 @@ def _make_random_call_config(
156157
definition: KDefinition,
157158
fn_data: _FunctionData,
158159
types: Mapping[Ty, TypeMetadata],
159-
random: Random,
160+
seed: int,
160161
) -> KInner:
161-
localvars = _random_locals(random, fn_data.args, types)
162+
localvars = _random_locals(Random(seed), fn_data.args, types)
162163
return _make_concrete_call_config_with_locals(
163164
definition=definition,
164165
fn_data=fn_data,
165166
localvars=localvars,
167+
seed=seed,
166168
)
167169

168170

@@ -171,23 +173,35 @@ def _make_concrete_call_config_with_locals(
171173
definition: KDefinition,
172174
fn_data: _FunctionData,
173175
localvars: list[KInner],
176+
seed: int | None,
174177
) -> KInner:
175178
def init_subst() -> dict[str, KInner]:
176179
init_config = definition.init_config(KSort('GeneratedTopCell'))
177180
_, res = split_config_from(init_config)
178181
return res
179182

180-
# The configuration is the default initial configuration, with the K cell updated with the call terminator
183+
# The configuration is the default initial configuration,
184+
# with the K cell updated with the call terminator (and with an srandInt call, if seed is set)
181185
# TODO: see if this can be expressed in more simple terms
186+
187+
k_cell = fn_data.call_terminator
188+
if seed is not None:
189+
# Seed the pseudorandom generator. This is necessary for cheatcode use in concrete execution.
190+
k_cell = KSequence(
191+
KApply('srandInt(_)_INT-COMMON_K_Int', intToken(seed)),
192+
k_cell,
193+
)
194+
182195
subst = Subst(
183196
{
184197
**init_subst(),
185198
**{
186-
'K_CELL': fn_data.call_terminator,
199+
'K_CELL': k_cell,
187200
'LOCALS_CELL': list_of(localvars),
188201
},
189202
}
190203
)
204+
191205
empty_config = definition.empty_config(KSort('GeneratedTopCell'))
192206
config = subst(empty_config)
193207
assert not free_vars(config), f'Config by construction should not have any free variables: {config}'

‎kmir/src/kmir/kmir.py‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@
2828

2929
if TYPE_CHECKING:
3030
from collections.abc import Iterator
31-
from random import Random
3231
from typing import Final
3332

3433
from pyk.cterm.show import CTermShow
@@ -93,10 +92,10 @@ def run_smir(
9392
*,
9493
start_symbol: str = 'main',
9594
depth: int | None = None,
96-
random: Random | None = None,
95+
seed: int | None = None,
9796
) -> Pattern:
9897
smir_info = smir_info.reduce_to(start_symbol)
99-
mode = RandomMode(random) if random else ConcreteMode()
98+
mode = RandomMode(seed) if seed else ConcreteMode()
10099
init_config, _ = make_call_config(
101100
self.definition,
102101
smir_info=smir_info,

‎kmir/src/tests/integration/data/run-smir-random/complex-types/init-0.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
3+
srandInt ( 0 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn

‎kmir/src/tests/integration/data/run-smir-random/complex-types/init-1.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
3+
srandInt ( 1 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn

‎kmir/src/tests/integration/data/run-smir-random/complex-types/init-2.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
3+
srandInt ( 2 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn

‎kmir/src/tests/integration/data/run-smir-random/complex-types/init-3.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
3+
srandInt ( 3 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn

‎kmir/src/tests/integration/data/run-smir-random/complex-types/init-4.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
3+
srandInt ( 4 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn

‎kmir/src/tests/integration/data/run-smir-random/complex-types/init-5.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
3+
srandInt ( 5 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn

‎kmir/src/tests/integration/data/run-smir-random/complex-types/init-6.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
3+
srandInt ( 6 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn

‎kmir/src/tests/integration/data/run-smir-random/complex-types/init-7.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<kmir>
22
<k>
3-
#execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
3+
srandInt ( 7 ) ~> #execTerminator ( terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 0 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( -2 ) , id: mirConstId ( 0 ) ) ) ) , args: operandCopy ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionContinue ) , span: span ( 0 ) ) ) ~> .K
44
</k>
55
<retVal>
66
noReturn

0 commit comments

Comments
 (0)