Add support symbolic input/output for C

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

@@ -0,0 +1,186 @@
+#include <stdio.h>
+#include "input_output.h"
+
+int simple_getc() {
+    unsigned char a = getc(stdin);
+    if (a == '0') {
+        return 0;
+    } else if (a == '1') {
+        return 1;
+    } else if (a == '2') {
+        return 2;
+    } else if (a == '3') {
+        return 3;
+    } else if (a == '4') {
+        return 4;
+    } else if (a == '5') {
+        return 5;
+    } else if (a == '6') {
+        return 6;
+    } else if (a == '7') {
+        return 7;
+    } else if (a == '8') {
+        return 8;
+    } else if (a == '9') {
+        return 9;
+    }
+    return -1;
+}
+
+int simple_fgetc(int x) {
+    if (x >= 0 && x <= 9) {
+        unsigned char a = fgetc(stdin);
+        if (a >= 'a' && a <= 'z') {
+            return 1;
+        } else {
+            return 2;
+        }
+    } else {
+        unsigned char a = fgetc(stdin);
+        unsigned char b = fgetc(stdin);
+        if (a >= 'a' && a <= 'z') {
+            if (b >= '0' && b <= '9') {
+                return 3;
+            } else {
+                return 4;
+            }
+        } else {
+            return 5;
+        }
+    }
+}
+
+int simple_fread() {
+    int arrA[4];
+    int arrB[4];
+    fread(arrA, sizeof(int), 4, stdin);
+    fread(arrB, sizeof(int), 4, stdin);
+
+    int sumA = 0, sumB = 0;
+    for (int i = 0; i < 4; i++) {
+        sumA += arrA[i];
+        sumB += arrB[i];
+    }
+    if (sumA == sumB) {
+        return 0;
+    } else if (sumA > sumB) {
+        return 1;
+    } else {
+        return -1;
+    }
+}
+
+int simple_fgets() {
+    char a[8];
+    fgets(a, 6, stdin);
+    if (a[0] == 'u' && a[1] == 't' && a[2] == 'b' && a[3] == 'o' && a[4] == 't') {
+        return 1;
+    }
+    return 0;
+}
+
+int simple_getchar() {
+    unsigned char a = getchar();
+    unsigned char b = getchar();
+
+    if (a + b < 0) {
+        return -1;
+    }
+
+    if (a + b < 100) {
+        return 0;
+    } else if (a + b < 200) {
+        return 1;
+    } else {
+        return 2;
+    }
+}
+
+int simple_gets() {
+    char a[8];
+    gets(a);
+    if (a[0] == 'u' && a[1] == 't' && a[2] == 'b' && a[3] == 'o' && a[4] == 't') {
+        return 1;
+    }
+    return 0;
+}
+
+char simple_putc(int x, int y) {
+    if (x + y > 0) {
+        putc('1', stdout);
+        return '1';
+    } else if (x + y < 0) {
+        putc('2', stdout);
+        return '2';
+    } else {
+        putc('0', stdout);
+        return '0';
+    }
+}
+
+char simple_fputc(int x, int y) {
+    if (x < y) {
+        fputc('<', stdout);
+        return '<';
+    } else if (x > y) {
+        fputc('>', stdout);
+        return '>';
+    } else {
+        fputc('=', stdout);
+        return '=';
+    }
+}
+
+char simple_fwrite(int x) {
+    if (x > 0) {
+        char a[] = "Positive";
+        fwrite(a, sizeof(char), 8, stdout);
+        return 'P';
+    } else if (x < 0) {
+        char a[] = "Negative";
+        fwrite(a, sizeof(char), 8, stdout);
+        return 'N';
+    } else {
+        char a[] = "Zero";
+        fwrite(a, sizeof(char), 4, stdout);
+        return 'Z';
+    }
+}
+
+char simple_fputs(char c) {
+    if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u') {
+        char a[] = "Vowel";
+        fputs("Vowel", stdout);
+        return 'V';
+    } else {
+        char a[] = "Consonant";
+        fputs("Consonant", stdout);
+        return 'C';
+    }
+}
+
+char simple_putchar(int x, int y) {
+    if (3 * x > 2 * y) {
+        putchar('>');
+        return '>';
+    } else if (3 * x < 2 * y) {
+        putchar('<');
+        return '<';
+    } else {
+        putchar('=');
+        return '=';
+    }
+}
+
+char simple_puts(char c) {
+    if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u') {
+        char a[] = "Vowel";
+        puts(a);
+        return 'V';
+    } else {
+        char a[] = "Consonant";
+        puts(a);
+        return 'C';
+    }
+}
+

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

@@ -0,0 +1,29 @@
+#ifndef INPUT_OUTPUT_H
+#define INPUT_OUTPUT_H
+
+int simple_getc();
+
+int simple_fgetc(int x);
+
+int simple_fread();
+
+int simple_fgets();
+
+int simple_getchar();
+
+int simple_gets();
+
+char simple_putc(int x, int y);
+
+char simple_fputc(int x, int y);
+
+char simple_fwrite(int x);
+
+char simple_fputs(char c);
+
+char simple_putchar(int x, int y);
+
+char simple_puts(char c);
+
+#endif
+

