diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml index dd128428..abbbb817 100644 --- a/.github/workflows/scala.yml +++ b/.github/workflows/scala.yml @@ -12,7 +12,12 @@ jobs: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - name: Checkout repository (with submodules) + uses: actions/checkout@v2 + with: + submodules: true + fetch-depth: 0 + - name: Set up JDK 11 uses: actions/setup-java@v2 with: @@ -20,6 +25,8 @@ jobs: distribution: 'adopt' - name: Set up sbt uses: sbt/setup-sbt@v1 + - name: Patch build.sbt files of submodules + run: ./patch-builds.sh - name: Build run: sbt nativeImage - name: Test diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000..544b5f61 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,9 @@ +[submodule "eldarica"] + path = eldarica + url = https://github.com/uuverifiers/eldarica +[submodule "horn-concurrency"] + path = horn-concurrency + url = https://github.com/uuverifiers/horn-concurrency +[submodule "princess"] + path = princess + url = https://github.com/uuverifiers/princess diff --git a/build.sbt b/build.sbt index 774b42ac..19018f5e 100644 --- a/build.sbt +++ b/build.sbt @@ -3,11 +3,13 @@ import java.nio.file.{Files, Paths} import java.nio.file.attribute.PosixFilePermissions import scala.language.postfixOps import scala.util.Try +import sbt._ +import Keys._ lazy val commonSettings = Seq( name := "TriCera", organization := "uuverifiers", - version := "0.4", + version := "0.4-DEV", homepage := Some(url("https://github.com/uuverifiers/tricera")), licenses := Seq("BSD-3-Clause" -> url("https://opensource.org/licenses/BSD-3-Clause")), description := "TriCera is a model checker for C programs.", @@ -90,32 +92,29 @@ ppWithErrorHandling := { } (compile in Compile) := ((compile in Compile) dependsOn ppWithErrorHandling).value -// Actual project -lazy val root = (project in file(".")). - aggregate(ccParser). - dependsOn(ccParser). - aggregate(acslParser). - dependsOn(acslParser). - settings(commonSettings: _*). +lazy val princess = ProjectRef(file("princess"), "root") +lazy val eldarica = ProjectRef(file("eldarica"), "root") +lazy val hornConcurrency = ProjectRef(file("horn-concurrency"), "root") -// -settings( - mainClass in Compile := Some("tricera.Main"), - // - scalacOptions in Compile ++= - List("-feature", - "-language:implicitConversions,postfixOps,reflectiveCalls"), - scalacOptions += "-opt:_", - resolvers += "uuverifiers" at "https://eldarica.org/maven/", - libraryDependencies += "uuverifiers" %% "eldarica" % "2.2.1", - libraryDependencies += "uuverifiers" %% "horn-concurrency" % "2.2.1", - libraryDependencies += "net.jcazevedo" %% "moultingyaml" % "0.4.2", - libraryDependencies += "org.scalactic" %% "scalactic" % "3.2.19", - libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.19" % "test", - excludeDependencies ++= Seq( - // exclude java-cup from transitive dependencies, ccParser includes newer version - ExclusionRule("net.sf.squirrel-sql.thirdparty-non-maven", "java-cup")), +// Actual project +lazy val root = (project in file(".")) + .settings(commonSettings) + .settings( + mainClass in Compile := Some("tricera.Main"), + scalacOptions in Compile ++= + List("-feature", "-language:implicitConversions,postfixOps,reflectiveCalls", + "-encoding", "UTF-8"), + scalacOptions += "-opt:_", + //resolvers += "uuverifiers" at "https://eldarica.org/maven/", + libraryDependencies ++= Seq( + "net.jcazevedo" %% "moultingyaml" % "0.4.2", + "org.scalactic" %% "scalactic" % "3.2.19", + "org.scalatest" %% "scalatest" % "3.2.19" % Test + ), + excludeDependencies ++= Seq( + ExclusionRule("net.sf.squirrel-sql.thirdparty-non-maven", "java-cup")), + nativeImageInstalled := false, nativeImageVersion := "21.1.0", nativeImageJvm := "graalvm-java11", @@ -130,11 +129,48 @@ settings( nativeImageAgentMerge := true ) - .enablePlugins(NativeImagePlugin) - -// project can also be built by providing dependencies under the lib directory -// and uncommenting below code to discard clashing transitive dependencies -//assemblyMergeStrategy in assembly := { -// case PathList("META-INF", xs @ _*) => MergeStrategy.discard -// case x => MergeStrategy.last -//} + .dependsOn(ccParser, acslParser, eldarica, hornConcurrency) + .aggregate(ccParser, acslParser) + .enablePlugins(NativeImagePlugin) + +// Remove java-cup-11a jars from unmanagedJars in subprojects +ccParser / Compile / unmanagedJars := +(ccParser / Compile / unmanagedJars).value.filterNot( + _.data.getName.contains("java-cup-11a")) + +lazy val settingsAlreadyOverridden = settingKey[Boolean]( + "Has overrideSettings command already run?") +settingsAlreadyOverridden := false + +commands += Command.command("overrideSettings") { state => + val extracted = Project.extract(state) + if (extracted.get(settingsAlreadyOverridden)) state + else { + Project.extract(state).appendWithSession( + Seq( + settingsAlreadyOverridden := true, + eldarica / organization := "uuverifiers-dev", + eldarica / version := "0.0.0-dev", + hornConcurrency / organization := "uuverifiers-dev", + hornConcurrency / version := "0.0.0-dev", + princess / organization := "uuverifiers-dev", + princess / version := "0.0.0-dev", + + eldarica / libraryDependencies := (eldarica / libraryDependencies).value.filterNot(_.organization.startsWith("uuverifiers")), + hornConcurrency / libraryDependencies := (hornConcurrency / libraryDependencies).value.filterNot(_.organization.startsWith("uuverifiers")), + ), + state + ) + } +} + +onLoad in Global := { + ((s: State) => "overrideSettings" :: s) compose (onLoad in Global).value +} + +assembly / assemblyMergeStrategy := { + case PathList("java_cup", "runtime", _ @ _*) => MergeStrategy.first + case PathList("META-INF", _ @ _*) => MergeStrategy.discard + case x => MergeStrategy.first +} + diff --git a/eldarica b/eldarica new file mode 160000 index 00000000..5ef4f222 --- /dev/null +++ b/eldarica @@ -0,0 +1 @@ +Subproject commit 5ef4f22231efff76d09c67c8ac082d86df062cde diff --git a/horn-concurrency b/horn-concurrency new file mode 160000 index 00000000..1755adb8 --- /dev/null +++ b/horn-concurrency @@ -0,0 +1 @@ +Subproject commit 1755adb855cac220407312584d542f5a4f063332 diff --git a/patch-builds.sh b/patch-builds.sh new file mode 100755 index 00000000..d5bf21ab --- /dev/null +++ b/patch-builds.sh @@ -0,0 +1,56 @@ +#!/usr/bin/env bash +set -e + +ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" + +echo "Patching local submodules under $ROOT_DIR ..." + +############################################ +# Patch eldarica build.sbt +############################################ +ELDARICA_BUILD="$ROOT_DIR/eldarica/build.sbt" + +if [[ -f "$ELDARICA_BUILD" ]]; then + if ! grep -q 'ProjectRef(file("../princess"), "root")' "$ELDARICA_BUILD"; then + echo " -> Patching eldarica/build.sbt" + + # Insert the line between dependsOn(...) and .settings(...) + awk ' + /dependsOn\(tplspecParser\)\./ { + print " dependsOn(ProjectRef(file(\"../princess\"), \"root\"))." + } + { print } + ' "$ELDARICA_BUILD" > "$ELDARICA_BUILD.tmp" && mv "$ELDARICA_BUILD.tmp" "$ELDARICA_BUILD" + else + echo " -> eldarica/build.sbt already patched" + fi +else + echo " !! eldarica/build.sbt not found" +fi + + +############################################ +# Patch horn-concurrency build.sbt +############################################ +HORN_BUILD="$ROOT_DIR/horn-concurrency/build.sbt" + +if [[ -f "$HORN_BUILD" ]]; then + if ! grep -q 'ProjectRef(file("../eldarica"), "root")' "$HORN_BUILD"; then + echo " -> Patching horn-concurrency/build.sbt" + + # Append after the main project definition + awk ' + /lazy val root = \(project in file\("\."\)\)\./ { + print $0 "\n dependsOn(ProjectRef(file(\"../eldarica\"), \"root\"))." + next + } + { print } + ' "$HORN_BUILD" > "$HORN_BUILD.tmp" && mv "$HORN_BUILD.tmp" "$HORN_BUILD" + else + echo " -> horn-concurrency/build.sbt already patched" + fi +else + echo " !! horn-concurrency/build.sbt not found" +fi + +echo "Done." diff --git a/princess b/princess new file mode 160000 index 00000000..d51595fb --- /dev/null +++ b/princess @@ -0,0 +1 @@ +Subproject commit d51595fb77b092cc785070163a90583670d248e3 diff --git a/regression-tests/acsl-standalone/Answers b/regression-tests/acsl-standalone/Answers index 4b26fb6f..5bf240bb 100644 --- a/regression-tests/acsl-standalone/Answers +++ b/regression-tests/acsl-standalone/Answers @@ -87,15 +87,15 @@ SAFE getptr_unsafe.c Warning: A property file exists, but properties are also specified in the command-line. Ignoring the property file. ----------------------------------------------------------------------- +---------------------------------------------------------------------------- Init: - foo1_1(emptyHeap, nullAddr, nullAddr, emptyHeap, nullAddr, nullAddr) ----------------------------------------------------------------------- + foo1_1(heap.empty, heap.null, heap.null, heap.empty, heap.null, heap.null) +---------------------------------------------------------------------------- Final: - foo1_1(emptyHeap, nullAddr, nullAddr, emptyHeap, nullAddr, nullAddr) ----------------------------------------------------------------------- + foo1_1(heap.empty, heap.null, heap.null, heap.empty, heap.null, heap.null) +---------------------------------------------------------------------------- Failed assertion: -false :- foo1_1(@h, @v_cleanup, p, @h_old, @v_cleanup_old, p_old), !is_O_Int(read(@h, p)). (line:4 col:9) (property: valid-deref) +false :- foo1_1(@h, @v_cleanup, p, @h_old, @v_cleanup_old, p_old), !is_O_Int(heap.read(@h, p)). (line:4 col:9) (property: valid-deref) UNSAFE @@ -104,18 +104,18 @@ SAFE assigns_unsafe.c -------------------------------------------------------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Init: - foo1_1(newHeap(alloc(emptyHeap, O_Int(47))), nullAddr, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(47))), nullAddr, nthAddr(1)) -------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo8_10(newHeap(alloc(emptyHeap, O_Int(42))), nullAddr, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(47))), nullAddr, nthAddr(1), 42) -------------------------------------------------------------------------------------------------------------------------------------- + foo1_1(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(47))), heap.null, heap.addr(1), heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(47))), heap.null, heap.addr(1)) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo8_10(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(42))), heap.null, heap.addr(1), heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(47))), heap.null, heap.addr(1), 42) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Final: - foo8_10(newHeap(alloc(emptyHeap, O_Int(42))), nullAddr, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(47))), nullAddr, nthAddr(1), 42) -------------------------------------------------------------------------------------------------------------------------------------- + foo8_10(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(42))), heap.null, heap.addr(1), heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(47))), heap.null, heap.addr(1), 42) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: false :- foo8_10(@h, @v_cleanup, p, @h_old, @v_cleanup_old, p_old, _res1), !(_res1 = 42 & @h = @h_old). (line:4 col:20) (property: postcondition of function foo asserted at 1:1.) @@ -126,25 +126,25 @@ SAFE maxptr_unsafe.c ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Init: - foo1_1(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nullAddr, nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nullAddr, nthAddr(1), nthAddr(2)) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo8_17(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nullAddr, nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nullAddr, nthAddr(1), nthAddr(2)) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo11_12(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nullAddr, nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nullAddr, nthAddr(1), nthAddr(2), 5) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo1_1(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(4))), O_Int(3))), heap.null, heap.addr(1), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(4))), O_Int(3))), heap.null, heap.addr(1), heap.addr(2)) +----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo8_17(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(4))), O_Int(3))), heap.null, heap.addr(1), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(4))), O_Int(3))), heap.null, heap.addr(1), heap.addr(2)) +----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo11_12(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(4))), O_Int(3))), heap.null, heap.addr(1), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(4))), O_Int(3))), heap.null, heap.addr(1), heap.addr(2), 5) +----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Final: - foo11_12(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nullAddr, nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(4))), O_Int(3))), nullAddr, nthAddr(1), nthAddr(2), 5) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo11_12(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(4))), O_Int(3))), heap.null, heap.addr(1), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(4))), O_Int(3))), heap.null, heap.addr(1), heap.addr(2), 5) +----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- foo11_12(@h, @v_cleanup, p, q, @h_old, @v_cleanup_old, p_old, q_old, _res1), !((_res1 = getInt(read(@h, p_old)) | _res1 = getInt(read(@h, q_old))) & _res1 >= getInt(read(@h, p_old)) & _res1 >= getInt(read(@h, q_old))). (line:3 col:25) (property: postcondition of function foo asserted at 1:1.) +false :- foo11_12(@h, @v_cleanup, p, q, @h_old, @v_cleanup_old, p_old, q_old, _res1), !((_res1 = getInt(heap.read(@h, p_old)) | _res1 = getInt(heap.read(@h, q_old))) & _res1 >= getInt(heap.read(@h, p_old)) & _res1 >= getInt(heap.read(@h, q_old))). (line:3 col:25) (property: postcondition of function foo asserted at 1:1.) UNSAFE @@ -153,25 +153,25 @@ SAFE old_unsafe.c ------------------------------------------------------------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ Init: - foo4_1(newHeap(alloc(emptyHeap, O_Int(45))), nullAddr, -42, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(45))), nullAddr, -42, nthAddr(1)) ------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo(newHeap(alloc(emptyHeap, O_Int(42))), nullAddr, -42, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(45))), nullAddr, -42, nthAddr(1)) ------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo10_8(newHeap(alloc(emptyHeap, O_Int(42))), nullAddr, 0, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(45))), nullAddr, -42, nthAddr(1)) ------------------------------------------------------------------------------------------------------------------------------------------- + foo4_1(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(45))), heap.null, -42, heap.addr(1), heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(45))), heap.null, -42, heap.addr(1)) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + foo(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(42))), heap.null, -42, heap.addr(1), heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(45))), heap.null, -42, heap.addr(1)) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + foo10_8(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(42))), heap.null, 0, heap.addr(1), heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(45))), heap.null, -42, heap.addr(1)) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ Final: - foo10_8(newHeap(alloc(emptyHeap, O_Int(42))), nullAddr, 0, nthAddr(1), newHeap(alloc(emptyHeap, O_Int(45))), nullAddr, -42, nthAddr(1)) ------------------------------------------------------------------------------------------------------------------------------------------- + foo10_8(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(42))), heap.null, 0, heap.addr(1), heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(45))), heap.null, -42, heap.addr(1)) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ Failed assertion: -false :- foo10_8(@h, @v_cleanup, g, p, @h_old, @v_cleanup_old, g_old, p_old), g != g_old + getInt(read(@h_old, p_old)). (line:6 col:22) (property: postcondition of function foo asserted at 4:1.) +false :- foo10_8(@h, @v_cleanup, g, p, @h_old, @v_cleanup_old, g_old, p_old), g != g_old + getInt(heap.read(@h_old, p_old)). (line:6 col:22) (property: postcondition of function foo asserted at 4:1.) UNSAFE @@ -180,25 +180,25 @@ SAFE dblptr-assigns_unsafe.c ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Init: - foo5_1(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), nullAddr, 0, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), nullAddr, 0, nthAddr(3), nthAddr(2)) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(42))), nullAddr, 0, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), nullAddr, 0, nthAddr(3), nthAddr(2)) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo14_9(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(42))), O_Addr(nthAddr(1)))), O_Int(42))), nullAddr, 42, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), nullAddr, 0, nthAddr(3), nthAddr(2)) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo5_1(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(50))), O_Addr(heap.addr(1)))), O_Int(51))), heap.null, 0, heap.addr(3), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(50))), O_Addr(heap.addr(1)))), O_Int(51))), heap.null, 0, heap.addr(3), heap.addr(2)) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(50))), O_Addr(heap.addr(1)))), O_Int(42))), heap.null, 0, heap.addr(3), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(50))), O_Addr(heap.addr(1)))), O_Int(51))), heap.null, 0, heap.addr(3), heap.addr(2)) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + foo14_9(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(42))), O_Addr(heap.addr(1)))), O_Int(42))), heap.null, 42, heap.addr(3), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(50))), O_Addr(heap.addr(1)))), O_Int(51))), heap.null, 0, heap.addr(3), heap.addr(2)) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Final: - foo14_9(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(42))), O_Addr(nthAddr(1)))), O_Int(42))), nullAddr, 42, nthAddr(3), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(50))), O_Addr(nthAddr(1)))), O_Int(51))), nullAddr, 0, nthAddr(3), nthAddr(2)) ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo14_9(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(42))), O_Addr(heap.addr(1)))), O_Int(42))), heap.null, 42, heap.addr(3), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(50))), O_Addr(heap.addr(1)))), O_Int(51))), heap.null, 0, heap.addr(3), heap.addr(2)) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- foo14_9(@h, @v_cleanup, g, p, q, @h_old, @v_cleanup_old, g_old, p_old, q_old), !(!(_p != q_old & _p != p_old) | read(@h, _p) = read(@h_old, _p)). (line:6 col:4) (property: postcondition of function foo asserted at 5:1.) +false :- foo14_9(@h, @v_cleanup, g, p, q, @h_old, @v_cleanup_old, g_old, p_old, q_old), !(!(_p != q_old & _p != p_old) | heap.read(@h, _p) = heap.read(@h_old, _p)). (line:6 col:4) (property: postcondition of function foo asserted at 5:1.) UNSAFE @@ -207,29 +207,29 @@ SAFE swap_unsafe.c ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ Init: - foo3_1(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nullAddr, nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nullAddr, nthAddr(1), nthAddr(2)) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo10_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nullAddr, nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nullAddr, nthAddr(1), nthAddr(2), 7) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo(newHeap(alloc(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 2)), O_Int(0))), nullAddr, nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nullAddr, nthAddr(1), nthAddr(2), 7) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - foo12_8(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(9))), O_Int(7))), O_Int(0))), nullAddr, nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nullAddr, nthAddr(1), nthAddr(2)) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo3_1(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(7))), O_Int(9))), O_Int(0))), heap.null, heap.addr(1), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(7))), O_Int(9))), O_Int(0))), heap.null, heap.addr(1), heap.addr(2)) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + foo10_3(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(7))), O_Int(9))), O_Int(0))), heap.null, heap.addr(1), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(7))), O_Int(9))), O_Int(0))), heap.null, heap.addr(1), heap.addr(2), 7) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + foo(heap.heapAddrPair_1(heap.alloc(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 2)), O_Int(0))), heap.null, heap.addr(1), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(7))), O_Int(9))), O_Int(0))), heap.null, heap.addr(1), heap.addr(2), 7) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ + | + | + V + foo12_8(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(9))), O_Int(7))), O_Int(0))), heap.null, heap.addr(1), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(7))), O_Int(9))), O_Int(0))), heap.null, heap.addr(1), heap.addr(2)) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ Final: - foo12_8(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(9))), O_Int(7))), O_Int(0))), nullAddr, nthAddr(1), nthAddr(2), newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Int(7))), O_Int(9))), O_Int(0))), nullAddr, nthAddr(1), nthAddr(2)) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + foo12_8(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(9))), O_Int(7))), O_Int(0))), heap.null, heap.addr(1), heap.addr(2), heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(7))), O_Int(9))), O_Int(0))), heap.null, heap.addr(1), heap.addr(2)) +------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ Failed assertion: -false :- foo12_8(@h, @v_cleanup, a, b, @h_old, @v_cleanup_old, a_old, b_old), !(getInt(read(@h, a_old)) = getInt(read(@h_old, b_old)) & getInt(read(@h, b_old)) = getInt(read(@h, a_old)) & (!(_p != a_old & _p != b_old) | read(@h, _p) = read(@h_old, _p))). (line:6 col:19) (property: postcondition of function foo asserted at 3:1.) +false :- foo12_8(@h, @v_cleanup, a, b, @h_old, @v_cleanup_old, a_old, b_old), !(getInt(heap.read(@h, a_old)) = getInt(heap.read(@h_old, b_old)) & getInt(heap.read(@h, b_old)) = getInt(heap.read(@h, a_old)) & (!(_p != a_old & _p != b_old) | heap.read(@h, _p) = heap.read(@h_old, _p))). (line:6 col:19) (property: postcondition of function foo asserted at 3:1.) UNSAFE diff --git a/regression-tests/horn-contracts/Answers b/regression-tests/horn-contracts/Answers index 5e7ba7af..41b930f6 100644 --- a/regression-tests/horn-contracts/Answers +++ b/regression-tests/horn-contracts/Answers @@ -158,8 +158,6 @@ SAFE stackptr-multi-arg.hcc Warning: no definition of function "non_det_int" available -Warning: Timeout while verifying clause: -inv_main_3(@h_post, savedglobalmod_0_1t2_0_1:36, savedglobalmod_0_1t1_0_1:35, init1:16, init2:17, globalmod_0_1t1_post, globalmod_0_1t2_post) :- inv_main39_0(@h, globalmod_0_1t2:30, globalmod_0_1t1:31, init1:16, init2:17, s1:22, s2:23, t1:33, t2:33, savedglobalmod_0_1t1_0_1:35, savedglobalmod_0_1t2_0_1:36), globalmod_0_1_post(@h, globalmod_0_1t2:30, globalmod_0_1t1:31, @h_post, globalmod_0_1t2_post, globalmod_0_1t1_post). Inferred ACSL annotations ================================================================================ @@ -193,23 +191,23 @@ SAFE stackptr-recursion.hcc ---------------------------------- +---------------------------------- Init: - main25_5(emptyHeap, 0, 0) ---------------------------------- - | - | - V - main35_0(emptyHeap, 0, 0, 2, 0) ---------------------------------- - | - | - V - main(emptyHeap, 0, 1) ---------------------------------- + main25_5(heap.empty, 0, 0) +---------------------------------- + | + | + V + main35_0(heap.empty, 0, 0, 2, 0) +---------------------------------- + | + | + V + main(heap.empty, 0, 1) +---------------------------------- Final: - main(emptyHeap, 0, 1) ---------------------------------- + main(heap.empty, 0, 1) +---------------------------------- Failed assertion: false :- main(@h, globalincr_0t:29, s:24), s:24 != 5. (line:26 col:5) (property: user-assertion) @@ -248,7 +246,7 @@ 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]]. +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 = heap.empty & globalf1_0p:12 = 0.\as[signed bv[32]]. Inferred ACSL annotations diff --git a/regression-tests/horn-hcc-array/Answers b/regression-tests/horn-hcc-array/Answers index 2a69efe7..21cec14e 100644 --- a/regression-tests/horn-hcc-array/Answers +++ b/regression-tests/horn-hcc-array/Answers @@ -2,68 +2,68 @@ out-of-bounds-line1.c Warning: no definition of function "nondet" available -------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------------- Init: - main9_3(emptyHeap, nullAddr, AddrRange(nullAddr, 0)) -------------------------------------------------------------------------------------- - | - | - V - main_2(newHeap(alloc(emptyHeap, O_Int(10))), nullAddr, AddrRange(nthAddr(1), 1), 1) -------------------------------------------------------------------------------------- + main9_3(heap.empty, heap.null, AddrRange(heap.null, 0)) +---------------------------------------------------------------------------------------------------------- + | + | + V + main_2(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(10))), heap.null, AddrRange(heap.addr(1), 1), 1) +---------------------------------------------------------------------------------------------------------- Final: - main_2(newHeap(alloc(emptyHeap, O_Int(10))), nullAddr, AddrRange(nthAddr(1), 1), 1) -------------------------------------------------------------------------------------- + main_2(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(10))), heap.null, AddrRange(heap.addr(1), 1), 1) +---------------------------------------------------------------------------------------------------------- Failed assertion: -false :- main_2(@h, @v_cleanup, a:6, n:9), !is_O_Int(read(@h, AddrRangeNth(a:6, n:9))). (line:6 col:5) (property: valid-deref) +false :- main_2(@h, @v_cleanup, a:6, n:9), !is_O_Int(heap.read(@h, heap.rangeNth(a:6, n:9))). (line:6 col:5) (property: valid-deref) UNSAFE out-of-bounds-line2.c ---------------------------------------------------------------------------------------------------- +-------------------------------------------------------------------------------------------------------------------- Init: - main7_3_1(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), nullAddr, AddrRange(nthAddr(1), 42)) ---------------------------------------------------------------------------------------------------- + main7_3_1(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(0), 42)), heap.null, AddrRange(heap.addr(1), 42)) +-------------------------------------------------------------------------------------------------------------------- Final: - main7_3_1(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), nullAddr, AddrRange(nthAddr(1), 42)) ---------------------------------------------------------------------------------------------------- + main7_3_1(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(0), 42)), heap.null, AddrRange(heap.addr(1), 42)) +-------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- main7_3_1(@h, @v_cleanup, a:4), !is_O_Int(read(@h, AddrRangeNth(a:4, 42))). (line:4 col:5) (property: valid-deref) +false :- main7_3_1(@h, @v_cleanup, a:4), !is_O_Int(heap.read(@h, heap.rangeNth(a:4, 42))). (line:4 col:5) (property: valid-deref) UNSAFE out-of-bounds-line3.c Warning: no definition of function "nondet" available -------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------------- Init: - main9_3(emptyHeap, nullAddr, AddrRange(nullAddr, 0)) -------------------------------------------------------------------------------------- - | - | - V - main_2(newHeap(alloc(emptyHeap, O_Int(10))), nullAddr, AddrRange(nthAddr(1), 1), 1) -------------------------------------------------------------------------------------- + main9_3(heap.empty, heap.null, AddrRange(heap.null, 0)) +---------------------------------------------------------------------------------------------------------- + | + | + V + main_2(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(10))), heap.null, AddrRange(heap.addr(1), 1), 1) +---------------------------------------------------------------------------------------------------------- Final: - main_2(newHeap(alloc(emptyHeap, O_Int(10))), nullAddr, AddrRange(nthAddr(1), 1), 1) -------------------------------------------------------------------------------------- + main_2(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(10))), heap.null, AddrRange(heap.addr(1), 1), 1) +---------------------------------------------------------------------------------------------------------- Failed assertion: -false :- main_2(@h, @v_cleanup, a:6, n:9), !is_O_Int(read(@h, AddrRangeNth(a:6, n:9))). (line:6 col:5) (property: valid-deref) +false :- main_2(@h, @v_cleanup, a:6, n:9), !is_O_Int(heap.read(@h, heap.rangeNth(a:6, n:9))). (line:6 col:5) (property: valid-deref) UNSAFE out-of-bounds-line4.c -------------------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------------------------------------ Init: - main7_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), nullAddr, AddrRange(nthAddr(1), 42)) -------------------------------------------------------------------------------------------------- + main7_3(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(0), 42)), heap.null, AddrRange(heap.addr(1), 42)) +------------------------------------------------------------------------------------------------------------------ Final: - main7_3(newBatchHeap(batchAlloc(emptyHeap, O_Int(0), 42)), nullAddr, AddrRange(nthAddr(1), 42)) -------------------------------------------------------------------------------------------------- + main7_3(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(0), 42)), heap.null, AddrRange(heap.addr(1), 42)) +------------------------------------------------------------------------------------------------------------------ Failed assertion: -false :- main7_3(@h, @v_cleanup, a:4), !is_O_Int(read(@h, AddrRangeNth(a:4, -1*1))). (line:4 col:5) (property: valid-deref) +false :- main7_3(@h, @v_cleanup, a:4), !is_O_Int(heap.read(@h, heap.rangeNth(a:4, -1*1))). (line:4 col:5) (property: valid-deref) UNSAFE @@ -137,15 +137,15 @@ UNKNOWN (Unsupported C fragment. Pointer arithmetic is currently not supported.) global-struct-array-1.c ------------------------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------------------------------------------------------------- Init: - main8_3(newHeap(alloc(newHeap(alloc(emptyHeap, O_S(S(10)))), O_S(S(20)))), AddrRange(nthAddr(1), 2)) ------------------------------------------------------------------------------------------------------- + main8_3(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_S(S(10)))), O_S(S(20)))), AddrRange(heap.addr(1), 2)) +------------------------------------------------------------------------------------------------------------------------------------------- Final: - main8_3(newHeap(alloc(newHeap(alloc(emptyHeap, O_S(S(10)))), O_S(S(20)))), AddrRange(nthAddr(1), 2)) ------------------------------------------------------------------------------------------------------- + main8_3(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_S(S(10)))), O_S(S(20)))), AddrRange(heap.addr(1), 2)) +------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- main8_3(@h, sArr:5), S::f(getS(read(@h, AddrRangeNth(sArr:5, 0)))) != 0. (line:8 col:3) (property: user-assertion) +false :- main8_3(@h, sArr:5), S::f(getS(heap.read(@h, heap.rangeNth(sArr:5, 0)))) != 0. (line:8 col:3) (property: user-assertion) UNSAFE @@ -154,15 +154,15 @@ SAFE nondet-global-array-explicit-1.c -------------------------------------------------------------------------------------- +----------------------------------------------------------------------------------------------------- Init: - main5_5(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 5)), AddrRange(nthAddr(1), 5)) -------------------------------------------------------------------------------------- + main5_5(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 5)), AddrRange(heap.addr(1), 5)) +----------------------------------------------------------------------------------------------------- Final: - main5_5(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 5)), AddrRange(nthAddr(1), 5)) -------------------------------------------------------------------------------------- + main5_5(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 5)), AddrRange(heap.addr(1), 5)) +----------------------------------------------------------------------------------------------------- Failed assertion: -false :- main5_5(@h, a:1), getInt(read(@h, AddrRangeNth(a:1, 0))) != 0. (line:5 col:5) (property: user-assertion) +false :- main5_5(@h, a:1), getInt(heap.read(@h, heap.rangeNth(a:1, 0))) != 0. (line:5 col:5) (property: user-assertion) UNSAFE @@ -174,20 +174,20 @@ SAFE nondet-static-array-explicit-1.c ---------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------------------------- Init: - main3_5(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 5)), AddrRange(nthAddr(1), 5)) ---------------------------------------------------------------------------------------- - | - | - V - main3_5_1(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 5)), AddrRange(nthAddr(1), 5)) ---------------------------------------------------------------------------------------- + main3_5(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 5)), AddrRange(heap.addr(1), 5)) +------------------------------------------------------------------------------------------------------- + | + | + V + main3_5_1(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 5)), AddrRange(heap.addr(1), 5)) +------------------------------------------------------------------------------------------------------- Final: - main3_5_1(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 5)), AddrRange(nthAddr(1), 5)) ---------------------------------------------------------------------------------------- + main3_5_1(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 5)), AddrRange(heap.addr(1), 5)) +------------------------------------------------------------------------------------------------------- Failed assertion: -false :- main3_5_1(@h, a:3), getInt(read(@h, AddrRangeNth(a:3, 0))) != 0. (line:6 col:5) (property: user-assertion) +false :- main3_5_1(@h, a:3), getInt(heap.read(@h, heap.rangeNth(a:3, 0))) != 0. (line:6 col:5) (property: user-assertion) UNSAFE @@ -218,15 +218,15 @@ UNKNOWN (Unsupported C fragment. Pointer arithmetic is currently not supported.) nondet-global-array-opt-1.c -------------------------------------------------------------------------------------- +----------------------------------------------------------------------------------------------------- Init: - main7_5(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 5)), AddrRange(nthAddr(1), 5)) -------------------------------------------------------------------------------------- + main7_5(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 5)), AddrRange(heap.addr(1), 5)) +----------------------------------------------------------------------------------------------------- Final: - main7_5(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 5)), AddrRange(nthAddr(1), 5)) -------------------------------------------------------------------------------------- + main7_5(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 5)), AddrRange(heap.addr(1), 5)) +----------------------------------------------------------------------------------------------------- Failed assertion: -false :- main7_5(@h, a:3), getInt(read(@h, AddrRangeNth(a:3, 1))) != 0. (line:7 col:5) (property: user-assertion) +false :- main7_5(@h, a:3), getInt(heap.read(@h, heap.rangeNth(a:3, 1))) != 0. (line:7 col:5) (property: user-assertion) UNSAFE @@ -238,20 +238,20 @@ SAFE nondet-static-array-opt-1.c ---------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------------------------- Init: - main3_5(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 5)), AddrRange(nthAddr(1), 5)) ---------------------------------------------------------------------------------------- - | - | - V - main3_5_1(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 5)), AddrRange(nthAddr(1), 5)) ---------------------------------------------------------------------------------------- + main3_5(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 5)), AddrRange(heap.addr(1), 5)) +------------------------------------------------------------------------------------------------------- + | + | + V + main3_5_1(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 5)), AddrRange(heap.addr(1), 5)) +------------------------------------------------------------------------------------------------------- Final: - main3_5_1(newBatchHeap(batchAlloc(emptyHeap, O_Int(9), 5)), AddrRange(nthAddr(1), 5)) ---------------------------------------------------------------------------------------- + main3_5_1(heap.heapRangePair_1(heap.allocRange(heap.empty, O_Int(9), 5)), AddrRange(heap.addr(1), 5)) +------------------------------------------------------------------------------------------------------- Failed assertion: -false :- main3_5_1(@h, a:3), getInt(read(@h, AddrRangeNth(a:3, 1))) != 0. (line:6 col:5) (property: user-assertion) +false :- main3_5_1(@h, a:3), getInt(heap.read(@h, heap.rangeNth(a:3, 1))) != 0. (line:6 col:5) (property: user-assertion) UNSAFE diff --git a/regression-tests/horn-hcc-enum/Answers b/regression-tests/horn-hcc-enum/Answers index 2b569f19..bc70a465 100644 --- a/regression-tests/horn-hcc-enum/Answers +++ b/regression-tests/horn-hcc-enum/Answers @@ -60,6 +60,4 @@ SAFE enum-typedef-pointer2.hcc Warning: no definition of function "nondet" available -Warning: Timeout while verifying clause: -inv_main_3(Pair(Pair::x(p:19), Pair::x(p:19)), 0) :- inv_main19_3_1(p:19), __eval16:16 != 0. SAFE diff --git a/regression-tests/horn-hcc-heap/Answers b/regression-tests/horn-hcc-heap/Answers index 70d46511..b7837336 100644 --- a/regression-tests/horn-hcc-heap/Answers +++ b/regression-tests/horn-hcc-heap/Answers @@ -4,18 +4,18 @@ SAFE list-001-fail.c ---------------------------------------------------------------------- +----------------------------------------------------------------------------------------- Init: - main11_3(emptyHeap) ---------------------------------------------------------------------- - | - | - V - main12_3(newHeap(alloc(emptyHeap, O_node(node(0)))), nthAddr(1), 0) ---------------------------------------------------------------------- + main11_3(heap.empty) +----------------------------------------------------------------------------------------- + | + | + V + main12_3(heap.heapAddrPair_1(heap.alloc(heap.empty, O_node(node(0)))), heap.addr(1), 0) +----------------------------------------------------------------------------------------- Final: - main12_3(newHeap(alloc(emptyHeap, O_node(node(0)))), nthAddr(1), 0) ---------------------------------------------------------------------- + main12_3(heap.heapAddrPair_1(heap.alloc(heap.empty, O_node(node(0)))), heap.addr(1), 0) +----------------------------------------------------------------------------------------- Failed assertion: false :- main12_3(@h, list:11, y:12), y:12 = 0. (line:13 col:3) (property: user-assertion) @@ -24,18 +24,18 @@ UNSAFE list-002-fail.c Warning: no definition of function "nondet_bool" available ---------------------------------------------------------------------------------------------- +--------------------------------------------------------------------------------------------------------------------- Init: - main14_3(emptyHeap) ---------------------------------------------------------------------------------------------- - | - | - V - main_4(newHeap(alloc(emptyHeap, O_node(node(nullAddr, nullAddr)))), nthAddr(1), nthAddr(1)) ---------------------------------------------------------------------------------------------- + main14_3(heap.empty) +--------------------------------------------------------------------------------------------------------------------- + | + | + V + main_4(heap.heapAddrPair_1(heap.alloc(heap.empty, O_node(node(heap.null, heap.null)))), heap.addr(1), heap.addr(1)) +--------------------------------------------------------------------------------------------------------------------- Final: - main_4(newHeap(alloc(emptyHeap, O_node(node(nullAddr, nullAddr)))), nthAddr(1), nthAddr(1)) ---------------------------------------------------------------------------------------------- + main_4(heap.heapAddrPair_1(heap.alloc(heap.empty, O_node(node(heap.null, heap.null)))), heap.addr(1), heap.addr(1)) +--------------------------------------------------------------------------------------------------------------------- Failed assertion: false :- main_4(@h, list:14, tail:17), list:14 = tail:17. (line:29 col:3) (property: user-assertion) @@ -49,20 +49,20 @@ SAFE mutually-referential-structs-unsafe.c -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Init: - main14_3(emptyHeap) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - main_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_parent(parent(nthAddr(2), nthAddr(3))))), O_child(child(nthAddr(1))))), O_child(child(nullAddr)))), nthAddr(1)) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + main14_3(heap.empty) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + main_3(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_parent(parent(heap.addr(2), heap.addr(3))))), O_child(child(heap.addr(1))))), O_child(child(heap.null)))), heap.addr(1)) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Final: - main_3(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_parent(parent(nthAddr(2), nthAddr(3))))), O_child(child(nthAddr(1))))), O_child(child(nullAddr)))), nthAddr(1)) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + main_3(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_parent(parent(heap.addr(2), heap.addr(3))))), O_child(child(heap.addr(1))))), O_child(child(heap.null)))), heap.addr(1)) +-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- main_3(@h, list:14), child::p(getchild(read(@h, parent::child1(getparent(read(@h, list:14)))))) != child::p(getchild(read(@h, parent::child2(getparent(read(@h, list:14)))))). (line:20 col:3) (property: user-assertion) +false :- main_3(@h, list:14), child::p(getchild(heap.read(@h, parent::child1(getparent(heap.read(@h, list:14)))))) != child::p(getchild(heap.read(@h, parent::child2(getparent(heap.read(@h, list:14)))))). (line:20 col:3) (property: user-assertion) UNSAFE @@ -95,20 +95,20 @@ SAFE typecastUnsafe-001.c --------------------------------------------------------------------------------- +------------------------------------------------------------------------------------------------------- Init: - main6_3(emptyHeap, nullAddr) --------------------------------------------------------------------------------- - | - | - V - main7_3(newHeap(alloc(emptyHeap, O_Int(0))), nullAddr, nthAddr(1), nthAddr(1)) --------------------------------------------------------------------------------- + main6_3(heap.empty, heap.null) +------------------------------------------------------------------------------------------------------- + | + | + V + main7_3(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(0))), heap.null, heap.addr(1), heap.addr(1)) +------------------------------------------------------------------------------------------------------- Final: - main7_3(newHeap(alloc(emptyHeap, O_Int(0))), nullAddr, nthAddr(1), nthAddr(1)) --------------------------------------------------------------------------------- + main7_3(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(0))), heap.null, heap.addr(1), heap.addr(1)) +------------------------------------------------------------------------------------------------------- Failed assertion: -false :- main7_3(@h, @v_cleanup, x:6, y:7), !is_O_S(read(@h, y:7)). (line:7 col:12) (property: valid-deref) +false :- main7_3(@h, @v_cleanup, x:6, y:7), !is_O_S(heap.read(@h, y:7)). (line:7 col:12) (property: valid-deref) UNSAFE @@ -145,20 +145,20 @@ SAFE unsafe-access-001.c ------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------- Init: - main2_3(emptyHeap, nullAddr) ------------------------------------------------------------------------------- - | - | - V - main3_3(newHeap(alloc(emptyHeap, O_Int(0))), nullAddr, nthAddr(1), nullAddr) ------------------------------------------------------------------------------- + main2_3(heap.empty, heap.null) +---------------------------------------------------------------------------------------------------- + | + | + V + main3_3(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(0))), heap.null, heap.addr(1), heap.null) +---------------------------------------------------------------------------------------------------- Final: - main3_3(newHeap(alloc(emptyHeap, O_Int(0))), nullAddr, nthAddr(1), nullAddr) ------------------------------------------------------------------------------- + main3_3(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(0))), heap.null, heap.addr(1), heap.null) +---------------------------------------------------------------------------------------------------- Failed assertion: -false :- main3_3(@h, @v_cleanup, x:2, y:3), !is_O_Addr(read(@h, y:3)). (line:3 col:7) (property: valid-deref) +false :- main3_3(@h, @v_cleanup, x:2, y:3), !is_O_Addr(heap.read(@h, y:3)). (line:3 col:7) (property: valid-deref) UNSAFE @@ -170,50 +170,50 @@ UNKNOWN (Unsupported C fragment. 6:8 Only limited support for stack pointers) free-1-unsafe.c ----------------------------------------------------------------------- +------------------------------------------------------------------------------------------- Init: - main2_3(emptyHeap, nullAddr) ----------------------------------------------------------------------- - | - | - V - main2_3_1(newHeap(alloc(emptyHeap, O_Int(9))), nullAddr, nthAddr(1)) ----------------------------------------------------------------------- - | - | - V - main(newHeap(alloc(emptyHeap, defObj)), nullAddr, nthAddr(1)) ----------------------------------------------------------------------- + main2_3(heap.empty, heap.null) +------------------------------------------------------------------------------------------- + | + | + V + main2_3_1(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(9))), heap.null, heap.addr(1)) +------------------------------------------------------------------------------------------- + | + | + V + main(heap.heapAddrPair_1(heap.alloc(heap.empty, defObj)), heap.null, heap.addr(1)) +------------------------------------------------------------------------------------------- Final: - main(newHeap(alloc(emptyHeap, defObj)), nullAddr, nthAddr(1)) ----------------------------------------------------------------------- + main(heap.heapAddrPair_1(heap.alloc(heap.empty, defObj)), heap.null, heap.addr(1)) +------------------------------------------------------------------------------------------- Failed assertion: -false :- main(@h, @v_cleanup, a:2), !is_O_Int(read(@h, a:2)). (line:2 col:7) (property: valid-deref) +false :- main(@h, @v_cleanup, a:2), !is_O_Int(heap.read(@h, a:2)). (line:2 col:7) (property: valid-deref) UNSAFE free-2-nondet-unsafe.c Warning: no definition of function "nondet" available ----------------------------------------------------------------------- +------------------------------------------------------------------------------------------- Init: - main4_3(emptyHeap, nullAddr) ----------------------------------------------------------------------- - | - | - V - main5_6_2(newHeap(alloc(emptyHeap, O_Int(9))), nullAddr, nthAddr(1)) ----------------------------------------------------------------------- - | - | - V - main(newHeap(alloc(emptyHeap, defObj)), nullAddr, nthAddr(1)) ----------------------------------------------------------------------- + main4_3(heap.empty, heap.null) +------------------------------------------------------------------------------------------- + | + | + V + main5_6_2(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(9))), heap.null, heap.addr(1)) +------------------------------------------------------------------------------------------- + | + | + V + main(heap.heapAddrPair_1(heap.alloc(heap.empty, defObj)), heap.null, heap.addr(1)) +------------------------------------------------------------------------------------------- Final: - main(newHeap(alloc(emptyHeap, defObj)), nullAddr, nthAddr(1)) ----------------------------------------------------------------------- + main(heap.heapAddrPair_1(heap.alloc(heap.empty, defObj)), heap.null, heap.addr(1)) +------------------------------------------------------------------------------------------- Failed assertion: -false :- main(@h, @v_cleanup, a:4), !is_O_Int(read(@h, a:4)). (line:4 col:7) (property: valid-deref) +false :- main(@h, @v_cleanup, a:4), !is_O_Int(heap.read(@h, a:4)). (line:4 col:7) (property: valid-deref) UNSAFE @@ -222,25 +222,25 @@ SAFE free-4-unsafe.c ------------------------------------------------------------------------------- +----------------------------------------------------------------------------------------------------- Init: - main4_3(emptyHeap, nullAddr) ------------------------------------------------------------------------------- - | - | - V - main4_3_1(newHeap(alloc(emptyHeap, O_Int(9))), nullAddr, nthAddr(1)) ------------------------------------------------------------------------------- - | - | - V - main6_3(newHeap(alloc(emptyHeap, defObj)), nullAddr, nthAddr(1), nthAddr(1)) ------------------------------------------------------------------------------- + main4_3(heap.empty, heap.null) +----------------------------------------------------------------------------------------------------- + | + | + V + main4_3_1(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Int(9))), heap.null, heap.addr(1)) +----------------------------------------------------------------------------------------------------- + | + | + V + main6_3(heap.heapAddrPair_1(heap.alloc(heap.empty, defObj)), heap.null, heap.addr(1), heap.addr(1)) +----------------------------------------------------------------------------------------------------- Final: - main6_3(newHeap(alloc(emptyHeap, defObj)), nullAddr, nthAddr(1), nthAddr(1)) ------------------------------------------------------------------------------- + main6_3(heap.heapAddrPair_1(heap.alloc(heap.empty, defObj)), heap.null, heap.addr(1), heap.addr(1)) +----------------------------------------------------------------------------------------------------- Failed assertion: -false :- main6_3(@h, @v_cleanup, a:4, b:6), !is_O_Int(read(@h, b:6)). (line:6 col:7) (property: valid-deref) +false :- main6_3(@h, @v_cleanup, a:4, b:6), !is_O_Int(heap.read(@h, b:6)). (line:6 col:7) (property: valid-deref) UNSAFE @@ -255,20 +255,20 @@ SAFE struct-chained-ptr-field-1-unsafe.c ------------------------------------------------------------------------------------------------------------------------ +--------------------------------------------------------------------------------------------------------------------------------------------------------------- Init: - main9_3(emptyHeap) ------------------------------------------------------------------------------------------------------------------------ - | - | - V - main_4(newHeap(alloc(newHeap(alloc(emptyHeap, O_Node(Node(nthAddr(2), 3)))), O_Node(Node(nullAddr, 0)))), nthAddr(1)) ------------------------------------------------------------------------------------------------------------------------ + main9_3(heap.empty) +--------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + main_4(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Node(Node(heap.addr(2), 3)))), O_Node(Node(heap.null, 0)))), heap.addr(1)) +--------------------------------------------------------------------------------------------------------------------------------------------------------------- Final: - main_4(newHeap(alloc(newHeap(alloc(emptyHeap, O_Node(Node(nthAddr(2), 3)))), O_Node(Node(nullAddr, 0)))), nthAddr(1)) ------------------------------------------------------------------------------------------------------------------------ + main_4(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Node(Node(heap.addr(2), 3)))), O_Node(Node(heap.null, 0)))), heap.addr(1)) +--------------------------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: -false :- main_4(@h, head:9), Node::data(getNode(read(@h, head:9))) != 0. (line:13 col:3) (property: user-assertion) +false :- main_4(@h, head:9), Node::data(getNode(heap.read(@h, head:9))) != 0. (line:13 col:3) (property: user-assertion) UNSAFE diff --git a/regression-tests/interpreted-predicates/simple-loop-invariant-false.c b/regression-tests/interpreted-predicates/simple-loop-invariant-false.c index 840bbae6..4d41aa9e 100644 --- a/regression-tests/interpreted-predicates/simple-loop-invariant-false.c +++ b/regression-tests/interpreted-predicates/simple-loop-invariant-false.c @@ -1,6 +1,6 @@ /*$ P(int x, int i, int n) { - x == i*n && i <= n //0 <= i not needed + x == i*n && i <= n && 0 <= i } $*/ @@ -10,13 +10,31 @@ void main() { int x = 0; int i = 0; assert(P(x, i, n)); - while (i < n) { - assume(P(x, i, n)); // does not work without this assumption + + int b = _; + if(b) { + x = _; i = _; n = _; + assume(i < n); + assume(P(x, i, n)); x += n; i++; assert(P(x, i, n)); + assume(0); + } else { + x = _; i = _; n = _; + assume(i >= n); + assume(P(x, i, n)); } - assume(P(x, i, n)); + + // while (i < n) { + // x = _; i = _; n = _; + // assume(P(x, i, n)); + // x += n; + // i++; + // assert(P(x, i, n)); + // } + // x = _; i = _; n = _; + // assume(P(x, i, n)); assert(x != n*n); diff --git a/regression-tests/interpreted-predicates/simple-loop-invariant-true.c b/regression-tests/interpreted-predicates/simple-loop-invariant-true.c index fcf75801..235ad5f6 100644 --- a/regression-tests/interpreted-predicates/simple-loop-invariant-true.c +++ b/regression-tests/interpreted-predicates/simple-loop-invariant-true.c @@ -1,6 +1,6 @@ /*$ P(int x, int i, int n) { - x == i*n && i <= n //0 <= i not needed + x == i*n && i <= n && 0 <= i } $*/ @@ -10,13 +10,31 @@ void main() { int x = 0; int i = 0; assert(P(x, i, n)); - while (i < n) { - assume(P(x, i, n)); // does not work without this assumption + + int b = _; + if(b) { + x = _; i = _; n = _; + assume(i < n); + assume(P(x, i, n)); x += n; i++; assert(P(x, i, n)); + assume(0); + } else { + x = _; i = _; n = _; + assume(i >= n); + assume(P(x, i, n)); } - assume(P(x, i, n)); + + // while (i < n) { + // x = _; i = _; n = _; + // assume(P(x, i, n)); + // x += n; + // i++; + // assert(P(x, i, n)); + // } + // x = _; i = _; n = _; + // assume(P(x, i, n)); assert(x == n*n); diff --git a/regression-tests/math-arrays/Answers b/regression-tests/math-arrays/Answers index 44fc5ef9..2d60b88a 100644 --- a/regression-tests/math-arrays/Answers +++ b/regression-tests/math-arrays/Answers @@ -4,7 +4,7 @@ simple-math-array-1.hcc Solution (Prolog) ================================================================================ main10_7_3(a:4, n:5, i:6) :- n:5 = 3 & 2 >= i:6 & i:6 >= 0 & ((i:6 = 2 & select(a:4, 2) = 2) | (i:6 >= 1 & select(a:4, 1 + i:6) - i:6 = 1 & select(a:4, i:6) = i:6) | (select(a:4, 2 + i:6) - i:6 = 2 & select(a:4, 1 + i:6) - i:6 = 1 & select(a:4, i:6) = i:6)). -main7_3(a:4, n:5, i:6) :- i:6 = 0 & n:5 = 3. +main7_3(a:4, n:5, i:6) :- n:5 = 3 & i:6 = 0. main7_7(a:4, n:5, i:6) :- n:5 = 3 & 3 >= i:6 & i:6 >= 0 & (0 >= i:6 | (i:6 = 1 & select(a:4, 0) = 0) | (select(a:4, 1) = 1 & select(a:4, 0) = 0 & (i:6 != 3 | select(a:4, 2) = 2))). ================================================================================ @@ -15,8 +15,8 @@ struct-array.hcc Solution (Prolog) ================================================================================ main10_5(arr:7, old_arr:8). -main_2(arr:7, old_arr:8) :- A::a(select(old_arr:8, 2)) >= 10 & store(old_arr:8, 2, A(2*A::a(select(old_arr:8, 2)))) = arr:7. -main_3(arr:7, old_arr:8) :- A::a(select(old_arr:8, 2)) >= 10 & store(old_arr:8, 2, A(2*A::a(select(old_arr:8, 2)))) = arr:7. +main_2(arr:7, old_arr:8) :- select(old_arr:8, 1) = select(arr:7, 1) & A::a(select(arr:7, 2)) = 2*A::a(select(old_arr:8, 2)). +main_3(arr:7, old_arr:8) :- select(old_arr:8, 1) = select(arr:7, 1). ================================================================================ SAFE diff --git a/regression-tests/runalldirs b/regression-tests/runalldirs index d1f5ea74..b91f8d08 100755 --- a/regression-tests/runalldirs +++ b/regression-tests/runalldirs @@ -29,7 +29,7 @@ run_test ./rundir horn-hcc-2 "" -assert -dev -t:60 run_test ./rundir horn-hcc-pointer "" -assert -dev -t:60 run_test ./rundir horn-hcc-struct "" -assert -dev -t:60 run_test ./rundir horn-hcc-enum "" -assert -dev -t:60 -run_test ./rundir horn-contracts "" -assert -dev -t:60 +run_test ./rundir horn-contracts "" -assert -dev -solutionReconstruction:wp -t:60 run_test ./rundir acsl-contracts "" -assertNoVerify -t:60 run_test ./rundir acsl-standalone "" -m:foo -assertNoVerify -cex -t:60 run_test ./rundir uninterpreted-predicates "" -assert -dev -t:60 @@ -37,7 +37,7 @@ run_test ./rundir math-arrays "" -assert -dev -t:60 run_test ./rundir quantifiers "" -assert -dev -t:60 run_test ./rundir interpreted-predicates "" -assert -dev -t:60 run_test ./rundir properties "" -assert -dev -t:60 -run_test ./rundir toh-contract-translation "" -dev -t:60 +run_test ./rundir toh-contract-translation "" -dev -solutionReconstruction:wp -t:60 run_test ./rundir loop-invariants "" -m:foo -inv -acsl -cex -dev -t:60 run_test ./rundir at-expressions "" -assert -dev -t:60 #run_test ./rundir ParametricEncoder "" diff --git a/regression-tests/toh-contract-translation/Answers b/regression-tests/toh-contract-translation/Answers index e1e76b28..1ba19093 100644 --- a/regression-tests/toh-contract-translation/Answers +++ b/regression-tests/toh-contract-translation/Answers @@ -63,7 +63,7 @@ Inferred ACSL annotations /* contract for findMax */ /*@ requires b == y && a == x && \separated(x, y) && \valid(y) && \valid(x); - ensures b == \old(y) && a == \old(x) && \old(b_init) == b_init && \old(a_init) == a_init && \old(r) == r && \old(b) == \old(y) && \old(a) == \old(x) && \separated(x, y) && \valid(y) && \valid(x) && ((b_init == \result && \result - a_init >= 1) || (\result == a_init && a_init >= b_init)); + ensures b == \old(y) && a == \old(x) && \old(b_init) == b_init && \old(a_init) == a_init && \old(r) == r && \old(b) == \old(y) && \old(a) == \old(x) && \separated(x, y) && \valid(y) && \valid(x) && ((\result == b_init && b_init - a_init >= 1) || (\result == a_init && a_init >= b_init)); */ ================================================================================ @@ -78,7 +78,7 @@ Inferred ACSL annotations /* contract for findMax */ /*@ requires b == y && a == x && r == max && \separated(y, max) && \separated(x, y) && \separated(x, max) && \valid(y) && \valid(x) && \valid(max); - ensures b_init == \old(b_init) && a_init == \old(a_init) && \old(max) == r && \old(y) == b && \old(x) == a && \old(b) == b && \old(a) == a && \old(r) == r && \separated(b, r) && \separated(a, b) && \separated(a, r) && \valid(b) && \valid(a) && \valid(r); + ensures b_init == \old(b_init) && a_init == \old(a_init) && \old(max) == r && \old(y) == b && \old(x) == a && \old(b) == b && \old(a) == a && \old(r) == r && \separated(b, r) && \separated(a, b) && \separated(a, r) && \valid(b) && \valid(a) && \valid(r) && (\old(a_init) >= \old(b_init) || (\old(b_init) - \old(a_init) >= 1 && *r == \old(b_init))) && (*r == \old(a_init) || (\old(b_init) - \old(a_init) >= 1 && *r == \old(b_init))); */ ================================================================================ @@ -106,18 +106,18 @@ SAFE truck-2.c ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Init: - main21_1(emptyHeap, 0, 0, 0, emptyHeap, 0, 0, 0) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - | - | - V - main46_22(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Truck(Truck(5, nthAddr(3))))), O_Human(Human(2)))), O_Human(Human(3)))), 2, 3, 5, emptyHeap, 0, 0, 0, 1) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + main21_1(heap.empty, 0, 0, 0, heap.empty, 0, 0, 0) +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + | + | + V + main46_22(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Truck(Truck(5, heap.addr(3))))), O_Human(Human(2)))), O_Human(Human(3)))), 2, 3, 5, heap.empty, 0, 0, 0, 1) +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Final: - main46_22(newHeap(alloc(newHeap(alloc(newHeap(alloc(emptyHeap, O_Truck(Truck(5, nthAddr(3))))), O_Human(Human(2)))), O_Human(Human(3)))), 2, 3, 5, emptyHeap, 0, 0, 0, 1) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + main46_22(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.heapAddrPair_1(heap.alloc(heap.empty, O_Truck(Truck(5, heap.addr(3))))), O_Human(Human(2)))), O_Human(Human(3)))), 2, 3, 5, heap.empty, 0, 0, 0, 1) +---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Failed assertion: UNSAFE diff --git a/src/main/scala/tricera/HeapInfo.scala b/src/main/scala/tricera/HeapInfo.scala index a8f8815d..b0930569 100644 --- a/src/main/scala/tricera/HeapInfo.scala +++ b/src/main/scala/tricera/HeapInfo.scala @@ -66,10 +66,10 @@ final case class HeapInfo(heap: Heap, heapModel : HeapModel) { function == heap.alloc def isNewHeapFun(function: IFunction): Boolean = - function == heap.allocResHeap + function == heap.heapAddrPair_1 def isNewAddrFun(function: IFunction): Boolean = - function == heap.allocResAddr + function == heap.heapAddrPair_2 def isHeap(constant: ProgVarProxy): Boolean = heapModel match { case m : HeapTheoryModel => diff --git a/src/main/scala/tricera/acsl/ACSLTranslator.scala b/src/main/scala/tricera/acsl/ACSLTranslator.scala index c960cb74..9c0ce465 100644 --- a/src/main/scala/tricera/acsl/ACSLTranslator.scala +++ b/src/main/scala/tricera/acsl/ACSLTranslator.scala @@ -849,7 +849,7 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { array.typ match { case p : CCHeapPointer => val heap: ITerm = if (useOldHeap) ctx.getOldHeapTerm else ctx.getHeapTerm - val access: IFunApp = ctx.getHeap.addressRangeNth(array.toTerm, index.toTerm) + val access: IFunApp = ctx.getHeap.rangeNth(array.toTerm, index.toTerm) val readObj: IFunApp = ctx.getHeap.read(heap, access) val getObj: IFunction = ctx.sortGetter(p.typ.toSort).getOrElse( throw new ACSLParseException(s"Cannot access $array[$index].", srcInfo) @@ -857,7 +857,7 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { CCTerm.fromTerm(getObj(readObj), p.typ, array.srcInfo) case p : CCHeapArrayPointer => val heap: ITerm = if (useOldHeap) ctx.getOldHeapTerm else ctx.getHeapTerm - val access: IFunApp = ctx.getHeap.addressRangeNth(array.toTerm, index.toTerm) + val access: IFunApp = ctx.getHeap.rangeNth(array.toTerm, index.toTerm) val readObj: IFunApp = ctx.getHeap.read(heap, access) val getObj: IFunction = ctx.sortGetter(p.elementType.toSort).getOrElse( throw new ACSLParseException(s"Cannot access $array[$index].", srcInfo) diff --git a/src/main/scala/tricera/concurrency/Symex.scala b/src/main/scala/tricera/concurrency/Symex.scala index ede92c50..32b42e4f 100644 --- a/src/main/scala/tricera/concurrency/Symex.scala +++ b/src/main/scala/tricera/concurrency/Symex.scala @@ -500,11 +500,14 @@ class Symex private (context : SymexContext, /** The original sub-expression that this AssignmentTarget was created from. */ def originalExp : Exp - /** Performs the state update for this type of LHS. */ - def update(newValue : CCTerm) + /** Performs the state update for this type of LHS using the passed RHS. + * Since the RHS may change using information from the LHS, it is also + * returned to be put on the stack (to be returned as the result of the + * statement). */ + def update(rhsVal : CCTerm) (implicit symex : Symex, evalSettings : EvalSettings, - evalCtx : EvalContext) : Unit + evalCtx : EvalContext) : CCTerm /** Same as update, but writes a non-deterministic value and also returns that value. */ def updateNonDet(implicit symex : Symex, @@ -519,14 +522,14 @@ class Symex private (context : SymexContext, private case class SimpleVar(exp : Exp) extends AssignmentTarget { override def originalExp : Exp = exp - override def update(newValue : CCTerm) + override def update(rhsVal : CCTerm) (implicit symex : Symex, evalSettings : EvalSettings, - evalCtx : EvalContext) : Unit = { + evalCtx : EvalContext) : CCTerm = { val lhsVal = eval(exp)(evalSettings, evalCtx.withEvaluatingLHS(true)) val lhsName = asLValue(exp) - val actualRhsVal = newValue match { + val actualRhsVal = rhsVal match { case CCTerm(_, _: CCStackPointer, srcInfo, _) => throw new UnsupportedCFragmentException( getLineStringShort(srcInfo) + " Only limited support for stack pointers") @@ -534,13 +537,13 @@ class Symex private (context : SymexContext, if (value.intValue != 0) { throw new TranslationException("Pointer assignment only supports 0 (NULL)") } else CCTerm.fromTerm( - context.heap.nullAddr(), CCHeapPointer(context.heap, lhsVal.typ), newValue.srcInfo) - case _ => newValue + context.heap.nullAddr(), CCHeapPointer(context.heap, lhsVal.typ), rhsVal.srcInfo) + case _ => rhsVal } val actualLhsTerm = getActualAssignedTerm(lhsVal, actualRhsVal) - newValue.typ match { + rhsVal.typ match { case arrayPtr1 : CCHeapArrayPointer => lhsVal.typ match { case _ : CCHeapPointer => @@ -557,19 +560,23 @@ class Symex private (context : SymexContext, case _ => } setValue(lhsName, actualLhsTerm, evalCtx.enclosingFunctionName) + actualRhsVal } } private case class StructField(baseExp : Exp, path : List[String], originalExp : Exp) extends AssignmentTarget { - override def update(newValue : CCTerm) + override def update(rhsVal : CCTerm) (implicit symex : Symex, evalSettings : EvalSettings, - evalCtx : EvalContext) : Unit = { - pushVal(newValue) + evalCtx : EvalContext) : CCTerm = { + val pushedRhs = rhsVal.t match { + case IIntLit(_) => false // no need to push + case _ => pushVal(rhsVal) ; true + } val baseLHSVal = eval(baseExp)(evalSettings, evalCtx.withEvaluatingLHS(true)) - val newValue2 = popVal + val rhsVal2 = if (pushedRhs) popVal else rhsVal val locTerm = getStaticLocationId(originalExp) baseLHSVal.typ match { case ptr : CCHeapPointer => // p->f @@ -582,16 +589,19 @@ class Symex private (context : SymexContext, val fieldAddress = getFieldAddress(structType, path) val fieldTerm = structType.getFieldTerm(baseLHSVal, fieldAddress) - val actualRhsVal = newValue match { // must match on newValue, not newValue2 + val actualRhsVal = rhsVal2 match { case CCTerm(_, _: CCStackPointer, srcInfo, _) => throw new UnsupportedCFragmentException( - getLineStringShort(srcInfo) + " Only limited support for stack pointers") + getLineStringShort(srcInfo) + + " Only limited support for stack pointers") case CCTerm(IIntLit(value), _, _, _) if isHeapPointer(fieldTerm) => if (value.intValue != 0) { - throw new TranslationException("Pointer assignment only supports 0 (NULL)") + throw new TranslationException( + "Pointer assignment only supports 0 (NULL)") } else CCTerm.fromTerm( - context.heap.nullAddr(), CCHeapPointer(context.heap, fieldTerm.typ), newValue.srcInfo) - case _ => newValue2 + context.heap.nullAddr(), + CCHeapPointer(context.heap, fieldTerm.typ), rhsVal2.srcInfo) + case _ => rhsVal2 } if (structType.sels.size > 1 || path.size > 1) { @@ -600,33 +610,37 @@ class Symex private (context : SymexContext, pushVal(processHeapResult(heapModel.read(baseLHSVal, values, locTerm)).get) maybeOutputClause(baseLHSVal.srcInfo) val oldStructTerm = popVal.toTerm // the result of the read - val newValue3 = popVal // the rhs value + val rhsVal3 = popVal // the rhs value val curBaseLHSVal = popVal // the address to write - val newStructTerm = structType.setFieldTerm(oldStructTerm, newValue3.toTerm, fieldAddress) - val newStructObj = wrapAsHeapObject(CCTerm.fromTerm(newStructTerm, structType, newValue3.srcInfo)) + val newStructTerm = structType.setFieldTerm(oldStructTerm, rhsVal3.toTerm, fieldAddress) + val newStructObj = wrapAsHeapObject(CCTerm.fromTerm(newStructTerm, structType, rhsVal3.srcInfo)) processHeapResult(heapModel.write(curBaseLHSVal, newStructObj, values, locTerm)) + rhsVal3 } else { // path.size == 1 && structType.sels.size == 1 val newStructTerm = structType.setFieldTerm(actualRhsVal.toTerm) val newStructObj = wrapAsHeapObject(CCTerm.fromTerm(newStructTerm, structType, actualRhsVal.srcInfo)) processHeapResult(heapModel.write(baseLHSVal, newStructObj, values, locTerm)) + actualRhsVal } case structType : CCStruct => // s.f val varName = asLValue(baseExp) val fieldAddress = getFieldAddress(structType, path) val oldStructTerm = baseLHSVal.toTerm - val newStructTerm = structType.setFieldTerm(oldStructTerm, newValue2.toTerm, fieldAddress) - val newStructObj = CCTerm.fromTerm(newStructTerm, structType, newValue2.srcInfo) + val newStructTerm = structType.setFieldTerm(oldStructTerm, rhsVal2.toTerm, fieldAddress) + val newStructObj = CCTerm.fromTerm(newStructTerm, structType, rhsVal2.srcInfo) setValue(varName, newStructObj, evalCtx.enclosingFunctionName) assignedToStruct = true + rhsVal2 case _ : CCStackPointer => // ps->f - pushVal(newValue2) + pushVal(rhsVal2) val lhsVal = eval(originalExp)(evalSettings, evalCtx.withEvaluatingLHS(true)) - val newValue3 = popVal + val rhsVal3 = popVal val lhsName = asLValue(originalExp) - val actualLhsTerm = getActualAssignedTerm(lhsVal, newValue3) + val actualLhsTerm = getActualAssignedTerm(lhsVal, rhsVal3) setValue(lhsName, actualLhsTerm, evalCtx.enclosingFunctionName) + rhsVal3 case _ => throw new TranslationException( "Invalid base for a struct field access: " + baseLHSVal) @@ -637,29 +651,40 @@ class Symex private (context : SymexContext, private case class ArrayElement(arrayBase : Exp, index : Exp, originalExp : Exp) extends AssignmentTarget { - override def update(newValue : CCTerm) + override def update(rhsVal : CCTerm) (implicit symex : Symex, evalSettings : EvalSettings, - evalCtx : EvalContext): Unit = { - val arrayTerm = eval(arrayBase)(evalSettings, evalCtx.withEvaluatingLHS(true)) + evalCtx : EvalContext) : CCTerm = { + val pushedRhs = rhsVal.t match { + case IIntLit(_) => false // no need to push + case _ => pushVal(rhsVal) ; true + } + val arrayTerm = eval(arrayBase)(evalSettings, + evalCtx.withEvaluatingLHS(true)) val indexTerm = eval(index) + val rhsVal2 = if (pushedRhs) popVal else rhsVal arrayTerm.typ match { case _ : CCHeapArrayPointer => processHeapResult(heapModel.arrayWrite( - arrayTerm, indexTerm, wrapAsHeapObject(newValue), values, getStaticLocationId(originalExp))) + arrayTerm, indexTerm, wrapAsHeapObject(rhsVal2), + values, getStaticLocationId(originalExp))) + rhsVal2 case _ : CCArray => - val lhsVal = eval(originalExp)(evalSettings, evalCtx.withEvaluatingLHS(true)) + val lhsVal = eval(originalExp)(evalSettings, + evalCtx.withEvaluatingLHS(true)) val newTerm = CCTerm.fromTerm(writeADT( lhsVal.toTerm.asInstanceOf[IFunApp], - newValue.toTerm, context.heap.userHeapConstructors, - context.heap.userHeapSelectors), lhsVal.typ, newValue.srcInfo) + rhsVal.toTerm, context.heap.userHeapConstructors, + context.heap.userHeapSelectors), lhsVal.typ, rhsVal2.srcInfo) val lhsName = asLValue(arrayBase) val oldLhsVal = getValue(lhsName, evalCtx.enclosingFunctionName) val innerTerm = lhsVal.toTerm.asInstanceOf[IFunApp].args.head val actualLhsTerm = getActualAssignedTerm( - CCTerm.fromTerm(innerTerm, oldLhsVal.typ, newValue.srcInfo), newTerm) + CCTerm.fromTerm(innerTerm, oldLhsVal.typ, rhsVal2.srcInfo), newTerm) setValue(lhsName, actualLhsTerm, evalCtx.enclosingFunctionName) - case _ => throw new TranslationException("Attempting array access on a non-array type.") + rhsVal2 + case _ => throw new TranslationException( + "Attempting array access on a non-array type.") } } } @@ -668,35 +693,48 @@ class Symex private (context : SymexContext, index : Exp, path : List[String], originalExp : Exp) extends AssignmentTarget { - override def update(newValue : CCTerm) + override def update(rhsVal : CCTerm) (implicit symex : Symex, evalSettings : EvalSettings, - evalCtx : EvalContext) : Unit = { + evalCtx : EvalContext) : CCTerm = { + val pushedRhs = rhsVal.t match { + case IIntLit(_) => false // no need to push + case _ => pushVal(rhsVal) ; true + } val arrayTerm = eval(arrayBase)(evalSettings, evalCtx.withEvaluatingLHS(true)) val indexTerm = eval(index) + val rhsVal2 = if (pushedRhs) popVal else rhsVal arrayTerm.typ match { case array : CCArray => - val oldStructTerm = array.arrayTheory.select(arrayTerm.toTerm, indexTerm.toTerm) + val oldStructTerm = + array.arrayTheory.select(arrayTerm.toTerm, indexTerm.toTerm) val structType = array.elementType.asInstanceOf[CCStruct] val fieldAddress = getFieldAddress(structType, path) val newStructInnerTerm = structType.setFieldTerm( - oldStructTerm, newValue.toTerm, fieldAddress) + oldStructTerm, rhsVal2.toTerm, fieldAddress) val newArrayTerm = array.arrayTheory.store( arrayTerm.toTerm, indexTerm.toTerm, newStructInnerTerm) val arrayVarName = asLValue(arrayBase) setValue(arrayVarName, CCTerm.fromTerm( - newArrayTerm, arrayTerm.typ, newValue.srcInfo), evalCtx.enclosingFunctionName) + newArrayTerm, arrayTerm.typ, rhsVal.srcInfo), + evalCtx.enclosingFunctionName) + rhsVal2 case array : CCHeapArrayPointer => val locTerm = getStaticLocationId(originalExp) - val readResult = processHeapResult(heapModel.arrayRead(arrayTerm, indexTerm, values, locTerm)).get + val readResult = processHeapResult( + heapModel.arrayRead(arrayTerm, indexTerm, values, locTerm)).get val oldStructTerm = readResult.toTerm val structType = array.elementType.asInstanceOf[CCStruct] val fieldAddress = getFieldAddress(structType, path) - val newStructInnerTerm = structType.setFieldTerm(oldStructTerm, newValue.toTerm, fieldAddress) - val newStructObj = CCTerm.fromTerm(newStructInnerTerm, structType, newValue.srcInfo) + val newStructInnerTerm = + structType.setFieldTerm(oldStructTerm, rhsVal2.toTerm, fieldAddress) + val newStructObj = CCTerm.fromTerm( + newStructInnerTerm, structType, rhsVal2.srcInfo) processHeapResult(heapModel.arrayWrite( - arrayTerm, indexTerm, wrapAsHeapObject(newStructObj), values, locTerm)) + arrayTerm, indexTerm, wrapAsHeapObject(newStructObj), + values, locTerm)) + rhsVal2 case _ => throw new TranslationException( "Field access on an element of a non-struct array.") @@ -706,19 +744,29 @@ class Symex private (context : SymexContext, private case class PointerDeref(pointerExp : Exp, originalExp : Exp) extends AssignmentTarget { - override def update(newValue : CCTerm) + override def update(rhsVal : CCTerm) (implicit symex : Symex, evalSettings : EvalSettings, - evalCtx : EvalContext) : Unit = { - val pointerVal = eval(pointerExp)(evalSettings, evalCtx.withEvaluatingLHS(false)) + evalCtx : EvalContext) : CCTerm = { + val pushedRhs = rhsVal.t match { + case IIntLit(_) => false // no need to push + case _ => pushVal(rhsVal) ; true + } + val pointerVal = + eval(pointerExp)(evalSettings, evalCtx.withEvaluatingLHS(false)) + val rhsVal2 = if (pushedRhs) popVal else rhsVal if (isHeapPointer(pointerVal)) { - processHeapResult(heapModel.write(pointerVal, wrapAsHeapObject(newValue), - values, getStaticLocationId(originalExp))) + processHeapResult(heapModel.write( + pointerVal, wrapAsHeapObject(rhsVal2), + values, getStaticLocationId(originalExp))) + rhsVal2 } else { - val lhsVal = eval(originalExp)(evalSettings, evalCtx.withEvaluatingLHS(true)) + val lhsVal = eval(originalExp)(evalSettings, + evalCtx.withEvaluatingLHS(true)) val lhsName = asLValue(originalExp) - val actualLhsTerm = getActualAssignedTerm(lhsVal, newValue) + val actualLhsTerm = getActualAssignedTerm(lhsVal, rhsVal2) setValue(lhsName, actualLhsTerm, evalCtx.enclosingFunctionName) + rhsVal2 } } } @@ -738,7 +786,8 @@ class Symex private (context : SymexContext, case ArrayStructField(arrayBase, index, path, _) => ArrayStructField(arrayBase, index, path :+ e.cident_, e) case _ => throw new TranslationException( - "Invalid expression for '.' member access in " + (context.printer print e)) + "Invalid expression for '.' member access in " + + (context.printer print e)) } case e: Epreop if e.unary_operator_.isInstanceOf[Indirection] => PointerDeref(e.exp_, e) @@ -899,7 +948,7 @@ class Symex private (context : SymexContext, case _ => evalHelp(exp.exp_2) maybeOutputClause(Some(getSourceInfo(exp))) - getAssignmentTarget(exp.exp_1).update(topVal) + pushVal (getAssignmentTarget(exp.exp_1).update(popVal)) } case exp : Eassign => // Compound assignment: '+=', '-=', etc. @@ -962,9 +1011,8 @@ class Symex private (context : SymexContext, lhsE.typ cast2Unsigned rhsE.toTerm) }), lhsE.typ, lhsE.srcInfo) - pushVal(valueToAssign) implicit val symex: Symex = this - getAssignmentTarget(exp.exp_1).update(valueToAssign) + pushVal(getAssignmentTarget(exp.exp_1).update(valueToAssign)) case exp : Econdition => // exp_1 ? exp_2 : exp_3 val srcInfo = Some(getSourceInfo(exp)) @@ -1118,9 +1166,8 @@ class Symex private (context : SymexContext, evalHelp(expToUpdate) maybeOutputClause(Some(getSourceInfo(exp))) val newValue = popVal mapTerm (_ + op) - pushVal(newValue) implicit val symex: Symex = this - getAssignmentTarget(expToUpdate).update(newValue) + pushVal(getAssignmentTarget(expToUpdate).update(newValue)) case _ : Epostinc | _ : Epostdec => val (expToUpdate, op) = exp match { @@ -1130,10 +1177,12 @@ class Symex private (context : SymexContext, evalHelp(expToUpdate) maybeOutputClause(Some(getSourceInfo(exp))) - val newValue = topVal mapTerm (_ + op) implicit val symex: Symex = this - getAssignmentTarget(expToUpdate).update(newValue) - + val updatedPostValue = // the pre-update value is already on the stack + getAssignmentTarget(expToUpdate).update(topVal mapTerm (_ + op)) + // The following should never fail as topVal's type always should + // always correctly resolve. + assert(updatedPostValue.typ == topVal.typ) case exp : Epreop => val srcInfo = Some(getSourceInfo(exp)) @@ -1163,7 +1212,7 @@ class Symex private (context : SymexContext, // todo: below type extraction is not safe! val heap = context.heap val t = addrTerm match { - case IFunApp(heap.addressRangeNth, args) => // if nthAddrRange(a, i) + case IFunApp(heap.rangeNth, args) => // if nthAddrRange(a, i) val scala.Seq(arrTerm, indTerm) = args // return the addressRange starting from i import heap._ diff --git a/src/main/scala/tricera/concurrency/ccreader/CCBinaryExpressions.scala b/src/main/scala/tricera/concurrency/ccreader/CCBinaryExpressions.scala index b60c4ab6..251ef76a 100644 --- a/src/main/scala/tricera/concurrency/ccreader/CCBinaryExpressions.scala +++ b/src/main/scala/tricera/concurrency/ccreader/CCBinaryExpressions.scala @@ -227,7 +227,7 @@ object CCBinaryExpressions { (lhs.typ, rhs.typ) match { case (_: CCHeapArrayPointer, _: CCArithType) => throw new TranslationException( - "Pointer arithmetic over arrays is only supported with addition.") + "Pointer arithmetic over arrays is only supported with addition.") case _ => // nothing } } diff --git a/src/main/scala/tricera/concurrency/ccreader/CCType.scala b/src/main/scala/tricera/concurrency/ccreader/CCType.scala index 532d9cdf..9ee506ae 100644 --- a/src/main/scala/tricera/concurrency/ccreader/CCType.scala +++ b/src/main/scala/tricera/concurrency/ccreader/CCType.scala @@ -57,7 +57,7 @@ abstract sealed class CCType { case CCHeapObject(heap) => heap.ObjectSort case CCStackPointer(_, _, _) => Sort.Integer case CCHeapPointer(heap, _) => heap.AddressSort - case CCHeapArrayPointer(heap, _, _) => heap.AddressRangeSort + case CCHeapArrayPointer(heap, _, _) => heap.RangeSort case CCArray(_, _, _, s, _) => s.sort case CCStruct(ctor, _) => ctor.resSort case CCStructField(n, s) => s(n).ctor.resSort @@ -80,7 +80,7 @@ abstract sealed class CCType { case CCStackPointer(_, _, _) => Sort.Integer case CCHeapPointer(heap, _) => heap.AddressSort case CCArray(_, _, _, s, _) => s.sort - case CCHeapArrayPointer(heap, _, _) => heap.AddressRangeSort + case CCHeapArrayPointer(heap, _, _) => heap.RangeSort case CCStruct(ctor, _) => ctor.resSort case CCStructField(n, s) => s(n).ctor.resSort case CCIntEnum(_, _) => Sort.Integer @@ -101,7 +101,7 @@ abstract sealed class CCType { case CCHeapObject(heap) => heap.ObjectSort case CCStackPointer(_, _, _) => Sort.Integer case CCHeapPointer(heap, _) => heap.AddressSort - case CCHeapArrayPointer(heap, _, _) => heap.AddressRangeSort + case CCHeapArrayPointer(heap, _, _) => heap.RangeSort case CCArray(_, _, _, s, _) => s.sort case CCStruct(ctor, _) => ctor.resSort case CCStructField(n, s) => s(n).ctor.resSort @@ -123,7 +123,7 @@ abstract sealed class CCType { case CCHeapObject(heap) => heap.ObjectSort case CCStackPointer(_, _, _) => Sort.Integer case CCHeapPointer(heap, _) => heap.AddressSort - case CCHeapArrayPointer(heap, _, _) => heap.AddressRangeSort + case CCHeapArrayPointer(heap, _, _) => heap.RangeSort case CCArray(_, _, _, s, _) => s.sort case CCStruct(ctor, _) => ctor.resSort case CCStructField(n, s) => s(n).ctor.resSort @@ -281,7 +281,7 @@ abstract sealed class CCType { } structType.ctor(const: _*) case CCHeapPointer(heap, _) => heap.nullAddr() - case CCHeapArrayPointer(heap, _, _) => heap.nthAddrRange(0, IIntLit(1)) + case CCHeapArrayPointer(heap, _, _) => heap.range(0, IIntLit(1)) case CCArray(_, _, _, arrayTheory, _) => arrayTheory.const(0) case _ => IIntLit(0) } diff --git a/src/main/scala/tricera/concurrency/heap/HeapTheoryModel.scala b/src/main/scala/tricera/concurrency/heap/HeapTheoryModel.scala index c0956403..cc631642 100644 --- a/src/main/scala/tricera/concurrency/heap/HeapTheoryModel.scala +++ b/src/main/scala/tricera/concurrency/heap/HeapTheoryModel.scala @@ -128,10 +128,10 @@ class HeapTheoryModel(context : SymexContext, override def alloc(o : CCTerm, oType : CCType, s : scala.Seq[CCTerm], loc : CCTerm) : HeapOperationResult = { val newAlloc = context.heap.alloc(getValue(heapVar, s).toTerm, o.toTerm) - val newHeapTerm = CCTerm.fromTerm(context.heap.allocResHeap(newAlloc), + val newHeapTerm = CCTerm.fromTerm(context.heap.heapAddrPair_1(newAlloc), CCHeap(context.heap), o.srcInfo) - val newAddrTerm = CCTerm.fromTerm(context.heap.allocResAddr(newAlloc), + val newAddrTerm = CCTerm.fromTerm(context.heap.heapAddrPair_2(newAlloc), CCHeapPointer(context.heap, oType), o.srcInfo) var nextState = updateValue(heapVar, newHeapTerm, s) @@ -247,11 +247,11 @@ class HeapTheoryModel(context : SymexContext, * (or equivalently forall ind. read(h, nth(t, ind)) =/= defObj) */ val ind = scope.getFreshEvalVar(CCInt, p.srcInfo) - val readAddr = context.heap.addressRangeNth(p.toTerm, ind.term) + val readAddr = context.heap.rangeNth(p.toTerm, ind.term) val readObj = context.heap.read(getValue(heapVar, nextState).toTerm, readAddr) val assertion = CCTerm.fromFormula( p.toTerm === context.heap.nullAddr() ||| - (context.heap.addressRangeWithin(p.toTerm, readAddr) ==> + (context.heap.rangeWithin(p.toTerm, readAddr) ==> (readObj =/= context.heap.defaultObject)), CCInt, p.srcInfo) assertions = (assertion, properties.MemValidFree) :: assertions case _ => @@ -264,7 +264,7 @@ class HeapTheoryModel(context : SymexContext, // This is a side effect: the heap variable is updated with the result of batchWrite. val newHeapTerm = CCTerm.fromTerm( - context.heap.batchWrite(getValue(heapVar, nextState).toTerm, p.toTerm, context.defObj()), + context.heap.writeRange(getValue(heapVar, nextState).toTerm, p.toTerm, context.defObj()), heapVar.typ, p.srcInfo) nextState = updateValue(heapVar, newHeapTerm, nextState) @@ -278,7 +278,7 @@ class HeapTheoryModel(context : SymexContext, val memCleanupTerm = getValue(memCleanupVar.get, nextState) val newMemCleanupTerm = CCTerm.fromTerm( IExpression.ite( - memCleanupTerm.toTerm === context.heap.addressRangeNth(p.toTerm, 0), + memCleanupTerm.toTerm === context.heap.rangeNth(p.toTerm, 0), context.heap.nullAddr(), // then memCleanupTerm.toTerm), // else memCleanupTerm.typ, None) @@ -307,14 +307,14 @@ class HeapTheoryModel(context : SymexContext, s : scala.Seq[CCTerm]) : HeapOperationResult = { // TODO: remvoe the wrappers from here too! val newBatchAlloc = - context.heap.batchAlloc(getValue(heapVar, s).toTerm, + context.heap.allocRange(getValue(heapVar, s).toTerm, context.sortWrapperMap(o.typ.toSort)(o.toTerm), size) val newHeapTerm = CCTerm.fromTerm( - context.heap.batchAllocResHeap(newBatchAlloc), + context.heap.heapRangePair_1(newBatchAlloc), CCHeap(context.heap), o.srcInfo) val newAddrRange = CCTerm.fromTerm( - context.heap.batchAllocResAddr(newBatchAlloc), + context.heap.heapRangePair_2(newBatchAlloc), CCHeapArrayPointer(context.heap, o.typ, arrayLoc), o.srcInfo) var nextState = updateValue(heapVar, newHeapTerm, s) @@ -329,7 +329,7 @@ class HeapTheoryModel(context : SymexContext, val newProphTerm = CCTerm.fromTerm( IExpression.ite( nondetTerm === ap.theories.ADT.BoolADT.True & size > 0, - context.heap.addressRangeNth(newAddrRange.toTerm, 0), + context.heap.rangeNth(newAddrRange.toTerm, 0), prophTerm.toTerm), prophTerm.typ, None) nextState = updateValue(memCleanupVar.get, newProphTerm, nextState) } @@ -346,7 +346,7 @@ class HeapTheoryModel(context : SymexContext, loc : CCTerm) : HeapOperationResult = { val arrType = arr.typ.asInstanceOf[CCHeapArrayPointer] val readAddress = CCTerm.fromTerm( - context.heap.addressRangeNth(arr.toTerm, index.toTerm), + context.heap.rangeNth(arr.toTerm, index.toTerm), CCHeapPointer(context.heap, arrType.elementType), arr.srcInfo) @@ -355,7 +355,7 @@ class HeapTheoryModel(context : SymexContext, val boundsAssertion = if (context.propertiesToCheck.contains(properties.MemValidDeref)) { val assertion = CCTerm.fromFormula( - context.heap.addressRangeWithin( + context.heap.rangeWithin( arr.toTerm, readAddress.toTerm), CCInt, arr.srcInfo) scala.Seq((assertion, properties.MemValidDeref)) } else { @@ -378,7 +378,7 @@ class HeapTheoryModel(context : SymexContext, loc : CCTerm) : HeapOperationResult = { val arrType = arr.typ.asInstanceOf[CCHeapArrayPointer] val writeAddress = CCTerm.fromTerm( - context.heap.addressRangeNth(arr.toTerm, index.toTerm), + context.heap.rangeNth(arr.toTerm, index.toTerm), CCHeapPointer(context.heap, arrType.elementType), arr.srcInfo) @@ -387,7 +387,7 @@ class HeapTheoryModel(context : SymexContext, val boundsAssertion = if (context.propertiesToCheck.contains(properties.MemValidDeref)) { val assertion = CCTerm.fromFormula( - context.heap.addressRangeWithin( + context.heap.rangeWithin( arr.toTerm, writeAddress.toTerm), CCInt, index.srcInfo) scala.Seq((assertion, properties.MemValidDeref)) } else { @@ -433,7 +433,7 @@ class HeapTheoryModel(context : SymexContext, } val wrappedValue = context.sortWrapperMap(Sort.sortOf(valueToInit))(valueToInit) - val addrToWrite = context.heap.addressRangeNth(arrayBasePtr, i) + val addrToWrite = context.heap.rangeNth(arrayBasePtr, i) val writeResult = write( CCTerm.fromTerm(addrToWrite, CCHeapPointer(context.heap, arrayPtr.elementType), None), CCTerm.fromTerm(wrappedValue, arrayPtr.elementType, None), @@ -464,8 +464,8 @@ class HeapTheoryModel(context : SymexContext, case None => SimpleResult( returnValue = Some(CCTerm.fromTerm( - context.heap.batchAllocResAddr( - context.heap.batchAlloc( + context.heap.heapRangePair_2( + context.heap.allocRange( context.heap.emptyHeap(), context.heap.defaultObject, IIntLit(0))), CCHeapArrayPointer(context.heap, objTerm.typ, loc), objTerm.srcInfo)), diff --git a/src/main/scala/tricera/params/TriCeraParameters.scala b/src/main/scala/tricera/params/TriCeraParameters.scala index 6dd15aa7..d4c40bbe 100644 --- a/src/main/scala/tricera/params/TriCeraParameters.scala +++ b/src/main/scala/tricera/params/TriCeraParameters.scala @@ -136,7 +136,7 @@ class TriCeraParameters extends GlobalParameters { override def withAndWOTemplates : Seq[TriCeraParameters] = for (p <- super.withAndWOTemplates) yield p.asInstanceOf[TriCeraParameters] - solutionReconstruction = GlobalParameters.SolutionReconstruction.WP + solutionReconstruction = GlobalParameters.SolutionReconstruction.CEGAR private val version = "0.4" @@ -396,8 +396,8 @@ class TriCeraParameters extends GlobalParameters { |Horn engine options (Eldarica): |-sym (Experimental) Use symbolic execution with the default engine (bfs) |-sym:t Use symbolic execution where t : {dfs, bfs} - | dfs: depth-first forward (does not support non-linear clauses) - | bfs: breadth-first forward + | dfs : depth-first forward (does not support non-linear clauses) + | bfs : breadth-first forward |-symDepth:n Set a max depth for symbolic execution (underapproximate) | (currently only supported with bfs) |-disj Use disjunctive interpolation @@ -414,9 +414,9 @@ class TriCeraParameters extends GlobalParameters { |-splitClauses:n Aggressiveness when splitting disjunctions in clauses | (0 <= n <= 2, default: 1) |-solutionReconstruction:t - | Solution reconstruction method where t : {wp, cegar} - | wp : weakest-preconditions-based reconstruction (default) - | cegar : CEGAR-based reconstruction + | Solution reconstruction method where t : {cegar, wp} + | cegar : CEGAR-based reconstruction (default) + | wp : weakest-preconditions-based reconstruction |-pHints Print initial predicates and abstraction templates |-logSimplified Show clauses after Eldarica preprocessing in Prolog format |-logSimplifiedSMT Show clauses after Eldarica preprocessing in SMT-LIB format diff --git a/src/main/scala/tricera/postprocessor/ContractProcessorUtils.scala b/src/main/scala/tricera/postprocessor/ContractProcessorUtils.scala index 8fed894d..2a659583 100644 --- a/src/main/scala/tricera/postprocessor/ContractProcessorUtils.scala +++ b/src/main/scala/tricera/postprocessor/ContractProcessorUtils.scala @@ -129,10 +129,10 @@ case class ContractConditionInfo(predicate: Predicate, ci: ContractInfo) { def isAllocFun(function: IFunction): Boolean = function == heapTheory.alloc def isNewHeapFun(function: IFunction): Boolean = - function == heapTheory.allocResHeap + function == heapTheory.heapAddrPair_1 def isNewAddrFun(function: IFunction): Boolean = - function == heapTheory.allocResAddr + function == heapTheory.heapAddrPair_2 def isGetter(function: IFunction): Boolean = acslContext.getterSort(function).isDefined