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

Fix AcInstrDecodeTest>>testPowerAddiSymbolic #36

Merged
merged 2 commits into from
Jun 19, 2024
Merged

Conversation

shingarov
Copy link
Owner

A trivial push yesterday (classifying a method) re-triggered CI and now https://github.com/shingarov/Pharo-ArchC/actions/runs/9171675951/job/25216516144 . I don't understand how this could possibly pass before.

In this line:

self assert: (instr fieldValue: 'd') equals: 'x'

the "instr fieldValue: 'd'" is a Z3Int, so the #= down in #assert:equals:
coerces the 'x' to a Z3Int.  So now we have two 'x' symbols: a BV16 'x'
and an Int 'x', which are not necessarily equal.
The correct thing to do is to start from the same BV 'x',
and compare the Int interpretation of `d` to the signed Int
interpretation of 'x'.
@janvrany
Copy link
Collaborator

janvrany commented May 22, 2024

I don't understand how this could possibly pass before.

Neither do I, not yet. But this is worth investigating...

@janvrany
Copy link
Collaborator

I don't understand how this could possibly pass before.

It did pass before MA commit shingarov/MachineArithmetic@216a5c8.

This is because the before that, in signedValue there was:

self simplify isNumeral ifFalse: [ ^self ].

The problem is fieldValue: returns sometimes an integer, sometimes Z3Int and sometimes bitvector. Worse, it tells you it does return an Integer.

@janvrany janvrany merged commit c0f4aab into pure-z3 Jun 19, 2024
2 checks passed
@janvrany janvrany deleted the fix-addi-symbolic branch June 19, 2024 13:23
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