Skip to content

Conversation

@S1eGa
Copy link
Collaborator

@S1eGa S1eGa commented Jan 22, 2024

PR providing support for generating error report in SARIF format.

Adds support for reporting errors in SARIF format:

  • Introduces CodeEvent as a base unit for storing information about event in code.
  • CodeEvents are managed with EventRecorder, capable of serializing recorded trace.
  • termianateStateOnProgramError receives an ErrorEvent object contatining all required informration about error.

Enhances gepExprBases:

  • Bases for addresses stored for constant expressions
  • Precalculates bases for llvm::ConstantExpr (i.e. for getElementPtr in arguments of instructions)

Removes checks on baseInBounds during memory operations.

Adds hacks for managing objects with neighboring addresses (in some cases gepExprBases could fail for that case).

Fixes ODR violation with llvm::APFloat::RoundingMode.

@S1eGa S1eGa force-pushed the report-sarif branch 3 times, most recently from a9b5efc to 1d6067b Compare January 24, 2024 17:28
@codecov-commenter
Copy link

codecov-commenter commented Jan 25, 2024

Codecov Report

Merging #167 (c481629) into main (c7dd2ee) will increase coverage by 0.28%.
Report is 1 commits behind head on main.
The diff coverage is 89.92%.

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

Additional details and impacted files
@@            Coverage Diff             @@
##             main     #167      +/-   ##
==========================================
+ Coverage   69.42%   69.71%   +0.28%     
==========================================
  Files         210      216       +6     
  Lines       30083    30393     +310     
  Branches     6668     6716      +48     
==========================================
+ Hits        20886    21187     +301     
+ Misses       6692     6689       -3     
- Partials     2505     2517      +12     
Files Coverage Δ
include/klee/ADT/ImmutableList.h 91.83% <100.00%> (+0.53%) ⬆️
include/klee/Core/Interpreter.h 100.00% <ø> (ø)
include/klee/Module/KModule.h 71.42% <ø> (+4.76%) ⬆️
include/klee/Module/SarifReport.h 89.28% <100.00%> (+1.05%) ⬆️
lib/Core/CodeEvent.h 100.00% <100.00%> (ø)
lib/Core/CodeLocation.cpp 100.00% <100.00%> (ø)
lib/Core/EventRecorder.h 100.00% <100.00%> (ø)
lib/Core/ExecutionState.cpp 71.63% <100.00%> (ø)
lib/Core/Executor.h 74.07% <ø> (ø)
lib/Core/ExecutorUtil.cpp 70.89% <100.00%> (+0.64%) ⬆️
... and 23 more

... and 1 file with indirect coverage changes

@S1eGa S1eGa force-pushed the report-sarif branch 5 times, most recently from a45b568 to 6fa80e7 Compare January 26, 2024 21:39
@S1eGa S1eGa force-pushed the report-sarif branch 7 times, most recently from 7155494 to c3ac2ff Compare February 12, 2024 16:54
@S1eGa S1eGa requested a review from misonijnik February 14, 2024 19:52
@S1eGa S1eGa marked this pull request as ready for review February 14, 2024 19:52
@@ -0,0 +1,34 @@
#ifndef KLEE_RETURN_EVENT_H
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It might be ok to have declarations of all kinds of events in one header.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll better separate them in different files. With grow number of events single header will be less readable (e.g. Passes.h). I suggest an alternative: use a directory for headers, each consisting of a single class.

@@ -0,0 +1,76 @@
#ifndef KLEE_CODE_LOCATION_H
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We must have a copyright and license block in the head part of all files to match the KLEE project style.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add *- C++ -*- for .cpp related headers, please.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

KLEE -> KLEEF

debugLogBuffer(debugBufferString) {
debugLogBuffer(debugBufferString), sarifReport({}) {

// FIXME: put configuration in different place.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

?

baseInBounds =
AndExpr::create(baseInBounds, mo->getBoundsCheckPointer(base, size));
}
// if (base != address || size != bytes) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Clean dead code.

// RUN: %clang -emit-llvm -g -c %s -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee -write-sarifs --use-sym-size-alloc --use-sym-size-li --skip-not-symbolic-objects --posix-runtime --libc=uclibc -cex-cache-validity-cores --output-dir=%t.klee-out %t.bc > %t.log
// RUN: python3 %S/../../checker.py %t.klee-out/report.sarif %S/pattern.sarif
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add checker.py as a command in lit.cfg

@S1eGa S1eGa force-pushed the report-sarif branch 2 times, most recently from fda377e to dd98605 Compare February 22, 2024 11:12

config.substitutions.append(
('%checker', f"python3 {os.path.join(os.path.dirname(__file__), 'checker.py')}".strip())
) No newline at end of file
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add a new line.

@@ -0,0 +1,76 @@
#ifndef KLEE_CODE_LOCATION_H
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add *- C++ -*- for .cpp related headers, please.

@@ -0,0 +1,76 @@
#ifndef KLEE_CODE_LOCATION_H
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

KLEE -> KLEEF

  * Introduces `CodeEvent` as a base unit for storing information about event in code.
  * `CodeEvent`s are managed with `EventRecorder`, capable of serializing recorded trace.
  * `termianateStateOnProgramError` receives an `ErrorEvent` object contatining all required information about error.
[feat] Enhances `gepExprBases`:
  * Bases for addresses stored for constant expressions.
  * Precalculates bases for `llvm::ConstantExpr` (i.e. for `getElementPtr` in arguments of instructions).
[perf] Removes checks on `baseInBounds` during memory operations.
[fix] Adds hacks for managing objects with neighboring addresses (in some cases `gepExprBases` could assume that the beginning of one object is the end of another).
[fix] Fixes ODR violation with `llvm::APFloat::RoundingMode`.
@misonijnik misonijnik merged commit ebca2f3 into UnitTestBot:main Feb 26, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants