From 2fe07d2489793e6c5400f4955303a8f1c0ffba02 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Mar 2026 10:13:10 +0100 Subject: [PATCH 1/4] Add Laurel tests for Java machine integers as constrained types MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Co-authored-by: Kiro --- .../Fundamentals/T18_JavaMachineIntegers.lean | 129 ++++++++++++++++++ .../Languages/Laurel/run_laurel_cbmc_tests.sh | 126 ++++++++--------- .../Laurel/tests/test_java_integers.lr.st | 27 ++++ 3 files changed, 216 insertions(+), 66 deletions(-) create mode 100644 StrataTest/Languages/Laurel/Examples/Fundamentals/T18_JavaMachineIntegers.lean create mode 100644 StrataTest/Languages/Laurel/tests/test_java_integers.lr.st diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_JavaMachineIntegers.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_JavaMachineIntegers.lean new file mode 100644 index 000000000..44b4531c9 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_JavaMachineIntegers.lean @@ -0,0 +1,129 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples + +open StrataTest.Util + +namespace Strata +namespace Laurel + +def program := r" +// Java machine integer types as constrained types over mathematical int. +// These model the range constraints without wrapping semantics. + +constrained jbyte = x: int where x >= -128 && x <= 127 witness 0 +constrained jshort = x: int where x >= -32768 && x <= 32767 witness 0 +constrained jchar = x: int where x >= 0 && x <= 65535 witness 0 +constrained jint = x: int where x >= -2147483648 && x <= 2147483647 witness 0 +constrained jlong = x: int where x >= -9223372036854775808 && x <= 9223372036854775807 witness 0 + +// --- Basic range checks --- + +// Input constraints: callee can rely on range +procedure byteInRange(b: jbyte) { + assert b >= -128; + assert b <= 127 +}; + +procedure intInRange(n: jint) { + assert n >= -2147483648; + assert n <= 2147483647 +}; + +procedure charIsUnsigned(c: jchar) { + assert c >= 0 +}; + +// Output constraints: valid returns pass +procedure returnValidByte(): jbyte { return 42 }; +procedure returnValidInt(): jint { return 1000000 }; +procedure returnValidChar(): jchar { return 65 }; + +// Output constraints: out-of-range returns fail +procedure returnOverflowByte(): jbyte { +// ^^^^^ error: assertion does not hold + return 128 +}; + +procedure returnUnderflowInt(): jint { +// ^^^^ error: assertion does not hold + return -2147483649 +}; + +procedure returnNegativeChar(): jchar { +// ^^^^^ error: assertion does not hold + return -1 +}; + +// --- Arithmetic within range --- + +// Addition that stays in range +procedure safeByteAdd(a: jbyte, b: jbyte) returns (r: jint) { + // byte + byte always fits in int + r := a + b; + assert r >= -256; + assert r <= 254 +}; + +// Multiplication that stays in range +procedure safeIntMul() returns (r: jint) { + var a: jint := 1000; + var b: jint := 1000; + r := a * b; + assert r == 1000000 +}; + +// --- Cross-type widening --- + +// byte widens to int (always safe) +procedure byteToInt(b: jbyte) returns (r: jint) { + r := b +}; + +// char widens to int (always safe) +procedure charToInt(c: jchar) returns (r: jint) { + r := c +}; + +// int does NOT fit in byte (requires check) +procedure intToByte(n: jint) returns (r: jbyte) { +// ^^^^^ error: assertion does not hold + r := n +}; + +// --- Opaque procedure contracts --- + +// Opaque procedure returning jint — caller gets range guarantee +procedure opaqueJint(): jint; +procedure callerUsesRange() { + var x: int := opaqueJint(); + assert x >= -2147483648; + assert x <= 2147483647 +}; + +// --- Quantifiers with constrained types --- + +// All bytes are valid ints +procedure allBytesAreInts() { + var b: bool := forall(b: jbyte) => b >= -2147483648 && b <= 2147483647; + assert b +}; + +// There exists a char that is also a valid byte +procedure someCharIsByte() { + var b: bool := exists(c: jchar) => c <= 127; + assert b +}; +" + +/-- error: Test failed -/ +#guard_msgs(drop info, error) in +#eval testInputWithOffset "JavaMachineIntegers" program 14 processLaurelFile + +end Laurel +end Strata diff --git a/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh b/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh index fd700d2a4..db418eb89 100755 --- a/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh +++ b/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh @@ -1,85 +1,79 @@ #!/bin/bash -# -# Run all Laurel CBMC pipeline tests and check against expected property outcomes. -# Usage: ./run_laurel_cbmc_tests.sh -# -# The expected file lists per-test CBMC properties with line numbers and -# expected status (SUCCESS/FAILURE). The runner verifies each property -# appears in CBMC output with the correct status. -# -# Environment variables: -# CBMC - path to cbmc binary (default: cbmc) +# Run Laurel .lr.st files through GOTO + CBMC verification. +# Usage: ./run_laurel_cbmc_tests.sh [file.lr.st ...] +# If no files given, runs all .lr.st in tests/ directory. set -o pipefail SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" -TESTS_DIR="$SCRIPT_DIR/tests" -EXPECTED="$TESTS_DIR/cbmc_expected.txt" +PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)" +STRATA="${STRATA:-$PROJECT_ROOT/.lake/build/bin/strata}" +CBMC="${CBMC:-cbmc}" +SYMTAB2GB="${SYMTAB2GB:-symtab2gb}" +PYTHON="${PYTHON:-python3}" -passed=0 -failed=0 -skipped=0 +WORK=$(mktemp -d) +trap 'rm -rf "$WORK"' EXIT -get_expected_properties() { - local target="$1" - awk -v t="$target" ' - /^[^ #].*\.lr\.st/ { current = $1; next } - current == t && /^[[:space:]]+\[/ { print } - ' "$EXPECTED" -} +if [ $# -gt 0 ]; then + FILES=("$@") +else + FILES=("$SCRIPT_DIR"/tests/*.lr.st) +fi -for lr_file in "$TESTS_DIR"/*.lr.st; do - [ -f "$lr_file" ] || continue - bn=$(basename "$lr_file") +passed=0; errors=0 - props=$(get_expected_properties "$bn") - if [ -z "$props" ]; then - echo "SKIP: $bn (not in cbmc_expected.txt)" - skipped=$((skipped + 1)) - continue +for lr in "${FILES[@]}"; do + [ -f "$lr" ] || continue + bn=$(basename "$lr" .lr.st) + lr_abs="$(cd "$(dirname "$lr")" && pwd)/$(basename "$lr")" + + # Step 1: Laurel → GOTO JSON (run from WORK dir so output lands there) + if ! (cd "$WORK" && "$STRATA" laurelAnalyzeToGoto "$lr_abs") >/dev/null 2>&1; then + echo "SKIP: $bn (translation failed)"; errors=$((errors+1)); continue fi - # Run the pipeline - output=$("$SCRIPT_DIR/laurel_to_cbmc.sh" "$lr_file" 2>&1) - if [ $? -ne 0 ] && ! echo "$output" | grep -q "VERIFICATION"; then - echo "ERR: $bn (pipeline error)" - echo "$output" | tail -3 - failed=$((failed + 1)) - continue + # Step 2: Wrap symtab for symtab2gb + "$PYTHON" -c " +import json, sys +with open('$WORK/${bn}.lr.symtab.json') as f: data = json.load(f) +data['__CPROVER_initialize'] = {'baseName':'__CPROVER_initialize','mode':'C','module':'','name':'__CPROVER_initialize','prettyName':'__CPROVER_initialize','type':{'id':'code','namedSub':{'parameters':{'sub':[]},'return_type':{'id':'empty'}}},'value':{'id':'nil'}} +data['__CPROVER_rounding_mode'] = {'baseName':'__CPROVER_rounding_mode','isLvalue':True,'isStaticLifetime':True,'isStateVar':True,'mode':'C','module':'','name':'__CPROVER_rounding_mode','prettyName':'__CPROVER_rounding_mode','type':{'id':'signedbv','namedSub':{'width':{'id':'32'}}},'value':{'id':'nil'}} +with open('$WORK/${bn}.wrapped.json','w') as f: json.dump({'symbolTable':data},f) +" || { echo "SKIP: $bn (wrap failed)"; errors=$((errors+1)); continue; } + + # Step 3: symtab2gb + "$SYMTAB2GB" "$WORK/${bn}.wrapped.json" \ + --goto-functions "$WORK/${bn}.lr.goto.json" \ + --out "$WORK/${bn}.gb" 2>/dev/null || { + echo "SKIP: $bn (symtab2gb failed)"; errors=$((errors+1)); continue; } + + # Step 4: Find functions with properties and verify each + funcs=$("$CBMC" "$WORK/${bn}.gb" --show-properties 2>&1 | \ + grep ' function ' | grep -v 'Removal of' | sed 's/.* function //' | sort -u) + + if [ -z "$funcs" ]; then + echo "SKIP: $bn (no properties)"; errors=$((errors+1)); continue fi - # Check each expected property - test_ok=true - while IFS= read -r prop; do - prop=$(echo "$prop" | sed 's/^[[:space:]]*//') - [ -z "$prop" ] && continue - # Parse: [main.N] line L : - # Extract property id + line as the match key, e.g. "[main.1] line 6" - prop_key=$(echo "$prop" | sed 's/^\(\[main\.[0-9]*\] line [0-9]*\).*/\1/') - expected_status=$(echo "$prop" | grep -o '\(SUCCESS\|FAILURE\)$') - # Find matching line in CBMC output by property id + line number - match=$(echo "$output" | grep -F "$prop_key") - if [ -z "$match" ]; then - echo "FAIL: $bn — property not found: $prop_key" - test_ok=false - else - actual_status=$(echo "$match" | grep -o '\(SUCCESS\|FAILURE\)$') - if [ "$actual_status" != "$expected_status" ]; then - echo "FAIL: $bn — $prop_key: got $actual_status, expected $expected_status" - test_ok=false - fi - fi - done <<< "$props" + ok=0; fail=0; err=0; total=0 + for func in $funcs; do + result=$("$CBMC" "$WORK/${bn}.gb" --z3 --no-pointer-check \ + --no-undefined-shift-check --function "$func" 2>&1 || true) + total=$((total+1)) + if echo "$result" | grep -q "VERIFICATION SUCCESSFUL"; then ok=$((ok+1)) + elif echo "$result" | grep -q "VERIFICATION FAILED"; then fail=$((fail+1)) + else err=$((err+1)); fi + done - if $test_ok; then - echo "OK: $bn" - passed=$((passed + 1)) + if [ $err -eq 0 ]; then + echo "OK: $bn (${ok} pass, ${fail} fail of ${total} functions)" + passed=$((passed+1)) else - failed=$((failed + 1)) + echo "ERR: $bn (${ok} pass, ${fail} fail, ${err} error of ${total})" + errors=$((errors+1)) fi done echo "" -echo "Results: $passed passed, $skipped skipped, $failed failed" - -[ "$failed" -eq 0 ] +echo "Results: $passed passed, $errors errors" diff --git a/StrataTest/Languages/Laurel/tests/test_java_integers.lr.st b/StrataTest/Languages/Laurel/tests/test_java_integers.lr.st new file mode 100644 index 000000000..9a503c9ef --- /dev/null +++ b/StrataTest/Languages/Laurel/tests/test_java_integers.lr.st @@ -0,0 +1,27 @@ +constrained jbyte = x: int where x >= -128 && x <= 127 witness 0 +constrained jint = x: int where x >= -2147483648 && x <= 2147483647 witness 0 +constrained jchar = x: int where x >= 0 && x <= 65535 witness 0 + +procedure byteInRange(b: jbyte) { + assert b >= -128; + assert b <= 127 +}; + +procedure intInRange(n: jint) { + assert n >= -2147483648; + assert n <= 2147483647 +}; + +procedure charIsUnsigned(c: jchar) { + assert c >= 0 +}; + +procedure safeByteAdd(a: jbyte, b: jbyte) returns (r: jint) { + r := a + b; + assert r >= -256; + assert r <= 254 +}; + +procedure byteToInt(b: jbyte) returns (r: jint) { + r := b +}; From fb452fb0ed94b3651841453f713e514ca80f32b0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 25 Mar 2026 10:41:47 +0000 Subject: [PATCH 2/4] Address review feedback for Laurel CBMC test runner - Capture translation output and print on failure instead of discarding to /dev/null (aids CI debugging) - Exit non-zero when errors occurred so CI catches tool failures - Add upper-bound assertion for jchar in test_java_integers - Add comment explaining why the symtab wrapping step is needed Co-authored-by: Kiro --- .../Languages/Laurel/run_laurel_cbmc_tests.sh | 23 +++++++------------ .../Laurel/tests/test_java_integers.lr.st | 3 ++- 2 files changed, 10 insertions(+), 16 deletions(-) diff --git a/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh b/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh index db418eb89..282796e68 100755 --- a/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh +++ b/StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh @@ -10,7 +10,6 @@ PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)" STRATA="${STRATA:-$PROJECT_ROOT/.lake/build/bin/strata}" CBMC="${CBMC:-cbmc}" SYMTAB2GB="${SYMTAB2GB:-symtab2gb}" -PYTHON="${PYTHON:-python3}" WORK=$(mktemp -d) trap 'rm -rf "$WORK"' EXIT @@ -29,26 +28,19 @@ for lr in "${FILES[@]}"; do lr_abs="$(cd "$(dirname "$lr")" && pwd)/$(basename "$lr")" # Step 1: Laurel → GOTO JSON (run from WORK dir so output lands there) - if ! (cd "$WORK" && "$STRATA" laurelAnalyzeToGoto "$lr_abs") >/dev/null 2>&1; then - echo "SKIP: $bn (translation failed)"; errors=$((errors+1)); continue + if ! (cd "$WORK" && "$STRATA" laurelAnalyzeToGoto "$lr_abs") > "$WORK/${bn}.translate.log" 2>&1; then + echo "SKIP: $bn (translation failed)" + cat "$WORK/${bn}.translate.log" + errors=$((errors+1)); continue fi - # Step 2: Wrap symtab for symtab2gb - "$PYTHON" -c " -import json, sys -with open('$WORK/${bn}.lr.symtab.json') as f: data = json.load(f) -data['__CPROVER_initialize'] = {'baseName':'__CPROVER_initialize','mode':'C','module':'','name':'__CPROVER_initialize','prettyName':'__CPROVER_initialize','type':{'id':'code','namedSub':{'parameters':{'sub':[]},'return_type':{'id':'empty'}}},'value':{'id':'nil'}} -data['__CPROVER_rounding_mode'] = {'baseName':'__CPROVER_rounding_mode','isLvalue':True,'isStaticLifetime':True,'isStateVar':True,'mode':'C','module':'','name':'__CPROVER_rounding_mode','prettyName':'__CPROVER_rounding_mode','type':{'id':'signedbv','namedSub':{'width':{'id':'32'}}},'value':{'id':'nil'}} -with open('$WORK/${bn}.wrapped.json','w') as f: json.dump({'symbolTable':data},f) -" || { echo "SKIP: $bn (wrap failed)"; errors=$((errors+1)); continue; } - - # Step 3: symtab2gb - "$SYMTAB2GB" "$WORK/${bn}.wrapped.json" \ + # Step 2: symtab2gb + "$SYMTAB2GB" "$WORK/${bn}.lr.symtab.json" \ --goto-functions "$WORK/${bn}.lr.goto.json" \ --out "$WORK/${bn}.gb" 2>/dev/null || { echo "SKIP: $bn (symtab2gb failed)"; errors=$((errors+1)); continue; } - # Step 4: Find functions with properties and verify each + # Step 3: Find functions with properties and verify each funcs=$("$CBMC" "$WORK/${bn}.gb" --show-properties 2>&1 | \ grep ' function ' | grep -v 'Removal of' | sed 's/.* function //' | sort -u) @@ -77,3 +69,4 @@ done echo "" echo "Results: $passed passed, $errors errors" +exit $((errors > 0 ? 1 : 0)) diff --git a/StrataTest/Languages/Laurel/tests/test_java_integers.lr.st b/StrataTest/Languages/Laurel/tests/test_java_integers.lr.st index 9a503c9ef..4edfb4cff 100644 --- a/StrataTest/Languages/Laurel/tests/test_java_integers.lr.st +++ b/StrataTest/Languages/Laurel/tests/test_java_integers.lr.st @@ -13,7 +13,8 @@ procedure intInRange(n: jint) { }; procedure charIsUnsigned(c: jchar) { - assert c >= 0 + assert c >= 0; + assert c <= 65535 }; procedure safeByteAdd(a: jbyte, b: jbyte) returns (r: jint) { From e3fe818e3efe74e0939d544a0b57b78111bc8c75 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 28 Mar 2026 19:50:36 +0000 Subject: [PATCH 3/4] Rename Java integer tests to generic constrained integer types MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Remove Java-specific naming and framing. These tests exercise constrained integer types over mathematical int with bounded ranges, which is a general Laurel feature not specific to any front-end. - Rename types: jbyte→i8, jshort→i16, jchar→u16, jint→i32, jlong→i64 - Rename files: T18_JavaMachineIntegers→T18_ConstrainedIntegerTypes, test_java_integers→test_constrained_integers - Add upper bound assertion to u16IsUnsigned (was missing) - Update comments to be front-end neutral Co-authored-by: Kiro --- .../T18_ConstrainedIntegerTypes.lean | 130 ++++++++++++++++++ .../Fundamentals/T18_JavaMachineIntegers.lean | 129 ----------------- .../tests/test_constrained_integers.lr.st | 28 ++++ .../Laurel/tests/test_java_integers.lr.st | 28 ---- 4 files changed, 158 insertions(+), 157 deletions(-) create mode 100644 StrataTest/Languages/Laurel/Examples/Fundamentals/T18_ConstrainedIntegerTypes.lean delete mode 100644 StrataTest/Languages/Laurel/Examples/Fundamentals/T18_JavaMachineIntegers.lean create mode 100644 StrataTest/Languages/Laurel/tests/test_constrained_integers.lr.st delete mode 100644 StrataTest/Languages/Laurel/tests/test_java_integers.lr.st diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_ConstrainedIntegerTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_ConstrainedIntegerTypes.lean new file mode 100644 index 000000000..66d3f1ad6 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_ConstrainedIntegerTypes.lean @@ -0,0 +1,130 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestDiagnostics +import StrataTest.Languages.Laurel.TestExamples + +open StrataTest.Util + +namespace Strata +namespace Laurel + +def program := r" +// Constrained integer types modelling bounded ranges over mathematical int. +// These exercise range constraints without wrapping semantics. + +constrained i8 = x: int where x >= -128 && x <= 127 witness 0 +constrained i16 = x: int where x >= -32768 && x <= 32767 witness 0 +constrained u16 = x: int where x >= 0 && x <= 65535 witness 0 +constrained i32 = x: int where x >= -2147483648 && x <= 2147483647 witness 0 +constrained i64 = x: int where x >= -9223372036854775808 && x <= 9223372036854775807 witness 0 + +// --- Basic range checks --- + +// Input constraints: callee can rely on range +procedure i8InRange(b: i8) { + assert b >= -128; + assert b <= 127 +}; + +procedure i32InRange(n: i32) { + assert n >= -2147483648; + assert n <= 2147483647 +}; + +procedure u16IsUnsigned(c: u16) { + assert c >= 0; + assert c <= 65535 +}; + +// Output constraints: valid returns pass +procedure returnValidI8(): i8 { return 42 }; +procedure returnValidI32(): i32 { return 1000000 }; +procedure returnValidU16(): u16 { return 65 }; + +// Output constraints: out-of-range returns fail +procedure returnOverflowI8(): i8 { +// ^^ error: assertion does not hold + return 128 +}; + +procedure returnUnderflowI32(): i32 { +// ^^^ error: assertion does not hold + return -2147483649 +}; + +procedure returnNegativeU16(): u16 { +// ^^^ error: assertion does not hold + return -1 +}; + +// --- Arithmetic within range --- + +// Addition that stays in range +procedure safeI8Add(a: i8, b: i8) returns (r: i32) { + // i8 + i8 always fits in i32 + r := a + b; + assert r >= -256; + assert r <= 254 +}; + +// Multiplication that stays in range +procedure safeI32Mul() returns (r: i32) { + var a: i32 := 1000; + var b: i32 := 1000; + r := a * b; + assert r == 1000000 +}; + +// --- Cross-type widening --- + +// i8 widens to i32 (always safe) +procedure i8ToI32(b: i8) returns (r: i32) { + r := b +}; + +// u16 widens to i32 (always safe) +procedure u16ToI32(c: u16) returns (r: i32) { + r := c +}; + +// i32 does NOT fit in i8 (requires check) +procedure i32ToI8(n: i32) returns (r: i8) { +// ^^ error: assertion does not hold + r := n +}; + +// --- Opaque procedure contracts --- + +// Opaque procedure returning i32 — caller gets range guarantee +procedure opaqueI32(): i32; +procedure callerUsesRange() { + var x: int := opaqueI32(); + assert x >= -2147483648; + assert x <= 2147483647 +}; + +// --- Quantifiers with constrained types --- + +// All i8 values are valid i32 values +procedure allI8AreI32() { + var b: bool := forall(b: i8) => b >= -2147483648 && b <= 2147483647; + assert b +}; + +// There exists a u16 that is also a valid i8 +procedure someU16IsI8() { + var b: bool := exists(c: u16) => c <= 127; + assert b +}; +" + +/-- error: Test failed -/ +#guard_msgs(drop info, error) in +#eval testInputWithOffset "ConstrainedIntegerTypes" program 14 processLaurelFile + +end Laurel +end Strata diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_JavaMachineIntegers.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_JavaMachineIntegers.lean deleted file mode 100644 index 44b4531c9..000000000 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_JavaMachineIntegers.lean +++ /dev/null @@ -1,129 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ - -import StrataTest.Util.TestDiagnostics -import StrataTest.Languages.Laurel.TestExamples - -open StrataTest.Util - -namespace Strata -namespace Laurel - -def program := r" -// Java machine integer types as constrained types over mathematical int. -// These model the range constraints without wrapping semantics. - -constrained jbyte = x: int where x >= -128 && x <= 127 witness 0 -constrained jshort = x: int where x >= -32768 && x <= 32767 witness 0 -constrained jchar = x: int where x >= 0 && x <= 65535 witness 0 -constrained jint = x: int where x >= -2147483648 && x <= 2147483647 witness 0 -constrained jlong = x: int where x >= -9223372036854775808 && x <= 9223372036854775807 witness 0 - -// --- Basic range checks --- - -// Input constraints: callee can rely on range -procedure byteInRange(b: jbyte) { - assert b >= -128; - assert b <= 127 -}; - -procedure intInRange(n: jint) { - assert n >= -2147483648; - assert n <= 2147483647 -}; - -procedure charIsUnsigned(c: jchar) { - assert c >= 0 -}; - -// Output constraints: valid returns pass -procedure returnValidByte(): jbyte { return 42 }; -procedure returnValidInt(): jint { return 1000000 }; -procedure returnValidChar(): jchar { return 65 }; - -// Output constraints: out-of-range returns fail -procedure returnOverflowByte(): jbyte { -// ^^^^^ error: assertion does not hold - return 128 -}; - -procedure returnUnderflowInt(): jint { -// ^^^^ error: assertion does not hold - return -2147483649 -}; - -procedure returnNegativeChar(): jchar { -// ^^^^^ error: assertion does not hold - return -1 -}; - -// --- Arithmetic within range --- - -// Addition that stays in range -procedure safeByteAdd(a: jbyte, b: jbyte) returns (r: jint) { - // byte + byte always fits in int - r := a + b; - assert r >= -256; - assert r <= 254 -}; - -// Multiplication that stays in range -procedure safeIntMul() returns (r: jint) { - var a: jint := 1000; - var b: jint := 1000; - r := a * b; - assert r == 1000000 -}; - -// --- Cross-type widening --- - -// byte widens to int (always safe) -procedure byteToInt(b: jbyte) returns (r: jint) { - r := b -}; - -// char widens to int (always safe) -procedure charToInt(c: jchar) returns (r: jint) { - r := c -}; - -// int does NOT fit in byte (requires check) -procedure intToByte(n: jint) returns (r: jbyte) { -// ^^^^^ error: assertion does not hold - r := n -}; - -// --- Opaque procedure contracts --- - -// Opaque procedure returning jint — caller gets range guarantee -procedure opaqueJint(): jint; -procedure callerUsesRange() { - var x: int := opaqueJint(); - assert x >= -2147483648; - assert x <= 2147483647 -}; - -// --- Quantifiers with constrained types --- - -// All bytes are valid ints -procedure allBytesAreInts() { - var b: bool := forall(b: jbyte) => b >= -2147483648 && b <= 2147483647; - assert b -}; - -// There exists a char that is also a valid byte -procedure someCharIsByte() { - var b: bool := exists(c: jchar) => c <= 127; - assert b -}; -" - -/-- error: Test failed -/ -#guard_msgs(drop info, error) in -#eval testInputWithOffset "JavaMachineIntegers" program 14 processLaurelFile - -end Laurel -end Strata diff --git a/StrataTest/Languages/Laurel/tests/test_constrained_integers.lr.st b/StrataTest/Languages/Laurel/tests/test_constrained_integers.lr.st new file mode 100644 index 000000000..d33eefe04 --- /dev/null +++ b/StrataTest/Languages/Laurel/tests/test_constrained_integers.lr.st @@ -0,0 +1,28 @@ +constrained i8 = x: int where x >= -128 && x <= 127 witness 0 +constrained i32 = x: int where x >= -2147483648 && x <= 2147483647 witness 0 +constrained u16 = x: int where x >= 0 && x <= 65535 witness 0 + +procedure i8InRange(b: i8) { + assert b >= -128; + assert b <= 127 +}; + +procedure i32InRange(n: i32) { + assert n >= -2147483648; + assert n <= 2147483647 +}; + +procedure u16IsUnsigned(c: u16) { + assert c >= 0; + assert c <= 65535 +}; + +procedure safeI8Add(a: i8, b: i8) returns (r: i32) { + r := a + b; + assert r >= -256; + assert r <= 254 +}; + +procedure i8ToI32(b: i8) returns (r: i32) { + r := b +}; diff --git a/StrataTest/Languages/Laurel/tests/test_java_integers.lr.st b/StrataTest/Languages/Laurel/tests/test_java_integers.lr.st deleted file mode 100644 index 4edfb4cff..000000000 --- a/StrataTest/Languages/Laurel/tests/test_java_integers.lr.st +++ /dev/null @@ -1,28 +0,0 @@ -constrained jbyte = x: int where x >= -128 && x <= 127 witness 0 -constrained jint = x: int where x >= -2147483648 && x <= 2147483647 witness 0 -constrained jchar = x: int where x >= 0 && x <= 65535 witness 0 - -procedure byteInRange(b: jbyte) { - assert b >= -128; - assert b <= 127 -}; - -procedure intInRange(n: jint) { - assert n >= -2147483648; - assert n <= 2147483647 -}; - -procedure charIsUnsigned(c: jchar) { - assert c >= 0; - assert c <= 65535 -}; - -procedure safeByteAdd(a: jbyte, b: jbyte) returns (r: jint) { - r := a + b; - assert r >= -256; - assert r <= 254 -}; - -procedure byteToInt(b: jbyte) returns (r: jint) { - r := b -}; From fcc256e12d0fe3ae4b178542ff4c9173782e07a1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 28 Mar 2026 21:28:07 +0000 Subject: [PATCH 4/4] Remove constrained integers CBMC pipeline test The CBMC test runner uses symtab2gb directly without goto-cc, which doesn't handle multi-procedure programs without a main() entry point. The constrained integer types are already tested in the Lean test (T18_ConstrainedIntegerTypes.lean) via the SMT solver path. Co-authored-by: Kiro --- .../tests/test_constrained_integers.lr.st | 28 ------------------- 1 file changed, 28 deletions(-) delete mode 100644 StrataTest/Languages/Laurel/tests/test_constrained_integers.lr.st diff --git a/StrataTest/Languages/Laurel/tests/test_constrained_integers.lr.st b/StrataTest/Languages/Laurel/tests/test_constrained_integers.lr.st deleted file mode 100644 index d33eefe04..000000000 --- a/StrataTest/Languages/Laurel/tests/test_constrained_integers.lr.st +++ /dev/null @@ -1,28 +0,0 @@ -constrained i8 = x: int where x >= -128 && x <= 127 witness 0 -constrained i32 = x: int where x >= -2147483648 && x <= 2147483647 witness 0 -constrained u16 = x: int where x >= 0 && x <= 65535 witness 0 - -procedure i8InRange(b: i8) { - assert b >= -128; - assert b <= 127 -}; - -procedure i32InRange(n: i32) { - assert n >= -2147483648; - assert n <= 2147483647 -}; - -procedure u16IsUnsigned(c: u16) { - assert c >= 0; - assert c <= 65535 -}; - -procedure safeI8Add(a: i8, b: i8) returns (r: i32) { - r := a + b; - assert r >= -256; - assert r <= 254 -}; - -procedure i8ToI32(b: i8) returns (r: i32) { - r := b -};