server/src/KleeRunner.cpp

@@ -198,6 +198,7 @@ void KleeRunner::processBatchWithoutInteractive(MethodKtests &ktestChunk,
     std::vector<std::string> argvData = { "klee",
                                           entryPointFlag,
                                           "--libc=klee",
+                                          "--utbot",
                                           "--posix-runtime",
                                           "--fp-runtime",
                                           "--only-output-states-covering-new",
@@ -268,6 +269,7 @@ void KleeRunner::processBatchWithInteractive(const std::vector<tests::TestMethod
     std::vector<std::string> argvData = { "klee",
                                           entryPointFlag,
                                           "--libc=klee",
+                                          "--utbot",
                                           "--posix-runtime",
                                           "--fp-runtime",
                                           "--only-output-states-covering-new",

server/src/Tests.cpp

@@ -508,6 +508,7 @@ void KTestObjectParser::parseKTest(const MethodKtests &batch,
                                    bool filterByLineFlag,
                                    std::shared_ptr<LineInfo> lineInfo) {
     LOG_SCOPE_FUNCTION(DEBUG);
+    sourceFilePath = tests.sourceFilePath;
     for (auto &[testMethod, testCases] : batch) {
         auto it = tests.methods.find<std::string, tests::Tests::MethodDescriptionToStringEqual>(
             testMethod.methodName);
@@ -852,9 +853,9 @@ KTestObjectParser::parseTestCaseParams(const UTBotKTest &ktest,
         processGlobalParamPostValue(testCaseDescription, globalParam, rawKleeParams);
     }
 
-    //We should turn off symbolic stdin, because it doesn't work correct with interactive mode
-    //TODO: rewrite symbolic stdin, so that it can work with interactive mode
-    //processSymbolicStdin(testCaseDescription, rawKleeParams);
+    if (Paths::getSourceLanguage(sourceFilePath) == utbot::Language::C) {
+        processSymbolicStdin(testCaseDescription, rawKleeParams);
+    }
 
     processStubParamValue(testCaseDescription, methodNameToReturnTypeMap, rawKleeParams);
     if (!types::TypesHandler::skipTypeInReturn(methodDescription.returnType)) {

server/src/Tests.h

@@ -569,6 +569,8 @@ namespace tests {
                         bool filterByLineFlag,
                         std::shared_ptr<LineInfo> lineInfo);
     private:
+        fs::path sourceFilePath;
+
         types::TypesHandler &typesHandler;
 
         struct RawKleeParam {

server/src/printers/KleePrinter.cpp

@@ -32,6 +32,45 @@ printer::KleePrinter::KleePrinter(const types::TypesHandler *typesHandler,
     : Printer(srcLanguage), typesHandler(typesHandler), buildDatabase(std::move(buildDatabase)) {
 }
 
+void KleePrinter::writePosixWrapper(const Tests &tests,
+                                    const tests::Tests::MethodDescription &testMethod) {
+    declTestEntryPoint(tests, testMethod, false);
+    strFunctionCall(PrinterUtils::POSIX_INIT, {"&" + PrinterUtils::UTBOT_ARGC, "&" + PrinterUtils::UTBOT_ARGV});
+    std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name, false, true);
+    strDeclareVar("int", KleeUtils::RESULT_VARIABLE_NAME, constrFunctionCall(entryPoint,
+                        {PrinterUtils::UTBOT_ARGC, PrinterUtils::UTBOT_ARGV, PrinterUtils::UTBOT_ENVP},
+                        "", std::nullopt, false));
+    strFunctionCall(PrinterUtils::POSIX_CHECK_STDIN_READ, {});
+    strReturn(KleeUtils::RESULT_VARIABLE_NAME);
+    closeBrackets(1);
+    ss << NL;
+}
+
+void KleePrinter::writeTestedFunction(const Tests &tests,
+                                      const tests::Tests::MethodDescription &testMethod,
+                                      const std::optional<LineInfo::PredicateInfo> &predicateInfo,
+                                      const std::string &testedMethod,
+                                      bool onlyForOneEntity,
+                                      bool isWrapped) {
+    writeStubsForFunctionParams(typesHandler, testMethod, true);
+    declTestEntryPoint(tests, testMethod, isWrapped);
+    genGlobalParamsDeclarations(testMethod);
+    genParamsDeclarations(testMethod);
+    genPostGlobalSymbolicVariables(testMethod);
+    genPostParamsSymbolicVariables(testMethod);
+    if (types::TypesHandler::skipTypeInReturn(testMethod.returnType)) {
+        genVoidFunctionAssumes(testMethod, predicateInfo, testedMethod, onlyForOneEntity);
+    } else {
+        genNonVoidFunctionAssumes(testMethod, predicateInfo, testedMethod,
+                                  onlyForOneEntity);
+    }
+    genGlobalsKleeAssumes(testMethod);
+    genPostParamsKleeAssumes(testMethod);
+    strReturn("0");
+    closeBrackets(1);
+    ss << NL;
+}
+
 fs::path KleePrinter::writeTmpKleeFile(
     const Tests &tests,
     const std::string &buildDir,
@@ -92,22 +131,12 @@ fs::path KleePrinter::writeTmpKleeFile(
             continue;
         }
         try {
-            writeStubsForFunctionParams(typesHandler, testMethod, true);
-            declTestEntryPoint(tests, testMethod);
-            genGlobalParamsDeclarations(testMethod);
-            genParamsDeclarations(testMethod);
-            genPostGlobalSymbolicVariables(testMethod);
-            genPostParamsSymbolicVariables(testMethod);
-            if (types::TypesHandler::skipTypeInReturn(testMethod.returnType)) {
-                genVoidFunctionAssumes(testMethod, predicateInfo, testedMethod, onlyForOneEntity);
+            if (srcLanguage == utbot::Language::C) {
+                writeTestedFunction(tests, testMethod, predicateInfo, testedMethod, onlyForOneEntity, true);
+                writePosixWrapper(tests, testMethod);
             } else {
-                genNonVoidFunctionAssumes(testMethod, predicateInfo, testedMethod,
-                                          onlyForOneEntity);
+                writeTestedFunction(tests, testMethod, predicateInfo, testedMethod, onlyForOneEntity, false);
             }
-            genGlobalsKleeAssumes(testMethod);
-            genPostParamsKleeAssumes(testMethod);
-            strReturn("0");
-            closeBrackets(1);
         } catch (const UnImplementedException &e) {
             std::string message =
                 "Could not generate klee code for method \'" + methodName + "\', skipping it. ";
@@ -121,11 +150,13 @@ fs::path KleePrinter::writeTmpKleeFile(
 }
 
 void KleePrinter::declTestEntryPoint(const Tests &tests,
-                                     const Tests::MethodDescription &testMethod) {
-    std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name);
+                                     const Tests::MethodDescription &testMethod,
+                                     bool isWrapped) {
+    std::string entryPoint = KleeUtils::entryPointFunction(tests, testMethod.name, false, isWrapped);
     auto argvType = types::Type::createSimpleTypeFromName("char", 2);
     // if change args in next line also change cpp mangledPath in kleeUtils.cpp
-    strFunctionDecl("int", entryPoint, {types::Type::intType(), argvType, argvType}, {"utbot_argc", "utbot_argv", "utbot_envp"}, "") << LB();
+    strFunctionDecl("int", entryPoint, {types::Type::intType(), argvType, argvType},
+                    {PrinterUtils::UTBOT_ARGC, PrinterUtils::UTBOT_ARGV, PrinterUtils::UTBOT_ENVP}, "") << LB();
 }
 
 Tests::MethodParam KleePrinter::getKleeMethodParam(tests::Tests::MethodParam const &param) {

server/src/printers/KleePrinter.h

@@ -55,7 +55,7 @@ namespace printer {
             types::Type curType;
         };
 
-        void declTestEntryPoint(const Tests &tests, const Tests::MethodDescription &testMethod);
+        void declTestEntryPoint(const Tests &tests, const Tests::MethodDescription &testMethod, bool isWrapped);
 
         void genGlobalParamsDeclarations(const Tests::MethodDescription &testMethod);
 
@@ -129,6 +129,16 @@ namespace printer {
         void genPostSymbolicVariable(const Tests::MethodDescription &testMethod, const Tests::MethodParam &param);
 
         void genPostAssumes(const Tests::MethodParam &param, bool visitGlobal = false);
+
+        void writePosixWrapper(const Tests &tests,
+                               const tests::Tests::MethodDescription &testMethod);
+
+        void writeTestedFunction(const Tests &tests,
+                                 const tests::Tests::MethodDescription &testMethod,
+                                 const std::optional<LineInfo::PredicateInfo> &predicateInfo,
+                                 const std::string &testedMethod,
+                                 bool onlyForOneEntity,
+                                 bool isWrapped);
     };
 }
 

server/src/utils/KleeUtils.cpp

@@ -81,12 +81,16 @@ namespace KleeUtils {
 
     std::string entryPointFunction(const tests::Tests &tests,
                                    const std::string &methodName,
-                                   bool needToMangle) {
+                                   bool needToMangle,
+                                   bool isWrapped) {
         std::string methodNewName = getRenamedOperator(methodName);
+        if (isWrapped) {
+            methodNewName += PrinterUtils::WRAPPED_SUFFIX;
+        }
         std::string mangledPath = Paths::mangle(tests.relativeFileDir / tests.sourceFileNameNoExt);
         mangledPath = StringUtils::stringFormat("klee_entry__%s_%s", mangledPath, methodNewName);
         if (needToMangle && Paths::isCXXFile(tests.sourceFilePath)) {
-            mangledPath = "_Z" + std::to_string(mangledPath.size()) + mangledPath + "iPPcS0_";
+            mangledPath = PrinterUtils::MANGLED_PREFIX + std::to_string(mangledPath.size()) + mangledPath + PrinterUtils::MANGLED_SUFFIX;
         }
         return mangledPath;
     }