Add extra processing in alpha equality for MockDeterministicSource

UnitTestBot · Nov 3, 2023 · 635ef23 · 635ef23
1 parent 33e55ff
commit 635ef23
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 3 deletions.
diff --git a/lib/Expr/AlphaBuilder.cpp b/lib/Expr/AlphaBuilder.cpp
@@ -19,8 +19,18 @@ const Array *AlphaBuilder::visitArray(const Array *arr) {
   if (alphaArrayMap.find(arr) == alphaArrayMap.end()) {
     ref<SymbolicSource> source = arr->source;
     ref<Expr> size = visit(arr->getSize());
-
-    if (!arr->isConstantArray()) {
+    if (ref<MockDeterministicSource> mockSource =
+            dyn_cast_or_null<MockDeterministicSource>(source)) {
+      std::vector<ref<Expr>> args;
+      for (const auto &it : mockSource->args) {
+        args.push_back(visit(it));
+      }
+      source = SourceBuilder::mockDeterministic(mockSource->km,
+                                                mockSource->function, args);
+      alphaArrayMap[arr] = arrayCache.CreateArray(
+          size, source, arr->getDomain(), arr->getRange());
+      reverseAlphaArrayMap[alphaArrayMap[arr]] = arr;
+    } else if (!arr->isConstantArray()) {
       source = SourceBuilder::alpha(index);
       index++;
       alphaArrayMap[arr] = arrayCache.CreateArray(

diff --git a/test/Feature/MockStrategies.c b/test/Feature/MockStrategies.c
@@ -18,7 +18,7 @@
 // CHECK-3: KLEE: ERROR: Deterministic mocks can be generated with Z3 solver only.
 
 // RUN: rm -rf %t.klee-out-4
-// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHEsCK-4
+// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4
 // CHECK-4: KLEE: done: completed paths = 2
 // CHECK-4: KLEE: done: generated tests = 2