Skip to content

Commit eb7822f

Browse files
author
Saveliy Grigoryev
committed
Add support symbolic input/output for C
1 parent 05a4baa commit eb7822f

File tree

14 files changed

+800
-27
lines changed

14 files changed

+800
-27
lines changed

‎integration-tests/c-example/lib/input_output/input_output.c

Lines changed: 186 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,186 @@
1+
#include <stdio.h>
2+
#include "input_output.h"
3+
4+
int simple_getc() {
5+
unsigned char a = getc(stdin);
6+
if (a == '0') {
7+
return 0;
8+
} else if (a == '1') {
9+
return 1;
10+
} else if (a == '2') {
11+
return 2;
12+
} else if (a == '3') {
13+
return 3;
14+
} else if (a == '4') {
15+
return 4;
16+
} else if (a == '5') {
17+
return 5;
18+
} else if (a == '6') {
19+
return 6;
20+
} else if (a == '7') {
21+
return 7;
22+
} else if (a == '8') {
23+
return 8;
24+
} else if (a == '9') {
25+
return 9;
26+
}
27+
return -1;
28+
}
29+
30+
int simple_fgetc(int x) {
31+
if (x >= 0 && x <= 9) {
32+
unsigned char a = fgetc(stdin);
33+
if (a >= 'a' && a <= 'z') {
34+
return 1;
35+
} else {
36+
return 2;
37+
}
38+
} else {
39+
unsigned char a = fgetc(stdin);
40+
unsigned char b = fgetc(stdin);
41+
if (a >= 'a' && a <= 'z') {
42+
if (b >= '0' && b <= '9') {
43+
return 3;
44+
} else {
45+
return 4;
46+
}
47+
} else {
48+
return 5;
49+
}
50+
}
51+
}
52+
53+
int simple_fread() {
54+
int arrA[4];
55+
int arrB[4];
56+
fread(arrA, sizeof(int), 4, stdin);
57+
fread(arrB, sizeof(int), 4, stdin);
58+
59+
int sumA = 0, sumB = 0;
60+
for (int i = 0; i < 4; i++) {
61+
sumA += arrA[i];
62+
sumB += arrB[i];
63+
}
64+
if (sumA == sumB) {
65+
return 0;
66+
} else if (sumA > sumB) {
67+
return 1;
68+
} else {
69+
return -1;
70+
}
71+
}
72+
73+
int simple_fgets() {
74+
char a[8];
75+
fgets(a, 6, stdin);
76+
if (a[0] == 'u' && a[1] == 't' && a[2] == 'b' && a[3] == 'o' && a[4] == 't') {
77+
return 1;
78+
}
79+
return 0;
80+
}
81+
82+
int simple_getchar() {
83+
unsigned char a = getchar();
84+
unsigned char b = getchar();
85+
86+
if (a + b < 0) {
87+
return -1;
88+
}
89+
90+
if (a + b < 100) {
91+
return 0;
92+
} else if (a + b < 200) {
93+
return 1;
94+
} else {
95+
return 2;
96+
}
97+
}
98+
99+
int simple_gets() {
100+
char a[8];
101+
gets(a);
102+
if (a[0] == 'u' && a[1] == 't' && a[2] == 'b' && a[3] == 'o' && a[4] == 't') {
103+
return 1;
104+
}
105+
return 0;
106+
}
107+
108+
char simple_putc(int x, int y) {
109+
if (x + y > 0) {
110+
putc('1', stdout);
111+
return '1';
112+
} else if (x + y < 0) {
113+
putc('2', stdout);
114+
return '2';
115+
} else {
116+
putc('0', stdout);
117+
return '0';
118+
}
119+
}
120+
121+
char simple_fputc(int x, int y) {
122+
if (x < y) {
123+
fputc('<', stdout);
124+
return '<';
125+
} else if (x > y) {
126+
fputc('>', stdout);
127+
return '>';
128+
} else {
129+
fputc('=', stdout);
130+
return '=';
131+
}
132+
}
133+
134+
char simple_fwrite(int x) {
135+
if (x > 0) {
136+
char a[] = "Positive";
137+
fwrite(a, sizeof(char), 8, stdout);
138+
return 'P';
139+
} else if (x < 0) {
140+
char a[] = "Negative";
141+
fwrite(a, sizeof(char), 8, stdout);
142+
return 'N';
143+
} else {
144+
char a[] = "Zero";
145+
fwrite(a, sizeof(char), 4, stdout);
146+
return 'Z';
147+
}
148+
}
149+
150+
char simple_fputs(char c) {
151+
if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u') {
152+
char a[] = "Vowel";
153+
fputs("Vowel", stdout);
154+
return 'V';
155+
} else {
156+
char a[] = "Consonant";
157+
fputs("Consonant", stdout);
158+
return 'C';
159+
}
160+
}
161+
162+
char simple_putchar(int x, int y) {
163+
if (3 * x > 2 * y) {
164+
putchar('>');
165+
return '>';
166+
} else if (3 * x < 2 * y) {
167+
putchar('<');
168+
return '<';
169+
} else {
170+
putchar('=');
171+
return '=';
172+
}
173+
}
174+
175+
char simple_puts(char c) {
176+
if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u') {
177+
char a[] = "Vowel";
178+
puts(a);
179+
return 'V';
180+
} else {
181+
char a[] = "Consonant";
182+
puts(a);
183+
return 'C';
184+
}
185+
}
186+

