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.

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

Implement basic support for vectorized instructions. #657

Merged
merged 2 commits into from Jul 20, 2017

Conversation

@delcypher
Copy link
Contributor

commented May 24, 2017

We use LLVM's Scalarizer pass to remove most vectorized code so that the
Executor only needs to support the InsertElement and ExtractElement
instructions.

This pass was not available in LLVM 3.4 so to support that LLVM version
the pass has been back ported.

There is no support for LLVM 2.9.

There are a few limitations to this implementation.

  • The InsertElement and ExtractElement index cannot be symbolic.
  • Due to the lack of proper floating point support the
    float_vector_constant_llvm*.ll tests currently do not pass.

@delcypher delcypher requested review from ccadar and andreamattavelli May 24, 2017

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 24, 2017

@andreamattavelli @ccadar This is my attempt at upstreaming the vector instruction support I have in my fork of KLEE.

I don't think the current lack of support for a symbolic index for the InsertElement/ExtractElement instructions is a problem. The vectorized code likely comes from LLVM's optimizers where those indices will be concrete. During my testing I never came across symbolic indices.

Hopefully with this we can kill LLVM 2.9.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 24, 2017

@ccadar @andreamattavelli @MartinNowack One thing I wanted your opinion on is type checking the instructions.

If the Scalarizer pass screws up we might end up with vector operands being unexpectedly given to instructions.

So we could add these checks to many instructions in Executor::executeInstruction()

    assert(!(ki->inst->getOperand(0)->getType()->isVectorTy()) &&
           "Invalid operand type");
    assert(!(ki->inst->getOperand(1)->getType()->isVectorTy()) &&
           "Invalid operand type");

or even tighter (e.g. for the Add instruction)

    assert(ki->inst->getOperand(0)->getType()->isIntegerTy() &&
           "Invalid operand type");
    assert(ki->inst->getOperand(1)->getType()->isIntegerTy() &&
           "Invalid operand type");

The problem with this is this will likely decrease the performance of assert builds.

So my current PR doesn't add any of these assertions. However we could add these, if you value correctness over performance.

@delcypher delcypher force-pushed the delcypher:vectorized_instructions branch from 85a6b64 to 7950140 May 24, 2017

@ccadar

This comment has been minimized.

Copy link
Contributor

commented May 24, 2017

Thanks, Dan, that's an important contribution. Regarding your last point: what happens now if the Scalarizer pass misses an instruction? Don't you hit an existing assert?

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 24, 2017

All tests are passing apart from macOS which is flaky. The failure appears unrelated.

@ccadar

This comment has been minimized.

Copy link
Contributor

commented May 24, 2017

The failure seems unrelated to flaky tests.
More importantly, it's not a good idea to disregard test failures -- as we've seen in the past, it's easy to misidentify the root cause.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 24, 2017

@ccadar

Thanks, Dan, that's an important contribution. Regarding your last point: what happens now if the Scalarizer pass misses an instruction? Don't you hit an existing assert?

I don't know about missing an instruction but if I don't run the pass the Executor just carries on executing. Only the shuffle_element.c test fails because it hits the ShuffleVector instruction which is supposed to be removed by the pass.

I don't have tests that apply operators (e.g. Add) to vector data. I should probably add some and see what happens.

@andreamattavelli
Copy link
Contributor

left a comment

@delcypher besides some minor comments, looks very good already.
One major point to address (later) is the support to symbolic in vectorized instructions.

