Skip to content

Conversation

@CatarinaGamboa
Copy link
Collaborator

Previously, we only tested with a small set of long operations, which did not include operations with Long values inside predicates or long values with L.
Example that would not be properly checked:

void testDiv(){
        // we have a mask and want to see if the value in position [-4] is a 2
        @Refinement("((v/4096) % 16) == 2")
        long v = 0x01000000666663666L;
}

Now we can check this and see that the value is 3 and not 2 so an error.

This PR makes changes in:

  • New LiteralLong AST node (we had LiteralInt, LiteralDouble, etc, no Long)
  • Added LiteralLong through the full pipeline: visitor interface, Z3 translation (using mkInt for exact integer
    semantics), type inference, etc
  • In SMT solver translation to long
  • Tests in testsuite for these additions

Copy link
Collaborator

@rcosta358 rcosta358 left a comment

Choose a reason for hiding this comment

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

lgtm

try {
return new LiteralInt(text);
} catch (NumberFormatException e) {
return new LiteralLong(text);
Copy link
Collaborator

Choose a reason for hiding this comment

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

So we only convert a long to a LiteralLong if it overflows 32 bits, even if it was declared as a long, right?

Also, instead of using a try-catch here, we could do this:

String text = literalContext.INT().getText();
long value = Long.parseLong(text);
if (value >= Integer.MIN_VALUE && value <= Integer.MAX_VALUE) {
    return new LiteralInt(text);
} else {
    return new LiteralLong(text);
}

Both are fine for me. Which one do you prefer?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

to have literalContext.LONG() i needed to change the grammar in .g4 and i didn't want to 😅 ‍
We could not catch the exception its true, it probably is more readable so I'll change it! Athough we usually have more examples with ints but its fine

@CatarinaGamboa CatarinaGamboa merged commit 1b290cb into main Jan 30, 2026
1 check passed
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