Annotations

[ladisgin]

Summary:

Checklist:

• The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
• The PR is divided into a logical sequence of commits OR a single commit is sufficient.
• There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
• Each commit has a meaningful message documenting what it does.
• All messages added to the codebase, all comments, as well as commit messages are spellchecked.
• The code is commented OR not applicable/necessary.
• The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
• There are test cases for the code you added or modified OR no such test cases are required.

[codecov-commenter]

Codecov Report

Merging #109 (1dabff0) into main (7f6fd2d) will increase coverage by 0.05%.
The diff coverage is 70.17%.

❗ Current head 1dabff0 differs from pull request most recent head e749e81. Consider uploading reports for the commit e749e81 to get more accurate results

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #109      +/-   ##
==========================================
+ Coverage   69.42%   69.47%   +0.05%     
==========================================
  Files         210      213       +3     
  Lines       30083    30860     +777     
  Branches     6668     6827     +159     
==========================================
+ Hits        20884    21439     +555     
- Misses       6693     6852     +159     
- Partials     2506     2569      +63     

Files	Coverage Δ
include/klee/Core/Interpreter.h	100.00% <100.00%> (ø)
include/klee/Expr/AlphaBuilder.h	100.00% <ø> (ø)
include/klee/Expr/IndependentSet.h	69.76% <ø> (ø)
include/klee/Module/SarifReport.h	88.23% <ø> (ø)
lib/Core/ExecutionState.cpp	71.63% <ø> (ø)
lib/Core/Executor.h	74.07% <ø> (ø)
lib/Core/SpecialFunctionHandler.h	0.00% <ø> (ø)
lib/Expr/AlphaBuilder.cpp	95.08% <100.00%> (+0.85%)	⬆️
lib/Expr/ExprUtil.cpp	91.83% <100.00%> (+0.43%)	⬆️
lib/Expr/SourceBuilder.cpp	76.19% <100.00%> (+3.46%)	⬆️
... and 14 more

... and 2 files with indirect coverage changes

[ladisgin]

https://github.com/program-analysis-team/cooddy/blob/master/config/.annotations.json

#!/bin/python3

import sys
import json

def getNames(name: str) :
    name = name.replace(" ", "")
    openBracketIndex = name.find("(")
    closeBracketIndex = name.find(")")
    if openBracketIndex == -1 or openBracketIndex + 1 == closeBracketIndex :
        return name, name
    else:
        funcName = name[:openBracketIndex]
        mangledName = name[openBracketIndex + 1:closeBracketIndex]
        return funcName, mangledName


def transform(coody_json):
    utbot_json = {}
    for coody_name, annotation in coody_json.items():
        funcName, mangledName = getNames(coody_name)
        utbot_json[mangledName] = {"name": funcName, "annotation": annotation, "properties": []}
    return utbot_json


fi = open(sys.argv[1], "r")
j = json.load(fi)
res = transform(j)
# print(res)

fo = open("klee_annotation.json", "w")
json.dump(res, fo, indent=True)

[ladisgin]

TODO Add implementation for AllocSource

[Columpio]

In my opinion, the following steps should be made before merging it to main:

• Remove Add mocks #80 as this PR incorporates its features but also advances further
• (Obviously) rebase on main
• Remove duplicated mocking functionality, i.e., unify functionality given by flags MockExternalCalls, MockAllExternals, MockLinkedExternals, MockUnlinkedStrategy
• Add our own annotations file (probably, based on Cooddy one) and enable it by default
• Remove flags absorbed by annotations, like NullOnZeroMalloc

[ladisgin]

• mock-linked-externals renamed to mock-modeled-functions
• mock-all-externals ~= mock-policy=all
• mock-external-calls move to mock-policy=failed
• mock-strategy now have two value naive and deterministic used only with mock-policy=all
• mock-mutable-globals move to Mock category

NullOnZeroMalloc argument from original KLEE it'll be better save compatibility
Add configs/annotations.json, but don't add it by default, because this test has a complex replay that only works with llvm.