Skip to content

Commit 0688da8

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

File tree

16 files changed

+807
-27
lines changed

16 files changed

+807
-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
@@ -512,6 +512,7 @@ void KTestObjectParser::parseKTest(const MethodKtests &batch,
512512
auto it = tests.methods.find<std::string, tests::Tests::MethodDescriptionToStringEqual>(
513513
testMethod.methodName);
514514
LOG_S(DEBUG) << "Parse klee for method: " << testMethod.methodName;
515+
sourceFilePath = tests.sourceFilePath;
515516
parseTestCases(testCases, filterByLineFlag, it.value(), methodNameToReturnTypeMap, lineInfo);
516517
}
517518
}
@@ -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: 47 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,44 @@ 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) + PrinterUtils::WRAPPED_SUFFIX;
40+
strDeclareVar("int", KleeUtils::RESULT_VARIABLE_NAME, stringFunctionCall(entryPoint,
41+
{PrinterUtils::UTBOT_ARGC, PrinterUtils::UTBOT_ARGV, PrinterUtils::UTBOT_ENVP}));
42+
strFunctionCall(PrinterUtils::POSIX_CHECK_STDIN_READ, {});
43+
strReturn(KleeUtils::RESULT_VARIABLE_NAME);
44+
closeBrackets(1);
45+
ss << NL;
46+
}
47+
48+
void KleePrinter::writeTestedFunction(const Tests &tests,
49+
const tests::Tests::MethodDescription &testMethod,
50+
const std::optional<LineInfo::PredicateInfo> &predicateInfo,
51+
const std::string &testedMethod,
52+
bool onlyForOneEntity,
53+
bool isWrapped) {
54+
writeStubsForFunctionParams(typesHandler, testMethod, true);
55+
declTestEntryPoint(tests, testMethod, isWrapped);
56+
genGlobalParamsDeclarations(testMethod);
57+
genParamsDeclarations(testMethod);
58+
genPostGlobalSymbolicVariables(testMethod);
59+
genPostParamsSymbolicVariables(testMethod);
60+
if (types::TypesHandler::skipTypeInReturn(testMethod.returnType)) {
61+
genVoidFunctionAssumes(testMethod, predicateInfo, testedMethod, onlyForOneEntity);
62+
} else {
63+
genNonVoidFunctionAssumes(testMethod, predicateInfo, testedMethod,
64+
onlyForOneEntity);
65+
}
66+
genGlobalsKleeAssumes(testMethod);
67+
genPostParamsKleeAssumes(testMethod);
68+
strReturn("0");
69+
closeBrackets(1);
70+
ss << NL;
71+
}
72+
3573
fs::path KleePrinter::writeTmpKleeFile(
3674
const Tests &tests,
3775
const std::string &buildDir,
@@ -92,22 +130,12 @@ fs::path KleePrinter::writeTmpKleeFile(
92130
continue;
93131
}
94132
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);
133+
if (srcLanguage == utbot::Language::C) {
134+
writeTestedFunction(tests, testMethod, predicateInfo, testedMethod, onlyForOneEntity, true);
135+
writePosixWrapper(tests, testMethod);
103136
} else {
104-
genNonVoidFunctionAssumes(testMethod, predicateInfo, testedMethod,
105-
onlyForOneEntity);
137+
writeTestedFunction(tests, testMethod, predicateInfo, testedMethod, onlyForOneEntity, false);
106138
}
107-
genGlobalsKleeAssumes(testMethod);
108-
genPostParamsKleeAssumes(testMethod);
109-
strReturn("0");
110-
closeBrackets(1);
111139
} catch (const UnImplementedException &e) {
112140
std::string message =
113141
"Could not generate klee code for method \'" + methodName + "\', skipping it. ";
@@ -121,11 +149,13 @@ fs::path KleePrinter::writeTmpKleeFile(
121149
}
122150

123151
void KleePrinter::declTestEntryPoint(const Tests &tests,
124-
const Tests::MethodDescription &testMethod) {
125-
std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name);
152+
const Tests::MethodDescription &testMethod,
153+
bool isWrapped) {
154+
std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name, false, isWrapped);
126155
auto argvType = types::Type::createSimpleTypeFromName("char", 2);
127156
// 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();
157+
strFunctionDecl("int", entryPoint, {types::Type::intType(), argvType, argvType},
158+
{PrinterUtils::UTBOT_ARGC, PrinterUtils::UTBOT_ARGV, PrinterUtils::UTBOT_ENVP}, "") << LB();
129159
}
130160

131161
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/printers/Printer.cpp‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -672,4 +672,9 @@ namespace printer {
672672
void Printer::writeCopyrightHeader() {
673673
ss << Copyright::GENERATED_C_CPP_FILE_HEADER << NL;
674674
}
675+
676+
std::string Printer::stringFunctionCall(const std::string &functionName,
677+
const std::vector<std::string> &args) {
678+
return functionName + "(" + StringUtils::joinWith(args, ", ") + ")";
679+
}
675680
}

‎server/src/printers/Printer.h‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,9 @@ namespace printer {
104104
SRef end = SCNL,
105105
VSRef modifiers = {});
106106

107+
std::string stringFunctionCall(const std::string &functionName,
108+
const std::vector<std::string> &args);
109+
107110
Stream strFunctionCall(std::string_view functionName,
108111
const std::vector<std::string> &args,
109112
const std::string &end = SCNL,

0 commit comments

Comments
 (0)