‎integration-tests/c-example/lib/input_output/input_output.h

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
#ifndef INPUT_OUTPUT_H
2+
#define INPUT_OUTPUT_H
3+
4+
int simple_getc();
5+
6+
int simple_fgetc(int x);
7+
8+
int simple_fread();
9+
10+
int simple_fgets();
11+
12+
int simple_getchar();
13+
14+
int simple_gets();
15+
16+
char simple_putc(int x, int y);
17+
18+
char simple_fputc(int x, int y);
19+
20+
char simple_fwrite(int x);
21+
22+
char simple_fputs(char c);
23+
24+
char simple_putchar(int x, int y);
25+
26+
char simple_puts(char c);
27+
28+
#endif
29+

‎server/src/Tests.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -508,6 +508,7 @@ void KTestObjectParser::parseKTest(const MethodKtests &batch,
508508
bool filterByLineFlag,
509509
std::shared_ptr<LineInfo> lineInfo) {
510510
LOG_SCOPE_FUNCTION(DEBUG);
511+
sourceFilePath = tests.sourceFilePath;
511512
for (auto &[testMethod, testCases] : batch) {
512513
auto it = tests.methods.find<std::string, tests::Tests::MethodDescriptionToStringEqual>(
513514
testMethod.methodName);
@@ -852,9 +853,9 @@ KTestObjectParser::parseTestCaseParams(const UTBotKTest &ktest,
852853
processGlobalParamPostValue(testCaseDescription, globalParam, rawKleeParams);
853854
}
854855

855-
//We should turn off symbolic stdin, because it doesn't work correct with interactive mode
856-
//TODO: rewrite symbolic stdin, so that it can work with interactive mode
857-
//processSymbolicStdin(testCaseDescription, rawKleeParams);
856+
if (Paths::getSourceLanguage(sourceFilePath) == utbot::Language::C) {
857+
processSymbolicStdin(testCaseDescription, rawKleeParams);
858+
}
858859

859860
processStubParamValue(testCaseDescription, methodNameToReturnTypeMap, rawKleeParams);
860861
if (!types::TypesHandler::skipTypeInReturn(methodDescription.returnType)) {

‎server/src/Tests.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -569,6 +569,8 @@ namespace tests {
569569
bool filterByLineFlag,
570570
std::shared_ptr<LineInfo> lineInfo);
571571
private:
572+
fs::path sourceFilePath;
573+
572574
types::TypesHandler &typesHandler;
573575

574576
struct RawKleeParam {

‎server/src/printers/KleePrinter.cpp

Lines changed: 48 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,45 @@ printer::KleePrinter::KleePrinter(const types::TypesHandler *typesHandler,
3232
: Printer(srcLanguage), typesHandler(typesHandler), buildDatabase(std::move(buildDatabase)) {
3333
}
3434

35+
void KleePrinter::writePosixWrapper(const Tests &tests,
36+
const tests::Tests::MethodDescription &testMethod) {
37+
declTestEntryPoint(tests, testMethod, false);
38+
strFunctionCall(PrinterUtils::POSIX_INIT, {"&" + PrinterUtils::UTBOT_ARGC, "&" + PrinterUtils::UTBOT_ARGV});
39+
std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name, false, true);
40+
strDeclareVar("int", KleeUtils::RESULT_VARIABLE_NAME, constrFunctionCall(entryPoint,
41+
{PrinterUtils::UTBOT_ARGC, PrinterUtils::UTBOT_ARGV, PrinterUtils::UTBOT_ENVP},
42+
"", std::nullopt, false));
43+
strFunctionCall(PrinterUtils::POSIX_CHECK_STDIN_READ, {});
44+
strReturn(KleeUtils::RESULT_VARIABLE_NAME);
45+
closeBrackets(1);
46+
ss << NL;
47+
}
48+
49+
void KleePrinter::writeTestedFunction(const Tests &tests,
50+
const tests::Tests::MethodDescription &testMethod,
51+
const std::optional<LineInfo::PredicateInfo> &predicateInfo,
52+
const std::string &testedMethod,
53+
bool onlyForOneEntity,
54+
bool isWrapped) {
55+
writeStubsForFunctionParams(typesHandler, testMethod, true);
56+
declTestEntryPoint(tests, testMethod, isWrapped);
57+
genGlobalParamsDeclarations(testMethod);
58+
genParamsDeclarations(testMethod);
59+
genPostGlobalSymbolicVariables(testMethod);
60+
genPostParamsSymbolicVariables(testMethod);
61+
if (types::TypesHandler::skipTypeInReturn(testMethod.returnType)) {
62+
genVoidFunctionAssumes(testMethod, predicateInfo, testedMethod, onlyForOneEntity);
63+
} else {
64+
genNonVoidFunctionAssumes(testMethod, predicateInfo, testedMethod,
65+
onlyForOneEntity);
66+
}
67+
genGlobalsKleeAssumes(testMethod);
68+
genPostParamsKleeAssumes(testMethod);
69+
strReturn("0");
70+
closeBrackets(1);
71+
ss << NL;
72+
}
73+
3574
fs::path KleePrinter::writeTmpKleeFile(
3675
const Tests &tests,
3776
const std::string &buildDir,
@@ -92,22 +131,12 @@ fs::path KleePrinter::writeTmpKleeFile(
92131
continue;
93132
}
94133
try {
95-
writeStubsForFunctionParams(typesHandler, testMethod, true);
96-
declTestEntryPoint(tests, testMethod);
97-
genGlobalParamsDeclarations(testMethod);
98-
genParamsDeclarations(testMethod);
99-
genPostGlobalSymbolicVariables(testMethod);
100-
genPostParamsSymbolicVariables(testMethod);
101-
if (types::TypesHandler::skipTypeInReturn(testMethod.returnType)) {
102-
genVoidFunctionAssumes(testMethod, predicateInfo, testedMethod, onlyForOneEntity);
134+
if (srcLanguage == utbot::Language::C) {
135+
writeTestedFunction(tests, testMethod, predicateInfo, testedMethod, onlyForOneEntity, true);
136+
writePosixWrapper(tests, testMethod);
103137
} else {
104-
genNonVoidFunctionAssumes(testMethod, predicateInfo, testedMethod,
105-
onlyForOneEntity);
138+
writeTestedFunction(tests, testMethod, predicateInfo, testedMethod, onlyForOneEntity, false);
106139
}
107-
genGlobalsKleeAssumes(testMethod);
108-
genPostParamsKleeAssumes(testMethod);
109-
strReturn("0");
110-
closeBrackets(1);
111140
} catch (const UnImplementedException &e) {
112141
std::string message =
113142
"Could not generate klee code for method \'" + methodName + "\', skipping it. ";
@@ -121,11 +150,13 @@ fs::path KleePrinter::writeTmpKleeFile(
121150
}
122151

123152
void KleePrinter::declTestEntryPoint(const Tests &tests,
124-
const Tests::MethodDescription &testMethod) {
125-
std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name);
153+
const Tests::MethodDescription &testMethod,
154+
bool isWrapped) {
155+
std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name, false, isWrapped);
126156
auto argvType = types::Type::createSimpleTypeFromName("char", 2);
127157
// if change args in next line also change cpp mangledPath in kleeUtils.cpp
128-
strFunctionDecl("int", entryPoint, {types::Type::intType(), argvType, argvType}, {"utbot_argc", "utbot_argv", "utbot_envp"}, "") << LB();
158+
strFunctionDecl("int", entryPoint, {types::Type::intType(), argvType, argvType},
159+
{PrinterUtils::UTBOT_ARGC, PrinterUtils::UTBOT_ARGV, PrinterUtils::UTBOT_ENVP}, "") << LB();
129160
}
130161

131162
Tests::MethodParam KleePrinter::getKleeMethodParam(tests::Tests::MethodParam const &param) {

‎server/src/printers/KleePrinter.h

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ namespace printer {
5555
types::Type curType;
5656
};
5757

58-
void declTestEntryPoint(const Tests &tests, const Tests::MethodDescription &testMethod);
58+
void declTestEntryPoint(const Tests &tests, const Tests::MethodDescription &testMethod, bool isWrapped);
5959

6060
void genGlobalParamsDeclarations(const Tests::MethodDescription &testMethod);
6161

@@ -129,6 +129,16 @@ namespace printer {
129129
void genPostSymbolicVariable(const Tests::MethodDescription &testMethod, const Tests::MethodParam &param);
130130

131131
void genPostAssumes(const Tests::MethodParam &param, bool visitGlobal = false);
132+
133+
void writePosixWrapper(const Tests &tests,
134+
const tests::Tests::MethodDescription &testMethod);
135+
136+
void writeTestedFunction(const Tests &tests,
137+
const tests::Tests::MethodDescription &testMethod,
138+
const std::optional<LineInfo::PredicateInfo> &predicateInfo,
139+
const std::string &testedMethod,
140+
bool onlyForOneEntity,
141+
bool isWrapped);
132142
};
133143
}
134144

‎server/src/utils/KleeUtils.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -81,12 +81,16 @@ namespace KleeUtils {
8181

8282
std::string entryPointFunction(const tests::Tests &tests,
8383
const std::string &methodName,
84-
bool needToMangle) {
84+
bool needToMangle,
85+
bool isWrapped) {
8586
std::string methodNewName = getRenamedOperator(methodName);
87+
if (isWrapped) {
88+
methodNewName += PrinterUtils::WRAPPED_SUFFIX;
89+
}
8690
std::string mangledPath = Paths::mangle(tests.relativeFileDir / tests.sourceFileNameNoExt);
8791
mangledPath = StringUtils::stringFormat("klee_entry__%s_%s", mangledPath, methodNewName);
8892
if (needToMangle && Paths::isCXXFile(tests.sourceFilePath)) {
89-
mangledPath = "_Z" + std::to_string(mangledPath.size()) + mangledPath + "iPPcS0_";
93+
mangledPath = PrinterUtils::MANGLED_PREFIX + std::to_string(mangledPath.size()) + mangledPath + PrinterUtils::MANGLED_SUFFIX;
9094
}
9195
return mangledPath;
9296
}

‎server/src/utils/KleeUtils.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,9 @@ namespace KleeUtils {
1515
std::string getRenamedOperator(std::string_view methodName);
1616

1717
std::string entryPointFunction(const tests::Tests &tests,
18-
const std::string &methodName,
19-
bool needToMangle = false);
18+
const std::string &methodName,
19+
bool needToMangle = false,
20+
bool isWrapped = false);
2021

2122
std::string postSymbolicVariable(const std::string &variableName);
2223

0 commit comments

Comments
 (0)