FazBrowse GitHub Viewer
|
Trending
|
URL:
|
Home
Tools:
[Download Repo ZIP]
[View Raw Code]
[Original HTTPS Page]
java-smt/src/org/sosy_lab/java_smt/test/Fuzzer.java at master · sosy-lab/java-smt · GitHub
sosy-lab
java-smt
Repository navigation
Code
Issues
114
(114)
Pull requests
43
(43)
Discussions
Actions
Security and quality
Insights
Expand file tree
Breadcrumbs
java-smt
/
src
/
org
/
sosy_lab
/
java_smt
/
test
/
Fuzzer.java
Copy path
More file actions
More file actions
Latest commit
History
History
History
79 lines (64 loc) · 2.18 KB
Breadcrumbs
java-smt
/
src
/
org
/
sosy_lab
/
java_smt
/
test
/
Fuzzer.java
Copy path
File metadata and controls
79 lines (64 loc) · 2.18 KB
Raw
Copy raw file
Download raw file
Open symbols panel
Edit and raw actions
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
// This file is part of JavaSMT,
// an API wrapper for a collection of SMT solvers:
// https://github.com/sosy-lab/java-smt
//
// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
//
// SPDX-License-Identifier: Apache-2.0
package
org
.
sosy_lab
.
java_smt
.
test
;
import
java
.
util
.
Random
;
import
org
.
sosy_lab
.
common
.
UniqueIdGenerator
;
import
org
.
sosy_lab
.
java_smt
.
api
.
BooleanFormula
;
import
org
.
sosy_lab
.
java_smt
.
api
.
BooleanFormulaManager
;
import
org
.
sosy_lab
.
java_smt
.
api
.
FormulaManager
;
/** Boolean fuzzer, useful for testing. */
class
Fuzzer
{
private
final
BooleanFormulaManager
bfmgr
;
private
final
UniqueIdGenerator
idGenerator
;
private
BooleanFormula
[]
vars
=
new
BooleanFormula
[
0
];
private
final
Random
r
;
private
static
final
String
varNameTemplate
=
"VAR_"
;
Fuzzer
(
FormulaManager
pFmgr
,
Random
pRandom
) {
bfmgr
=
pFmgr
.
getBooleanFormulaManager
();
idGenerator
=
new
UniqueIdGenerator
();
r
=
pRandom
;
}
public
BooleanFormula
fuzz
(
int
formulaSize
,
int
maxNoVars
) {
vars
=
new
BooleanFormula
[
maxNoVars
];
populateVars
();
return
recFuzz
(
formulaSize
);
}
public
BooleanFormula
fuzz
(
int
formulaSize
,
BooleanFormula
...
pVars
) {
vars
=
pVars
;
return
recFuzz
(
formulaSize
);
}
private
BooleanFormula
recFuzz
(
int
formulaSize
) {
if
(
formulaSize
==
1
) {
// The only combination of size 1.
return
getVar
();
}
else
if
(
formulaSize
==
2
) {
// The only combination of size 2.
return
bfmgr
.
not
(
getVar
());
}
else
{
formulaSize
-=
1
;
int
pivot
=
formulaSize
/
2
;
return
switch
(
r
.
nextInt
(
3
)) {
case
0
->
bfmgr
.
or
(
recFuzz
(
pivot
),
recFuzz
(
formulaSize
-
pivot
));
case
1
->
bfmgr
.
and
(
recFuzz
(
pivot
),
recFuzz
(
formulaSize
-
pivot
));
case
2
->
bfmgr
.
not
(
recFuzz
(
formulaSize
));
default
->
throw
new
UnsupportedOperationException
(
"Unexpected state"
);
};
}
}
private
BooleanFormula
getVar
() {
return
vars
[
r
.
nextInt
(
vars
.
length
)];
}
private
void
populateVars
() {
for
(
int
i
=
0
;
i
<
vars
.
length
;
i
++) {
vars
[
i
] =
getNewVar
();
}
}
private
BooleanFormula
getNewVar
() {
return
bfmgr
.
makeVariable
(
varNameTemplate
+
idGenerator
.
getFreshId
());
}
}
Back
|
FazBrowse Home
|
New Git URL