From fc44f6ffd211f97ce54e65f0a742e08d440d8a98 Mon Sep 17 00:00:00 2001 From: Zafer Esen Date: Mon, 15 Dec 2025 13:44:26 +0100 Subject: [PATCH] Support machine arithmetic types on the heap --- regression-tests/horn-contracts/Answers | 16 +++++++++++++ regression-tests/horn-contracts/runtests | 9 ++++++- .../horn-contracts/stackptr-ilp32.hcc | 12 ++++++++++ regression-tests/horn-hcc-array/Answers | 3 +++ regression-tests/horn-hcc-array/ilp32-bug-1.c | 9 +++++++ regression-tests/horn-hcc-array/runtests | 8 +++++++ .../scala/tricera/concurrency/CCReader.scala | 24 +++++++++++++------ 7 files changed, 73 insertions(+), 8 deletions(-) create mode 100644 regression-tests/horn-contracts/stackptr-ilp32.hcc create mode 100644 regression-tests/horn-hcc-array/ilp32-bug-1.c diff --git a/regression-tests/horn-contracts/Answers b/regression-tests/horn-contracts/Answers index 3679b159..5e7ba7af 100644 --- a/regression-tests/horn-contracts/Answers +++ b/regression-tests/horn-contracts/Answers @@ -245,3 +245,19 @@ Inferred ACSL annotations ================================================================================ SAFE + +stackptr-ilp32.hcc +Warning: The following clause has different terms with the same name (term: globalf1_0p:12) +main10_5(@h, globalf1_0p:12, c:9.\as[signed bv[32]]) :- c:9 >= -2147483648 & 2147483647 >= c:9 & globalf1_0p:12 >= -2147483648 & 2147483647 >= globalf1_0p:12 & @h = emptyHeap & globalf1_0p:12 = 0.\as[signed bv[32]]. + + +Inferred ACSL annotations +================================================================================ +/* contract for f1 */ +/*@ + requires \valid(p) && 2147483647 >= *p && *p >= -2147483648; + ensures \valid(p) && (*p == 0 || \old(*p) >= 2147483648 || -2147483649 >= \old(*p)); +*/ +================================================================================ + +SAFE diff --git a/regression-tests/horn-contracts/runtests b/regression-tests/horn-contracts/runtests index e8811d86..1bac88de 100755 --- a/regression-tests/horn-contracts/runtests +++ b/regression-tests/horn-contracts/runtests @@ -30,4 +30,11 @@ for name in $TESTS; do echo echo $name $LAZABS -cex -acsl -m:entryPoint "$@" $name 2>&1 | grep -v 'at ' -done \ No newline at end of file +done + +ILP32TESTS="stackptr-ilp32.hcc" +for name in $ILP32TESTS; do + echo + echo $name + $LAZABS -cex -acsl -arithMode:ilp32 "$@" $name 2>&1 | grep -v 'at ' +done diff --git a/regression-tests/horn-contracts/stackptr-ilp32.hcc b/regression-tests/horn-contracts/stackptr-ilp32.hcc new file mode 100644 index 00000000..babe83ed --- /dev/null +++ b/regression-tests/horn-contracts/stackptr-ilp32.hcc @@ -0,0 +1,12 @@ +/*@contract@*/ +static void f1(int *p) +{ + *p = 0; +} + +void main() +{ + int c; + f1(&c); + assert(c == 0); +} \ No newline at end of file diff --git a/regression-tests/horn-hcc-array/Answers b/regression-tests/horn-hcc-array/Answers index d31da2d0..2a69efe7 100644 --- a/regression-tests/horn-hcc-array/Answers +++ b/regression-tests/horn-hcc-array/Answers @@ -260,3 +260,6 @@ SAFE nondet-static-array-opt-3.c SAFE + +ilp32-bug-1.c +SAFE diff --git a/regression-tests/horn-hcc-array/ilp32-bug-1.c b/regression-tests/horn-hcc-array/ilp32-bug-1.c new file mode 100644 index 00000000..4c1dec4a --- /dev/null +++ b/regression-tests/horn-hcc-array/ilp32-bug-1.c @@ -0,0 +1,9 @@ +int i[2]; + +void f1() { + assert(i[1] == (i[1] & 0x0000FFFF) + (i[1] & 0xFFFF0000)); +} + +void main() { + f1(); +} \ No newline at end of file diff --git a/regression-tests/horn-hcc-array/runtests b/regression-tests/horn-hcc-array/runtests index 3fcac6e0..bb08237a 100755 --- a/regression-tests/horn-hcc-array/runtests +++ b/regression-tests/horn-hcc-array/runtests @@ -18,6 +18,8 @@ NONDETINITESTS="\ nondet-global-array-opt-1.c nondet-global-array-opt-2.c nondet-global-array-opt-3.c \ nondet-static-array-opt-1.c nondet-static-array-opt-2.c nondet-static-array-opt-3.c" +ILP32TESTS="ilp32-bug-1.c" + ## -heapModel:native for name in $TESTS; do @@ -46,6 +48,12 @@ for name in $NONDETINITESTS; do $LAZABS -cex -abstract:off -forceNondetInit -heapModel:native "$@" $name 2>&1 | grep -v 'at ' done +for name in $ILP32TESTS; do + echo + echo $name + $LAZABS -cex -abstract:off -forceNondetInit -heapModel:native -arithMode:ilp32 "$@" $name 2>&1 | grep -v 'at ' +done + ## -heapModel:array # for name in $TESTS; do diff --git a/src/main/scala/tricera/concurrency/CCReader.scala b/src/main/scala/tricera/concurrency/CCReader.scala index bd3bad1b..e42de671 100644 --- a/src/main/scala/tricera/concurrency/CCReader.scala +++ b/src/main/scala/tricera/concurrency/CCReader.scala @@ -623,12 +623,21 @@ class CCReader private (prog : Program, }).toList // todo: only add types that exist in the program - should also add machine arithmetic types - val predefSignatures = - List(("O_Int", HeapObj.CtorSignature(List(("getInt", HeapObj.OtherSort(Sort.Integer))), ObjSort)), - ("O_UInt", HeapObj.CtorSignature(List(("getUInt", HeapObj.OtherSort(Sort.Nat))), ObjSort)), - ("O_Addr", HeapObj.CtorSignature(List(("getAddr", HeapObj.AddrSort)), ObjSort)), - ("O_AddrRange", HeapObj.CtorSignature(List(("getAddrRange", HeapObj.AddrRangeSort)), ObjSort)) - ) + val predefSignatures = List( + ("O_Int", HeapObj.CtorSignature( + List(("getInt", HeapObj.OtherSort(CCInt.toSort))), ObjSort)), + ("O_UInt", HeapObj.CtorSignature( + List(("getUInt", HeapObj.OtherSort(CCUInt.toSort))), ObjSort)), + ("O_Addr", HeapObj.CtorSignature( + List(("getAddr", HeapObj.AddrSort)), ObjSort)), + ("O_AddrRange", HeapObj.CtorSignature( + List(("getAddrRange", HeapObj.AddrRangeSort)), ObjSort)) + ) + // Make sure that we have one object sort per sort + private val ctorObjSorts = + predefSignatures.flatMap(s => s._2.arguments.map(_._2)) + assert(ctorObjSorts.toSet.size == ctorObjSorts.size) + val wrapperSignatures : List[(String, HeapObj.CtorSignature)] = predefSignatures ++ @@ -668,7 +677,8 @@ class CCReader private (prog : Program, val structSels = heap.userHeapSelectors.slice(structCtorsOffset+structCount, structCtorsOffset+2*structCount) - val objectSorts : scala.IndexedSeq[Sort] = objectGetters.toIndexedSeq.map(f => f.resSort) + val objectSorts : scala.IndexedSeq[Sort] = + objectGetters.toIndexedSeq.map(f => f.resSort) val sortGetterMap : Map[Sort, MonoSortedIFunction] = objectSorts.zip(objectGetters).toMap val sortWrapperMap : Map[Sort, MonoSortedIFunction] =