Skip to content

Commit a9db5f3

Browse files
Saveliy Grigoryevladisgin
Saveliy Grigoryev
authored and
ladisgin
committed
Add functional stubs
1 parent daf5c3c commit a9db5f3

File tree

15 files changed

+261
-30
lines changed

15 files changed

+261
-30
lines changed

‎integration-tests/c-example/lib/linked-list/linked-list.c

+50
Original file line numberDiff line numberDiff line change
@@ -146,4 +146,54 @@ int sort_list(struct Node *head) {
146146
}
147147
}
148148
return 0;
149+
}
150+
151+
int sort_list_with_comparator(struct Node *head, int (*cmp) (int, int)) {
152+
int n = len_bound(head, SIZE);
153+
if (n == SIZE) {
154+
for (int i = 0; i < n - 2; i++) {
155+
struct Node *cop = head;
156+
while (cop->next != NULL) {
157+
if (!cmp(cop->x, cop->next->x)) {
158+
int t = cop->x;
159+
cop->x = cop->next->x;
160+
cop->next->x = t;
161+
}
162+
cop = cop->next;
163+
}
164+
}
165+
int fl = 1;
166+
struct Node *cop = head;
167+
while (cop->next != NULL) {
168+
if (!cmp(cop->x, cop->next->x)) {
169+
fl = -1;
170+
}
171+
cop = cop->next;
172+
}
173+
if (fl == 1) {
174+
return 1;
175+
} else {
176+
return -1;
177+
}
178+
}
179+
return 0;
180+
}
181+
182+
int find_maximum(int x, int y, int (*compare) (int, int)) {
183+
int t = compare(x, y);
184+
if (t) {
185+
return x;
186+
} else {
187+
return y;
188+
}
189+
}
190+
191+
int vowel_consonant(char c, char (*vowel) (char)) {
192+
char s = vowel(c);
193+
if (s == 'a' || s == 'e' || s == 'i' || s == 'o' || s == 'u' || s == 'y') {
194+
return 1;
195+
} else {
196+
return -1;
197+
}
198+
149199
}

‎integration-tests/c-example/lib/linked-list/linked-list.h

+6
Original file line numberDiff line numberDiff line change
@@ -52,4 +52,10 @@ int len_bound(struct Node *head, int bound);
5252

5353
int sort_list(struct Node *head);
5454

55+
int sort_list_with_comparator(struct Node *head, int (*cmp) (int, int));
56+
57+
int find_maximum(int x, int y, int (*compare) (int, int));
58+
59+
int vowel_consonant(char c, char (*vowel) (char));
60+
5561
#endif

‎server/build.sh

100644100755
File mode changed.

‎server/src/Tests.cpp

+21
Original file line numberDiff line numberDiff line change
@@ -633,6 +633,26 @@ void KTestObjectParser::assignTypeUnnamedVar(Tests::MethodTestCase &testCase,
633633
}
634634
}
635635

