Add Laurel tests for Java machine integers as constrained types

[tautschnig]

Model Java primitive integer types (byte, short, char, int, long) as Laurel constrained types over mathematical int with range predicates.

Tests cover:

• Range constraints on inputs and outputs
• Valid and invalid returns (overflow/underflow detection)
• Cross-type widening (byte→int safe, int→byte unsafe)
• Arithmetic within range
• Opaque procedure contracts with range guarantees
• Quantifiers over constrained types

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[Copilot]

Pull request overview

Adds Laurel test coverage for modeling Java primitive integer types as constrained types over mathematical int, and updates the Laurel→CBMC test runner to execute .lr.st files via the GOTO/CBMC pipeline.

Changes:

• Added a new Laurel CBMC pipeline test file for constrained “Java integer” types.
• Added a new Lean example/test (T18_JavaMachineIntegers) exercising constrained Java integer semantics (ranges, invalid returns, widening, arithmetic, opaque contracts, quantifiers).
• Reworked run_laurel_cbmc_tests.sh to run strata laurelAnalyzeToGoto + symtab2gb + per-function CBMC checks.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 4 comments.

File	Description
StrataTest/Languages/Laurel/tests/test_java_integers.lr.st	Adds CBMC-pipeline Laurel tests for constrained Java-like integer types.
StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh	Replaces the expected-property-based runner with a new per-function CBMC runner.
StrataTest/Languages/Laurel/Examples/Fundamentals/T18_JavaMachineIntegers.lean	Adds a comprehensive Lean-side Laurel example/test covering constrained Java machine integers.

Comments suppressed due to low confidence (1)

StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh:80

• The script currently never returns a non-zero exit status. Even when errors is incremented (translation/symtab2gb/CBMC issues), the last command is echo, so CI will still pass. Add an explicit exit condition at the end (e.g., [ "$errors" -eq 0 ] or exit "$errors").

echo ""
echo "Results: $passed passed, $errors errors"

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[keyboardDrummer]

What is this test adding that the existing tests for constrained types did not add yet? I don't think we need Java specific tests in the Laurel codebase: those can live on the JVerify side.

[tautschnig]

None of the existing tests exercised use of constrained types that are equivalent to bitvector types. (I have a follow-up PR that will introduce an option to translate such types to Core's bitvector types.)

[keyboardDrummer]

None of the existing tests exercised use of constrained types that are equivalent to bitvector types. (I have a follow-up PR that will introduce an option to translate such types to Core's bitvector types.)

A PR that would translate constrained types with specific constraints to BV types? That seems like too implicit behavior. Why not make BV types explicit in Laurel?

[tautschnig]

No, it won't be implicit behaviour, it will be controlled via an option. The goal is to be able to compare the different encoding approaches, so making BV types explicit in Laurel could very well be done, but is somewhat orthogonal to that.

[keyboardDrummer]

Is there a use-case for automatically translating constrained types to bitvectors? If a front-end wants to use bitvectors, why not use them directly (once they exist in Laurel) ?

I imagine we'll have options that allow configuring how to verify Laurel bitvectors, but I don't see a need for an option to convert constrained types to bvs.

Also, translating constrained types into bitvectors seems complicated. What if you have a constrained type like:

constrained nat32 := i: int | i >= 0 && i < ...

Are you going to translate that into

constrained nat32 := i: i32 | i >= 0

?

I'd rather ask the front-end to immediately write the second version.

[tautschnig]

My take so far is a very simple one: only use bitvectors when the constrained type directly maps to a bitvector. So, yes, I can do a PR that introduces bitvectors to Laurel, and then future front-ends can use those directly. My proposed constrained-types-to-bitvectors path should then become one available as a Core-to-Core translation (and perhaps one that should be available in both directions). That would then provide flexibility for verification as you suggest.

[keyboardDrummer]

My proposed constrained-types-to-bitvectors path should then become one available as a Core-to-Core translation

I don't understand what you mean. Core doesn't have a concept of constrained types so how could such a path exist as a Core to Core translation?

But the heart of my feedback remains the same. If explicit bv types are available, then I don't see a use-case for a translation that maps certain constrained types to bitvectors. Do you?

[tautschnig]

Quantifiers and bitvectors don't play well together in SMT solvers, so I do think it is reasonable that we have a verification path that uses constrained types rather than bitvectors. But, yes, this should be a decision to be made with respect to a specific back-end rather than prematurely by a front-end.

[tautschnig]

FWIW: I'm on the cbmc failure seen in the CI job, fix will follow in a separate PR that this one will then depend on.