@@ -333,6 +334,7 @@ namespace klee {
const char *Executor::TerminateReasonNames[] = {
[ Abort ] = "abort",
[ Assert ] = "assert",
[ BadVectorAccess] = "bad_vector_access",

This comment has been minimized.

Copy link
@andreamattavelli

andreamattavelli May 24, 2017

Contributor

Wrong formatting.

This comment has been minimized.

Copy link
@delcypher

delcypher May 24, 2017

Author Contributor

What do you want to see instead? badvectoraccess?

This comment has been minimized.

Copy link
@andreamattavelli

andreamattavelli May 24, 2017

Contributor

I was referring to the square braket ]:

[ BadVectorAccess ] = "bad_vector_access",
@@ -0,0 +1,244 @@
; FIXME: Need to upstream floating point support to make this test pass

This comment has been minimized.

Copy link
@andreamattavelli

andreamattavelli May 24, 2017

Contributor

I would remove this test from this PR and add it when floating-point support is upstreamed.

This comment has been minimized.

Copy link
@ccadar

ccadar Jun 29, 2017

Contributor

I agree.

@@ -0,0 +1,244 @@
; FIXME: Need to upstream floating point support to make this test pass

This comment has been minimized.

Copy link
@andreamattavelli

andreamattavelli May 24, 2017

Contributor

I would remove this test from this PR and add it when floating-point support is upstreamed.

This comment has been minimized.

Copy link
@ccadar

ccadar Jun 29, 2017

Contributor

+1

@@ -0,0 +1,244 @@
; FIXME: Need to upstream floating point support to make this test pass

This comment has been minimized.

Copy link
@andreamattavelli

andreamattavelli May 24, 2017

Contributor

I would remove this test from this PR and add it when floating-point support is upstreamed.

This comment has been minimized.

Copy link
@ccadar

ccadar Jun 29, 2017

Contributor

+1

@andreamattavelli

This comment has been minimized.

Copy link
Contributor

commented May 24, 2017

@ccadar

The failure seems unrelated to flaky tests.

It is: I don't understand why but it seems that Travis-CI is affected by some strange network-related issues. Basically, homebrew fails to download the bottled version of LLVM 3.4 from the repository (which is currently my website).

@delcypher

So we could add these checks to many instructions in Executor::executeInstruction()

I am personally in favor of adding more asserts. If we need performance, we compile without assertions (I already do this).

@ccadar @delcypher

what happens now if the Scalarizer pass misses an instruction? Don't you hit an existing assert?

I think that by adding more asserts will likely make KLEE fail if an instruction escapes from the pass. Does it make sense to you?

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 24, 2017

@andreamattavelli

One major point to address (later) is the support to symbolic in vectorized instructions.

As I mentioned I have doubts about this actually happening in practice. More testing will reveal whether this is actually needed.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 24, 2017

@andreamattavelli

I think that by adding more asserts will likely make KLEE fail if an instruction escapes from the pass. Does it make sense to you?

I've added asserts for all the instructions that I think need them. I've also added a few tests to check that scalarization is happening as expected. I also fixed a bug in the order the passes were being run.

@andreamattavelli

This comment has been minimized.

Copy link
Contributor

commented May 25, 2017

@delcypher I'm happy with the current state of this PR. Before approval, I'd like to test it on a few case studies.

@andreamattavelli

This comment has been minimized.

Copy link
Contributor

commented May 25, 2017

@delcypher it does work perfectly on all the case studies where I experienced vectorization-related issues.
I'll wait for @ccadar to comment.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 25, 2017

@ccadar
@delcypher I'm happy with the current state of this PR. Before approval, I'd like to test it on a few case studies.

Thanks. Do you want me to squash the commits into a single commit?

@andreamattavelli

This comment has been minimized.

Copy link
Contributor

commented May 25, 2017

@delcypher

Do you want me to squash the commits into a single commit?

I think it is better to wait for @ccadar's approval, then squash, wait for Travis, and merge.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 25, 2017

@andreamattavelli I've pushed a few additional changes. Could you re-run on your case studies?

I forgot to add asserts to the select instruction. When I added additional tests it turned out those asserts were wrong. We might get operands of vector type to the select instruction's true and false operands..

@andreamattavelli

This comment has been minimized.

Copy link
Contributor

commented May 25, 2017

@delcypher everything works correctly. I guess that I haven't experience such a problem with select. I can try to increase optimization level to see if I can spot it.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 25, 2017

@andreamattavelli

I can try to increase optimization level to see if I can spot it.

-Oall-the-things 🔥

I changed/removed the asserts on the select instruction because they were wrong so I doubt you'll be able to make them fire.

@andreamattavelli

This comment has been minimized.

Copy link
Contributor

commented May 25, 2017

@delcypher

I changed/removed the asserts on the select instruction because they were wrong so I doubt you'll be able to make them fire.

I'm still using the old version. But no, I cannot make the assertion fail even with the maximum level of optimization.

@andreamattavelli

This comment has been minimized.

Copy link
Contributor

commented May 25, 2017

@delcypher @ccadar Going to run this PR through KLEE regression infrastructure just in case.

@ccadar

This comment has been minimized.

Copy link
Contributor

commented May 25, 2017

It would be great to run this through the larger regression infrastructure, making sure you enable optimizations. I'll try to look at the code soon too. And yes, it would be useful to add this as a single commit. Thanks!

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 26, 2017

@ccadar @andreamattavelli I just had a though there is a slight problem with the implementation inlib/Module/KModule.cpp. Currently we run the Scalarizer pass early on (before div/overshift checks because they don't know how to deal with vector instructions).

However if opts.Optimize was true (I think it's false by default right now) then vector instructions might introduced again. We have fine grained control over the optimizations we run so either

  • we need to make sure that the Optimize() function does not introduce vector instructions
    or
  • we can run the Scalarizer pass again after optimization.

Also note that I noticed in the past in my fork of KLEE the Scalarizer pass sometimes left behind unnecessary instructions, those can be cleaned up by adding createDeadCodeEliminationPass() to the passes. We have to be careful here though because this pass might remove code that performs undefined behaviour.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jun 7, 2017

@ccadar @andreamattavelli Can we merge this? PRs are starting to appear (e.g. #669) that are going to conflict with this.

At this point this PR has been reasonably well tested and I think we can attack the problem with --optimize in the future.

@andreamattavelli

This comment has been minimized.

Copy link
Contributor

commented Jun 8, 2017

Can we merge this?

Not so sure. In the previous comment you made some interesting points that still need to be addressed.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jun 14, 2017

@andreamattavelli Sure they need be addressed but we don't need to do this right now

  • --optimize is currently off by default
  • KLEE's optimization is broken in several ways.
    • Given that it is been off by default for so long running this passes will likely lead to problems (e.g. unsupported intrinsics)
    • KLEE's optimization pass pipeline was written a long time ago and is completely out of date with
      what modern Clang does. It likely needs a complete re-write. We should be using LLVM's PassManagerBuilder if we want to construct a standard compiler pass pipeline. If we want to do something different then someone needs to take ownership of KLEE's custom pass pipeline and invest time to figure out what optimizations make sense for symbolic execution.
    • KLEE's optimization also has confusing command line flags (#366)

In summary I don't think we should block this PR due to the broken optimization feature in KLEE.

The assertions I've added will catch violations of the invariant we expect (i.e. arithmetic/comparision instructions don't receive vector operands).

@ccadar

This comment has been minimized.

Copy link
Contributor

commented Jun 14, 2017

Hi @delcypher , I agree and will try to review and merge this in the next couple of weeks (and hopefully sooner). However, with respect to dropping 2.9, (#318), support for optimizations is the main remaining showstopper (after this PR), as 2.9 is the only version I know where one can still run fully optimized code. In any case, I agree treating the deprecation of 2.9 as the next big milestone.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jun 14, 2017

@ccadar With this PR in place I was able to run optimized (optimized externally by Clang, not by KLEE) code without problems on my benchmarks. For LLVM 3.4 at least this PR is probably enough to be able to run optimized code in most cases. As you see above @andreamattavelli didn't run into any problems with this PR enabled and optimizations enabled.

For newer LLVMs there are still problems but those can be addressed later given that we don't officially support them yet.

If there are actually examples for LLVM 3.4 where KLEE runs into unhandled intrinsics we need benchmarks to confirm and fix these.

Given the above (and because technically we don't support LLVM > 3.4 yet) I think we can start to deprecated LLVM 2.9 once this PR is merged.

@delcypher delcypher force-pushed the delcypher:vectorized_instructions branch from 2bc6f3f to 32940f3 Jul 5, 2017

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jul 5, 2017

@ccadar I've squashed the two commits into one.

@MartinNowack
Copy link
Contributor

left a comment

@delcypher Like the addition: A few things should still be fixed. The amount of test cases is fine for me.
@delcypher @ccadar @andreamattavelli
Maybe we should think about commenting test cases more, sometimes I don't know what the intention of a test case was in the first place, so fixing it if goes wrong is harder.

@@ -1102,8 +1104,16 @@ ref<klee::ConstantExpr> Executor::evalConstant(const Constant *c) {
}
ref<Expr> res = ConcatExpr::createN(kids.size(), kids.data());
return cast<ConstantExpr>(res);
} else if (const ConstantVector *cv = dyn_cast<ConstantVector>(c)) {
ref<Expr> *kids = new ref<Expr>[ cv->getNumOperands() ];

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

Don't use C-style new/free allocation, llvm::SmallVector is the better choice and gets deallocated if it goes out of scope.
And one line less code ;)

This comment has been minimized.

Copy link
@delcypher

delcypher Jul 6, 2017

Author Contributor

Yes this seems like a good idea. The reason the code is written this way is that I inherited this code from KLEE-FP and didn't bother to change it.

@@ -1935,27 +1935,43 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
// Arithmetic / logical

case Instruction::Add: {
assert(i->getOperand(0)->getType()->isIntegerTy() &&

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

I agree with @ccadar and @delcypher ;)
Too many checks, it clutters the code a lot. Can this be improved?

case Instruction::InsertElement: {
InsertElementInst *iei = cast<InsertElementInst>(i);
ref<Expr> vec = eval(ki, 0, state).value;
ref<Expr> newElt = eval(ki, 1, state).value;

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

Yes, we should check the width if it is equivalent.

ref<Expr> newElt = eval(ki, 1, state).value;
ref<Expr> idx = eval(ki, 2, state).value;

if (!isa<ConstantExpr>(idx)) {

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

As you need a ConstantExpr anyway later, do a dyn_cast<>() and check for nullptr.

unsigned EltBits = getWidthForLLVMType(vt->getElementType());

if (iIdx >= vt->getNumElements()) {
// Out of bounds write

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

comment is superfluous at that point.

This comment has been minimized.

Copy link
@delcypher

delcypher Jul 6, 2017

Author Contributor

If you know the code well yes, if you don't then I don't think it's superfluous.

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

Agree.

}

const unsigned elementCount = vt->getNumElements();
ref<Expr> *elems = new ref<Expr>[elementCount];

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

Please use llvm::SmallVector here as well

break;
}
case Instruction::ExtractElement: {
ExtractElementInst *eei = cast<ExtractElementInst>(i);

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

constify and move to point where you actually need the variable

This comment has been minimized.

Copy link
@delcypher

delcypher Jul 6, 2017

Author Contributor

I disagree. I deliberately wrote it this away trying to avoid "the pyramid of doom" by preferring early exit. Unless you mean doing the dyn_cast<> outside of the if conditional and then checking if the result is nullptr to do early exit. In which case I would agree that's a nice change because it means doing the LLVM RTTI style type check once instead of twice.

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

Doing the check just once was my point. And I absolutely agree with you to prefer an early exit.

ref<Expr> vec = eval(ki, 0, state).value;
ref<Expr> idx = eval(ki, 1, state).value;

if (!isa<ConstantExpr>(idx)) {

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

dyn_cast and constify

This comment has been minimized.

Copy link
@delcypher

delcypher Jul 6, 2017

Author Contributor

See previous comment about "the pyramid of doom"

case Instruction::ShuffleVector:
terminateStateOnError(state, "XXX vector instructions unhandled",
Unhandled);
llvm_unreachable(

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

Why not terminate the state? The whole KLEE execution gets killed.
It is similar to the insufficient system model we have, therefore it should be handled the same way.

This comment has been minimized.

Copy link
@delcypher

delcypher Jul 6, 2017

Author Contributor

I was doing that because in principle we should never see the ShuffleVector instruction. However terminateStateOnError() is more robust and will have well defined behaviour in a release build.

// other than InsertElementInst and ExtractElementInst.
//
// NOTE: Must come before division/overshift checks because those passes
// don't know how to handle vector instructions.

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

fix comment: "how"

This comment has been minimized.

Copy link
@delcypher

delcypher Jul 6, 2017

Author Contributor

Could you elaborate. I'm not sure what you're suggesting. Are you saying s/how/"how"/?

This comment has been minimized.

Copy link
@MartinNowack

MartinNowack Jul 6, 2017

Contributor

Ignore this. I must have read something else.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jul 6, 2017

@MartinNowack

Too many checks, it clutters the code a lot. Can this be improved?

I have two ideas

  • MACROS. Define some short hand macros that do the assertion checks
  • A sanity check LLVM pass. The Executor would run this pass just before execution starts (i.e. the IR has already been modified so we can assume that what the pass sees is what the Executor executes). This pass would check the instructions where we expect the "no vector operand" invariant to hold and abort if the invariant does not hold.

However I don't really have a problem with the asserts. They actually document an invariant we expect to hold at that point in the code. If we move those checks out of the code and somewhere else it becomes harder to see the relationship between the invariant and the place in the code we expect the invariant to hold. However the checks are syntactically are quite long though and will be prone to causing lots of breakages if LLVM's API changes. So the macro option might be sensible here.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jul 6, 2017

For reference the macro option would look something like

#define ASSERT_OPERAND_IS_SCALAR_INT(I, N) \
  assert(I->getOperand(N)->getType()->isIntegerTy() && "Operand should be scalar integer")
#define ASSERT_OPERAND_IS_SCALAR_FLOAT(I, N) \
  assert(I->getOperand(N)->getType()->isFloatingPointTy() && "Operand should be scalar float")

which would then look like

  case Instruction::Add: {
    ASSERT_OPERAND_IS_SCALAR_INT(i, 0);
    ASSERT_OPERAND_IS_SCALAR_INT(i, 1);
    ref<Expr> left = eval(ki, 0, state).value;
    ref<Expr> right = eval(ki, 1, state).value;
    bindLocal(ki, state, AddExpr::create(left, right));
    break;
  }
@MartinNowack

This comment has been minimized.

Copy link
Contributor

commented Jul 6, 2017

@delcypher I like the idea with the additional pass a lot.
I agree with the point that we have assertions to directly communicate the intention, which is a good thing. I'm not a big fan of hiding this stuff in macros. The problem with those assertions are that they are currently on one of the hottest paths of KLEE. Checking those properties for billions of instructions should be avoided.

The good thing about macros would be that we could easily enable them if we have a debug build and otherwise disable them. And the effort to implement them would be less.

@ccadar

This comment has been minimized.

Copy link
Contributor

commented Jul 6, 2017

Yes, the extra pass sounds best, but I'm happy to go with asserts too at this point.
I agree tests should be commented more.

@ccadar

This comment has been minimized.

Copy link
Contributor

commented Jul 16, 2017

I'd like to see this PR merged soon, but I am becoming more reticent about having these large number of asserts validating each operation, as they clutter the code and also affect the performance of the assert build (which right now is the default!).

What I suggest is the following:

  1. address the easy but useful code comments from @MartinNowack
  2. remove the asserts
  3. merge
  4. open a todo issue to implement the sanity-check LLVM pass (we should do that, but I don't think it's absolutely needed at this point)

What do you think?

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jul 16, 2017

@ccadar I'd like to implement the pass because it's not too much work. However it'll be a few days before I have time to do this.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jul 17, 2017

I've addressed most of @MartinNowack 's comments but please don't merge yet. I still need to write the pass and remove the asserts.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jul 18, 2017

@ccadar @MartinNowack The pass is now implemented and assertions removed. This should be ready to go now. Please review, hopefully it's just "bikeshedding" left as the names I've picked could be better.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jul 18, 2017

Eurgh damn it. LLVM 2.9 build is broken.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jul 18, 2017

Build is now fixed


// Enforce the operand type invariants that the Executor expects
if (!roascp->checkPassed()) {
klee_error("Unexpected vector operands detected");

This comment has been minimized.

Copy link
@ccadar

ccadar Jul 18, 2017

Contributor

Really minor, but I would drop "vector" from this message, as there might be other issues detected, e.g., different operand types to a select.

This comment has been minimized.

Copy link
@delcypher

delcypher Jul 19, 2017

Author Contributor

Perhaps we ought to rename the pass then because the pass name implies it only checks that some operands are of scalar type. Suggestions for a name? InstructionOperandTypeCheckPass?

This comment has been minimized.

Copy link
@ccadar

ccadar Jul 19, 2017

Contributor

Yes, I think that's a better name. BTW, I would also add a comment upfront that this pass depends on the scalarizer one.

@ccadar

This comment has been minimized.

Copy link
Contributor

commented Jul 18, 2017

Thanks, @delcypher , this looks good to me, modulo squashing some of the commits.

Implement basic support for vectorized instructions.
We use LLVM's Scalarizer pass to remove most vectorized code so that the
Executor only needs to support the InsertElement and ExtractElement
instructions.

This pass was not available in LLVM 3.4 so to support that LLVM version
the pass has been back ported.

To check that the Executor is not receiving vector operand types
that it can't handle assertions have been added.

There are a few limitations to this implementation.

* The InsertElement and ExtractElement index cannot be symbolic.
* There is no support for LLVM < 3.4.

@delcypher delcypher force-pushed the delcypher:vectorized_instructions branch from bfb2937 to 41e1116 Jul 19, 2017

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jul 19, 2017

Thanks, @delcypher , this looks good to me, modulo squashing some of the commits.

@ccadar Done. I've kept the commit that removes the asserts and replaces them with a pass as a separate commit because I think it's important we preserve the history of doing this so it's possible for someone to work out why it's implemented this way.

@ccadar

This comment has been minimized.

Copy link
Contributor

commented Jul 19, 2017

Hi @delcypher , I agree we should have two commits there. Thanks again for your work on this, I'm happy to approve it. Let's wait just a bit longer before merging it, to give @MartinNowack an opportunity to react.

@ccadar
ccadar approved these changes Jul 19, 2017
@MartinNowack

This comment has been minimized.

Copy link
Contributor

commented Jul 20, 2017

Beside the remark about the comments, I'm fine with the changes. Great job!

Replace assertions of types on LLVM instructions in the Executor with a
pass that checks these assertions. This improves several things.

* This pass provides more friendly messages than assertions in that it
just emits a warning and carries on checking the rest of the
instructions.

* The takes the checks outside of the Executor's hot path and so avoids
checking the same instruction multiple times. Now each instruction
is only checked once just before execution starts.

The disadvantage of this approach is the check for invariants we expect
to hold have been pulled far away from where we expect them to hold.
After discussion with @ccadar and @MartinNowack it was decided we will
take this hit to readability for better performance and simpler code in
the Executor.

@delcypher delcypher force-pushed the delcypher:vectorized_instructions branch from 41e1116 to ffe695c Jul 20, 2017

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Jul 20, 2017

@MartinNowack

Beside the remark about the comments, I'm fine with the changes. Great job!

Comments fixed. I'll merge once I see CI has passed.

@ccadar ccadar merged commit 051e44e into klee:master Jul 20, 2017

1 check passed

continuous-integration/travis-ci/pr The Travis CI build passed
Details
@ccadar

This comment has been minimized.

Copy link
Contributor

commented Jul 20, 2017

Thanks again for this contribution, @delcypher , merged!

@andreamattavelli , @delcypher , @MartinNowack I plan to do a new release now (i.e. today/tomorrow), so please don't merge more things until that is completed. Thanks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
4 participants
You can’t perform that action at this time.