[go: up one dir, main page]
Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Execute unimplemented llvm.* intrinsics likewise external functions #1541

Draft
wants to merge 5 commits into
base: master
Choose a base branch
from
Draft

Execute unimplemented llvm.* intrinsics likewise external functions #1541

wants to merge 5 commits into from

Conversation

operasfantom
Copy link
Contributor
@operasfantom operasfantom commented Jul 6, 2022 •
edited
Loading

Summary:

This PR closes #1528.

Added derived class KIntrinsic which inherits from KCallable. This aims to distinguish that from KFunction and create a simple IR call inside ExternalDispatcherImpl::createDispatcher.

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.

@operasfantom operasfantom marked this pull request as draft July 6, 2022 15:03
@operasfantom
Copy link
Contributor Author

I think I might need a little help with this PR, until then it remains as a draft. The current error I can't deal with is the following:

# command stderr:
/tmp/klee_src/test/Intrinsics/ExternalCallConcrete.ll:28:28: error: CHECK-EXTERNAL-CONCRETE: expected string not found in input
; CHECK-EXTERNAL-CONCRETE: KLEE: done: completed paths = 3
                           ^
<stdin>:8:54: note: scanning from here
KLEE: WARNING ONCE: calling external: llvm.minnum.f32_0(1065353216, 1073741824) at [no debug info]
                                                     ^
<stdin>:15:23: note: possible intended match here
LLVM ERROR: Broken function found, compilation aborted!

Thus, apparently, the external call was executed successfully but then tests were not generated. I couldn't reproduce that LLVM ERROR either on newer or older versions of LLVM in my environment. Does anyone guess what it could be?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Execute unimplemented llvm.* intrinsics likewise external functions
1 participant
@operasfantom