636+
void KTestObjectParser::assignTypeStubVar(Tests::MethodTestCase &testCase,
637+
const Tests::MethodDescription &methodDescription) {
638+
for (auto const &obj : testCase.objects) {
639+
if (StringUtils::endsWith(obj.name, PrinterUtils::KLEE_SYMBOLIC_SUFFIX)) {
640+
std::string stubFuncName = obj.name.substr(0, obj.name.length() - PrinterUtils::KLEE_SYMBOLIC_SUFFIX.length());
641+
if (!CollectionUtils::contains(methodDescription.functionPointers, stubFuncName)) {
642+
std::string message = "Can't find function pointer with name " + stubFuncName;
643+
LOG_S(ERROR) << message;
644+
continue;
645+
}
646+
types::Type stubType = types::Type::createArray(methodDescription.functionPointers.at(stubFuncName)->returnType);
647+
shared_ptr<AbstractValueView> stubView = testParameterView({obj.name, obj.bytes}, {stubType, obj.name},
648+
PointerUsage::PARAMETER, testCase.fromAddressToName,
649+
testCase.lazyReferences, methodDescription);
650+
testCase.stubParamValues.emplace_back(obj.name, 0, stubView);
651+
testCase.stubParamTypes.emplace_back(stubType, obj.name, std::nullopt);
652+
}
653+
}
654+
}
655+
636656
void KTestObjectParser::parseTestCases(const UTBotKTestList &cases,
637657
bool filterByLineFlag,
638658
Tests::MethodDescription &methodDescription,
@@ -709,6 +729,7 @@ void KTestObjectParser::parseTestCases(const UTBotKTestList &cases,
709729
LOG_S(MAX) << traceStream.str();
710730

711731
assignTypeUnnamedVar(testCase, methodDescription);
732+
assignTypeStubVar(testCase, methodDescription);
712733

713734
methodDescription.testCases.push_back(testCase);
714735
}

‎server/src/Tests.h

+7-1
Original file line numberDiff line numberDiff line change
@@ -335,6 +335,7 @@ namespace tests {
335335
const shared_ptr<AbstractValueView> &view)
336336
: name(std::move(name)), alignment(alignment), view(view) {};
337337
};
338+
338339
struct TestCaseDescription {
339340
string scopeName;
340341

@@ -374,6 +375,8 @@ namespace tests {
374375
vector<TestCaseParamValue> paramValues;
375376
vector<TestCaseParamValue> paramPostValues;
376377
vector<TestCaseParamValue> lazyValues;
378+
vector<TestCaseParamValue> stubParamValues;
379+
vector<MethodParam> stubParamTypes;
377380
shared_ptr<AbstractValueView> returnValueView;
378381

379382
bool isError() const;
@@ -665,7 +668,10 @@ namespace tests {
665668
vector<RawKleeParam> &rawKleeParams);
666669

667670
void assignTypeUnnamedVar(Tests::MethodTestCase &testCase,
668-
const Tests::MethodDescription &methodDescription);
671+
const Tests::MethodDescription &methodDescription);
672+
673+
void assignTypeStubVar(Tests::MethodTestCase &testCase,
674+
const Tests::MethodDescription &methodDescription);
669675

670676
void workWithStructInBFS(std::queue<JsonNumAndType> &order, std::vector<bool> &visited,
671677
const Offset &off, std::vector<UTBotKTestObject> &objects, const types::StructInfo &structInfo);

‎server/src/printers/Printer.cpp

+44-20
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
#include "utils/ArgumentsUtils.h"
1010
#include "utils/Copyright.h"
1111
#include "visitors/VerboseParameterVisitor.h"
12+
#include "printers/KleeConstraintsPrinter.h"
1213

1314
#include "loguru.h"
1415

@@ -385,15 +386,30 @@ namespace printer {
385386
return ss;
386387
}
387388

389+
std::stringstream& Printer::checkOverflowStubArray(const string &cntCall) {
390+
ss << TAB_N() << "if (" << cntCall << " == " <<
391+
types::TypesHandler::getElementsNumberInPointerOneDim(types::PointerUsage::PARAMETER) << ") {" << NL;
392+
tabsDepth++;
393+
ss << TAB_N() << cntCall << "--;" << NL;
394+
ss << RB();
395+
return ss;
396+
}
397+
398+
388399
std::stringstream &Printer::strStubForMethod(const Tests::MethodDescription &method,
389400
const types::TypesHandler &typesHandler,
390401
const string &prefix,
391402
const string &suffix,
392-
bool makeSymbolic,
393403
bool makeStatic) {
394404
auto methodCopy = method;
395-
396405
methodCopy.name = method.name;
406+
407+
string stubSymbolicVarName = getStubSymbolicVarName(method.name);
408+
if (!types::TypesHandler::isVoid(method.returnType)) {
409+
strDeclareArrayVar(types::Type::createArray(method.returnType), stubSymbolicVarName,
410+
types::PointerUsage::PARAMETER);
411+
}
412+
397413
if (!prefix.empty()) {
398414
methodCopy.name = prefix + "_" + methodCopy.name;
399415
}
@@ -411,23 +427,31 @@ namespace printer {
411427
strReturn(returnValue) << RB() << NL;
412428
return ss;
413429
}
414-
if (makeSymbolic) {
415-
string firstTimeCallVar = "firstTimeCall";
416-
string stubSymbolicVarName = getStubSymbolicVarName(method.name);
417-
strDeclareVar("static int", firstTimeCallVar, "1");
418-
ss << TAB_N() << "#ifdef " << PrinterUtils::KLEE_MODE << NL;
419-
tabsDepth++;
420-
ss << TAB_N() << "if (" << firstTimeCallVar << " == 1)" << LB();
421-
strAssignVar(firstTimeCallVar, "0");
422-
strKleeMakeSymbolic(stubSymbolicVarName, !method.returnType.isArray(),
423-
stubSymbolicVarName);
424-
ss << RB();
425-
tabsDepth--;
426-
ss << TAB_N() << "#endif" << NL;
427-
returnValue = stubSymbolicVarName;
428-
} else {
429-
returnValue = typesHandler.getDefaultValueForType(methodCopy.returnType, getLanguage());
430-
}
430+
431+
string firstTimeCallVar = "firstTimeCall";
432+
strDeclareVar("static int", firstTimeCallVar, "1");
433+
const string cntCall = "cntCall";
434+
strDeclareVar("static int", cntCall, "0");
435+
ss << TAB_N() << "#ifdef " << PrinterUtils::KLEE_MODE << NL;
436+
tabsDepth++;
437+
ss << TAB_N() << "if (" << firstTimeCallVar << " == 1)" << LB();
438+
strAssignVar(firstTimeCallVar, "0");
439+
strKleeMakeSymbolic(stubSymbolicVarName, !method.returnType.isArray(),
440+
stubSymbolicVarName);
441+
types::TypeMaps tempMap = {};
442+
auto temp = shared_ptr <types::TypesHandler>(new types::TypesHandler(tempMap, types::TypesHandler::SizeContext()));
443+
printer::KleeConstraintsPrinter preferWriter(temp.get(), srcLanguage);
444+
preferWriter.setTabsDepth(tabsDepth);
445+
preferWriter.genConstraints(
446+
{types::Type::createArray(method.returnType), stubSymbolicVarName, std::nullopt});
447+
ss << preferWriter.ss.str();
448+
ss << RB();
449+
tabsDepth--;
450+
ss << TAB_N() << "#endif" << NL;
451+
452+
checkOverflowStubArray(cntCall);
453+
454+
returnValue = stubSymbolicVarName + "[" + cntCall + "++]";
431455
strReturn(returnValue) << RB() << NL;
432456
return ss;
433457
}
@@ -552,7 +576,7 @@ namespace printer {
552576
strTypedefFunctionPointer(*fInfo, typedefName);
553577
}
554578
strStubForMethod(tests::Tests::MethodDescription::fromFunctionInfo(*fInfo), *typesHandler,
555-
stubName, "stub", false, makeStatic);
579+
stubName, "stub", makeStatic);
556580
}
557581

558582
void Printer::genStubForStructFunctionPointer(const string &structName,

‎server/src/printers/Printer.h

+3-2
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,8 @@ namespace printer {
102102

103103
Stream strAssignVar(std::string_view name, std::string_view value);
104104

105+
std::stringstream& checkOverflowStubArray(const string &cntCall);
106+
105107
Stream strTabIf(bool needTabs);
106108

107109
Stream strFunctionDecl(
@@ -178,7 +180,6 @@ namespace printer {
178180

179181
Stream strReturn(std::string_view value);
180182

181-
182183
Stream strTypedefFunctionPointer(const types::FunctionInfo& method, const string& name);
183184

184185
Stream strDeclareArrayOfFunctionPointerVar(const string&arrayType, const string& arrayName,
@@ -187,7 +188,7 @@ namespace printer {
187188
Stream strStubForMethod(const Tests::MethodDescription& method,
188189
const types::TypesHandler&typesHandler,
189190
const string& prefix,
190-
const string& suffix, bool makeSymbolic = false,
191+
const string& suffix,
191192
bool makeStatic = false);
192193

193194
static string getStubSymbolicVarName(const string& methodName);

‎server/src/printers/StubsPrinter.cpp

+2-6
Original file line numberDiff line numberDiff line change
@@ -55,16 +55,12 @@ Stubs printer::StubsPrinter::genStubFile(const tests::Tests &tests,
5555
param.type = copyParamType;
5656
}
5757
}
58-
if (!typesHandler.omitMakeSymbolic(methodCopy.returnType)) {
59-
string symbolicVarName = Printer::getStubSymbolicVarName(methodCopy.name);
60-
strDeclareVar(methodCopy.returnType.usedType(), symbolicVarName, std::nullopt, std::nullopt,
61-
true, 0);
62-
}
58+
6359
if (methodCopy.sourceBody) {
6460
strFunctionDecl(methodCopy, " ");
6561
ss << methodCopy.sourceBody.value() << NL;
6662
} else {
67-
strStubForMethod(methodCopy, typesHandler, "", "", true);
63+
strStubForMethod(methodCopy, typesHandler, "", "");
6864
};
6965
ss << NL;
7066
}

‎server/src/printers/TestsPrinter.cpp

+13
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,18 @@ void TestsPrinter::printLazyReferences(const Tests::MethodDescription &methodDes
136136
}
137137
}
138138

139+
void TestsPrinter::printStubVariables(const Tests::MethodDescription &methodDescription,
140+
const Tests::MethodTestCase &testCase) {
141+
for (int i = 0; i < testCase.stubParamValues.size(); i++) {
142+
auto stub = testCase.stubParamValues[i];
143+
types::Type stubType = testCase.stubParamTypes[i].type;
144+
std::string bufferSuffix = "_buffer";
145+
std::string buffer = stub.name + bufferSuffix;
146+
strDeclareArrayVar(stubType, buffer, types::PointerUsage::PARAMETER, stub.view->getEntryValue());
147+
strMemcpy(stub.name, buffer, false);
148+
}
149+
}
150+
139151
void TestsPrinter::genParametrizedTestCase(const Tests::MethodDescription &methodDescription,
140152
const Tests::MethodTestCase &testCase,
141153
const std::optional<LineInfo::PredicateInfo>& predicateInfo) {
@@ -145,6 +157,7 @@ void TestsPrinter::genParametrizedTestCase(const Tests::MethodDescription &metho
145157
printClassObject(methodDescription);
146158
printLazyVariables(methodDescription, testCase);
147159
printLazyReferences(methodDescription, testCase);
160+
printStubVariables(methodDescription, testCase);
148161
printFunctionParameters(methodDescription, testCase, true);
149162
parametrizedAsserts(methodDescription, testCase, predicateInfo);
150163
ss << RB() << NL;

‎server/src/printers/TestsPrinter.h

+3
Original file line numberDiff line numberDiff line change
@@ -138,6 +138,9 @@ namespace printer {
138138
void printLazyReferences(const Tests::MethodDescription &methodDescription,
139139
const Tests::MethodTestCase &testCase);
140140

141+
void printStubVariables(const Tests::MethodDescription &methodDescription,
142+
const Tests::MethodTestCase &testCase);
143+
141144
static Tests::MethodParam getValueParam(const Tests::MethodParam &param);
142145
};
143146
}

‎server/src/types/Types.cpp

+15
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,21 @@ types::Type types::Type::createConstTypeFromName(const types::TypeName& type, si
7373
return res;
7474
}
7575

76+
types::Type types::Type::createArray(const types::Type &type) {
77+
Type res;
78+
res.mType = type.typeName() + "*";
79+
res.mUsedType = res.mType;
80+
res.mBaseType = type.baseType();
81+
res.mKinds = type.mKinds;
82+
res.mKinds.insert(res.mKinds.begin(), std::shared_ptr<AbstractType>(new ArrayType(
83+
TypesHandler::getElementsNumberInPointerOneDim(PointerUsage::PARAMETER), false)));
84+
res.dimension = type.dimension + 1;
85+
res.mTypeId = 0;
86+
res.mBaseTypeId = type.mBaseTypeId;
87+
res.maybeArray = true;
88+
return res;
89+
}
90+
7691
types::TypeName types::Type::typeName() const {
7792
return mType;
7893
}

‎server/src/types/Types.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -215,6 +215,8 @@ namespace types {
215215
*/
216216
static Type createConstTypeFromName(const TypeName &type, size_t pointersNum=0);
217217

218+
static Type createArray(const Type &type);
219+
218220
static Type CStringType();
219221

220222
static Type intType();
@@ -241,7 +243,7 @@ namespace types {
241243
static const std::string &getStdinParamName();
242244
private:
243245

244-
explicit Type(const TypeName& type, size_t pointersNum=0);
246+
explicit Type(const TypeName& type, size_t pointersNum=0);
245247

246248
TypeName mType;
247249
TypeName mBaseType;

‎server/test/framework/Syntax_Tests.cpp

+38
Original file line numberDiff line numberDiff line change
@@ -1818,6 +1818,44 @@ namespace {
18181818
);
18191819
}
18201820

1821+
TEST_F(Syntax_Test, sort_list_with_cmp) {
1822+
auto [testGen, status] = createTestForFunction(linked_list_c, 135);
1823+
1824+
ASSERT_TRUE(status.ok()) << status.error_message();
1825+
1826+
checkTestCasePredicates(
1827+
testGen.tests.at(linked_list_c).methods.begin().value().testCases,
1828+
vector<TestCasePredicate>(
1829+
{
1830+
[] (const tests::Tests::MethodTestCase& testCase) {
1831+
return stoi(testCase.returnValueView->getEntryValue()) == -1;
1832+
},
1833+
[] (const tests::Tests::MethodTestCase& testCase) {
1834+
return stoi(testCase.returnValueView->getEntryValue()) == 1;
1835+
},
1836+
[] (const tests::Tests::MethodTestCase& testCase) {
1837+
return stoi(testCase.returnValueView->getEntryValue()) == 0;
1838+
}
1839+
})
1840+
);
1841+
}
1842+
1843+
TEST_F(Syntax_Test, find_maximum) {
1844+
auto [testGen, status] = createTestForFunction(linked_list_c, 166);
1845+
1846+
ASSERT_TRUE(status.ok()) << status.error_message();
1847+
1848+
EXPECT_EQ(2, testUtils::getNumberOfTests(testGen.tests));
1849+
}
1850+
1851+
TEST_F(Syntax_Test, vowel_consonant) {
1852+
auto [testGen, status] = createTestForFunction(linked_list_c, 175);
1853+
1854+
ASSERT_TRUE(status.ok()) << status.error_message();
1855+
1856+
EXPECT_TRUE(testUtils::getNumberOfTests(testGen.tests) >= 2);
1857+
}
1858+
18211859
TEST_F(Syntax_Test, tree_deep) {
18221860
auto [testGen, status] = createTestForFunction(tree_c, 3, 45);
18231861

0 commit comments

Comments
 (0)