Add Laurel tests for Java machine integers as constrained types

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

StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh

@@ -1,85 +1,72 @@
 #!/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}"
 
-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") > "$WORK/${bn}.translate.log" 2>&1; then
+    echo "SKIP: $bn (translation failed)"
+    cat "$WORK/${bn}.translate.log"
+    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: 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 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)
+
+  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 <desc>: <STATUS>
-    # 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"
+exit $((errors > 0 ? 1 : 0))