The whole inlining logic

src/backend/generate_executable.py

@@ -2,7 +2,7 @@
 from pycparser.c_ast import FuncDef, Decl, FuncCall, ID, Compound, TypeDecl, IdentifierType, FuncDecl, ParamList, Return, Constant, Assignment, ExprList, BinaryOp, NamedInitializer, InitList, Struct, ArrayDecl, Cast, Typename
 import os
 
-pycparser_utils_path = '/home/c/Desktop/research/lf/code/pycparser/utils/fake_libc_include'
+pycparser_utils_path = '/home/abdalla/gamtime-project/pycparser/utils/fake_libc_include'
 
 class ExecutableTransformer(object):
     """ 

src/smt_solver/to_klee_format.py

@@ -4,7 +4,7 @@
 from pycparser.c_ast import FuncDef, Decl, FuncCall, ID, Compound, TypeDecl, IdentifierType, FuncDecl, ParamList, Return, Constant, ArrayDecl
 
 headers = ["#include </snap/klee/9/usr/local/include/klee/klee.h>", "#include <stdbool.h>"]
-pycparser_utils_path="/home/c/Desktop/research/lf/code/pycparser/utils/fake_libc_include"
+pycparser_utils_path="/home/abdalla/gamtime-project/pycparser/utils/fake_libc_include"
 
 class KleeTransformer(object):
     def __init__(self, ast, function_name, total_path_labels, total_number_of_labels):

test/tacle_test/programs/ext_func/c_lib_test/c_lib_test.c

@@ -0,0 +1,113 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <math.h>
+
+int ext_func_5(int x) {
+    char buffer[5];
+
+    // Convert integers to strings
+    sprintf(buffer, "%d", x);
+    // Append some digits to the string representation of x
+    strcat(buffer, "123");
+    // Convert back to integer
+    x = strtol(buffer, NULL, 10);
+
+    if (x == 5123) {
+        return 1;
+    } else {
+        return 0;
+    }
+
+
+}
+
+int ext_func_4(char buffer[]) {
+    if (strcmp(buffer, "HA")) {
+        return 1;
+    } else {
+        return 0;
+    }  
+}
+
+int ext_func_3(char buffer[]) {
+    printf(strtol(".-0.......", NULL, 10));
+    int x = strtol(buffer, NULL, 10);
+    if (x == 5) {
+        return 1;
+    } else {
+        return 0;
+    }  
+}
+
+int ext_func_2(int x) {
+    // int result = pow(base, exp);
+    // int result = base*exp; 
+    // if x >= 0 returnx else return -x
+    if (abs(x) == 4) {
+        return 0;
+    } else {
+        return 1;
+    }   
+}
+
+int ext_func_1(int base, int exp) {
+    int result = pow(base, exp);
+    // int result = base*exp;
+
+    if (result == 4) {
+        return 0;
+    } else {
+        return 1;
+    }   
+}
+
+int main() {
+
+// ext_func_1
+//   int base;
+//   klee_make_symbolic(&base, sizeof(base), "base");
+//   int exp;
+//   klee_make_symbolic(&exp, sizeof(exp), "exp");
+//   return ext_func_1(base, exp);
+
+// ext_func_2
+    // int x;
+    // klee_make_symbolic(&x, sizeof(x), "x");
+    // return ext_func_2(x);
+
+// ext_func_3
+  char buffer[10];
+  klee_make_symbolic(&buffer, sizeof(buffer), "buffer");
+  return ext_func_3(buffer);
+
+// ext_func_4
+//   char buffer[10];
+//   klee_make_symbolic(&buffer, sizeof(buffer), "buffer");
+//   return ext_func_4(buffer);
+
+// ext_func_5
+    // int x;
+    // klee_make_symbolic(&x, sizeof(x), "x");
+    // return ext_func_5(x);
+}
+
+
+
+
+
+
+
+// clang -emit-llvm -c -g ext_func.c -o ext_func.bc
+// clang -emit-llvm -c -g ext_func.c -I/../../../../klee-uclibc/include -o ext_func.bc
+// clang -emit-llvm -c -g ext_func.c -I/../../../../klee-uclibc/include -o ext_func.bc
+// klee --libc=uclibc --posix-runtime ext_func.bc
+// klee ext_func.bc
+// klee.ktest-tool klee-last/test000001.ktest 
+
+// clang -S -emit-llvm ext_func.c -o ext_func.ll
+// opt -dot-cfg -disable-output --enable-newgvn=0 ext_func.ll
+
+//solve path explosion                                                          
+//klee --libc=uclibc --posix-runtime --max-depth=5 ext_func.bc
+//klee --libc=uclibc --posix-runtime --max-depth=10 --use-merge --search=bfs ext_func.bc

test/tacle_test/programs/ext_func/ext_lib_test/ext_func.c

@@ -0,0 +1,54 @@
+#include "helper.h"
+#include </snap/klee/9/usr/local/include/klee/klee.h>
+
+int ext_func(int x){
+    if (abs(x) == 4) {
+        return 0;
+    } else {
+        return 1;
+    }
+}
+
+int main() {
+
+// ext_func_1
+    // int x;
+    // klee_make_symbolic(&x, sizeof(x), "x");
+    // return ret0(x);
+
+// ext_func_2
+    int x;
+    klee_make_symbolic(&x, sizeof(x), "x");
+    return ext_func(x);
+
+}
+
+
+
+
+
+
+// clang -emit-llvm -c helper.c -o helper.bc
+// clang -emit-llvm -c -g ext_func.c -o ext_func.bc
+// klee ext_func.bc
+// klee -link-llvm-lib=helper.bc ext_func.bc
+// klee.ktest-tool klee-last/test000001.ktest 
+
+// clang -emit-llvm -O0 -c helper.c -o helper.bc
+// clang -emit-llvm -O0 -c ext_func.c -o ext_func.bc
+// llvm-link ext_func.bc helper.bc -o combined.bc
+// opt -always-inline -inline -inline-threshold=10000000 combined.bc -o inlined.bc
+// opt -always-inline -inline -inline-threshold=10000000 combined_mod.bc -o inlined.bc
+// opt -dot-cfg inlined.bc
+// opt -dot-cfg inlined.bc
+// dot -Tpng .main.dot -o cfg_main.png
+
+// llvm-dis combined.bc -o combined.ll
+// llvm-dis inlined.bc -o inlined.ll
+// llvm-as combined.ll -o combined.bc
+// llvm-as combined_mod.ll -o combined_mod.bc
+// alwaysinline
+// clang -O0 combined.ll -o combined.bc
+
+
+

test/tacle_test/programs/ext_func/ext_lib_test/helper.c

@@ -0,0 +1,10 @@
+#include "helper.h"
+#include <stdio.h>
+
+int ret0(int x) {
+    return 0;
+}
+
+int abs(int x) {
+    return x >= 0 ? x : -x;
+}

test/tacle_test/programs/ext_func/ext_lib_test/helper.h

@@ -0,0 +1,10 @@
+#ifndef HELPER_H
+#define HELPER_H
+
+// __attribute__((always_inline));
+
+int ret0(int x);
+
+int abs(int x);
+
+#endif

test/tacle_test/programs/ext_func/ext_lib_test/inline.py

@@ -0,0 +1,95 @@
+import os
+import re
+import subprocess
+import sys
+
+def run_command(command):
+    result = subprocess.run(command, shell=True, capture_output=True, text=True, errors='replace')
+    if result.returncode != 0:
+        print(f"Error running command: {command}")
+        print(result.stdout)
+        print(result.stderr)
+        sys.exit(1)
+    return result.stdout
+
+def compile_to_bitcode(files):
+    bitcode_files = []
+    for file in files:
+        bc_file = file.replace('.c', '.bc')
+        run_command(f"clang -emit-llvm -O0 -c {file} -o {bc_file}")
+        bitcode_files.append(bc_file)
+    return bitcode_files
+
+def link_bitcode(bitcode_files, output_file):
+    run_command(f"llvm-link {' '.join(bitcode_files)} -o {output_file}")
+
+def disassemble_bitcode(input_file, output_file):
+    run_command(f"llvm-dis {input_file} -o {output_file}")
+
+def modify_llvm_ir(input_file, output_file):
+    with open(input_file, 'r') as file:
+        ir_content = file.read()
+
+    # Replace all occurrences of 'noinline' with 'alwaysinline'
+    ir_content = re.sub(r'\bnoinline\b', 'alwaysinline', ir_content)
+
+    # Remove all occurrences of 'optnone'
+    ir_content = re.sub(r'\boptnone \b', '', ir_content)
+
+    # Write the modified content to the output file
+    with open(output_file, 'w') as file:
+        file.write(ir_content)
+
+def assemble_bitcode(input_file, output_file):
+    run_command(f"llvm-as {input_file} -o {output_file}")
+
+def inline_functions(input_file, output_file):
+    run_command(f"opt -always-inline -inline -inline-threshold=10000000 {input_file} -o {output_file}")
+
+def generate_cfg(input_file):
+    run_command(f"opt -dot-cfg {input_file}")
+
+if __name__ == "__main__":
+    if len(sys.argv) < 2:
+        print("Usage: python process_files.py <file1.c> <file2.c> ...")
+        sys.exit(1)
+
+    c_files = sys.argv[1:]
+    combined_bc = "combined.bc"
+    combined_ll = "combined.ll"
+    combined_mod_ll = "combined_mod.ll"
+    combined_mod_bc = "combined_mod.bc"
+    inlined_bc = "inlined.bc"
+
+    # Step 1: Compile all C files to bitcode
+    bitcode_files = compile_to_bitcode(c_files)
+
+    # Step 2: Link all bitcode files into a single combined bitcode file
+    link_bitcode(bitcode_files, combined_bc)
+
+    # Step 3: Disassemble the combined bitcode file to LLVM IR
+    disassemble_bitcode(combined_bc, combined_ll)
+
+    # Step 4: Modify the LLVM IR file
+    modify_llvm_ir(combined_ll, combined_mod_ll)
+
+    # Step 5: Assemble the modified LLVM IR back to bitcode
+    assemble_bitcode(combined_mod_ll, combined_mod_bc)
+
+    # Step 6: Inline the functions in the modified bitcode
+    inline_functions(combined_mod_bc, inlined_bc)
+
+    # Step 7: Generate the CFG for the inlined bitcode
+    generate_cfg(inlined_bc)
+
+    print("Processing complete. Output files:")
+    print(f"  Combined bitcode: {combined_bc}")
+    print(f"  Combined LLVM IR: {combined_ll}")
+    print(f"  Modified LLVM IR: {combined_mod_ll}")
+    print(f"  Modified bitcode: {combined_mod_bc}")
+    print(f"  Inlined bitcode: {inlined_bc}")
+    print("CFG files generated in the current directory.")
+
+
+
+# python3 inline.py ext_func.c helper.c