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

fixed minor bugs #733

Merged
merged 2 commits into from
Mar 19, 2018
Merged

fixed minor bugs #733

merged 2 commits into from
Mar 19, 2018

Conversation

gitoleg
Copy link
Contributor

@gitoleg gitoleg commented Oct 26, 2017

forgotten parentheses in shift instructions

compare with bap.1.2.0:

  match st with
  | LSHIFT -> Bil.(Cast (LOW, !!bool_t, Var origDEST lsr (size - Var origCOUNT)))
  | RSHIFT | ARSHIFT ->
         Bil.(Cast (HIGH, !!bool_t, Var origDEST lsl (size - Var origCOUNT)))
  | _ -> failwith "impossible"

@ivg ivg self-assigned this Oct 26, 2017
@ivg ivg self-requested a review October 26, 2017 14:49
Copy link
Member

@ivg ivg left a comment

Choose a reason for hiding this comment

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

there are at least two more errors of the same kind, on line 860 and 862 (I'm pretty consistent, when I'm introducing bugs :D) Can you fix them also?

It's kind of disappointing that bap-veri was unable to find them. Did we just miss it from the output, or it didn't occur in a binary, or veri misses it due to a bug?

@ivg
Copy link
Member

ivg commented Oct 26, 2017

Since this PR and therefore, I would like that every change that affects instruction semantics, i.e., something that deals with BIL transformations or lifters, should be accompanied with the run of veri, that proves that we don't have any regressions. I think that we need to create a repository that will contain logs from bap-veri runs, so that the proof that we don't have a regression is encoded as a commit to this repo.

@gitoleg
Copy link
Contributor Author

gitoleg commented Mar 16, 2018

finally, your wish came true!
What our bil-tests said before:

XFAIL: veri-x86_64 for SHL
XFAIL: veri-x86_64 for SHLCL
XFAIL: veri-x86_64 for SHR
XFAIL: veri-x86_64 for SHRCL

And now those instructions have PASS status!
Anyway, will update testsuite to delete fail expectation

@ivg ivg merged commit 54b305d into BinaryAnalysisPlatform:master Mar 19, 2018
@gitoleg gitoleg deleted the minor-bugs-fix branch March 26, 2018 20:16
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.

2 participants