diff --git a/Ghidra/Debug/Debugger-api/src/main/java/ghidra/app/services/DebuggerEmulationService.java b/Ghidra/Debug/Debugger-api/src/main/java/ghidra/app/services/DebuggerEmulationService.java
index 9b896db335..f148775514 100644
--- a/Ghidra/Debug/Debugger-api/src/main/java/ghidra/app/services/DebuggerEmulationService.java
+++ b/Ghidra/Debug/Debugger-api/src/main/java/ghidra/app/services/DebuggerEmulationService.java
@@ -4,9 +4,9 @@
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
- *
+ *
* http://www.apache.org/licenses/LICENSE-2.0
- *
+ *
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
@@ -55,13 +55,20 @@ public interface DebuggerEmulationService {
/**
* The result of letting the emulator "run free"
+ *
+ * @param schedule the schedule that was emulated
+ * @param snapshot the snapshot where the final state was written down
+ * @param error if an error occurred, the error, or null
*/
record RecordEmulationResult(TraceSchedule schedule, long snapshot, Throwable error)
- implements EmulationResult {
- }
+ implements EmulationResult {}
/**
* An emulator managed by this service
+ *
+ * @param trace the trace the emulator is bound to
+ * @param emulator the emulator itself
+ * @param version the cache version. See {@link #isValid()}.
*/
record CachedEmulator(Trace trace, DebuggerPcodeMachine emulator, long version) {
public CachedEmulator(Trace trace, DebuggerPcodeMachine emulator) {
@@ -112,14 +119,16 @@ public interface DebuggerEmulationService {
*
* @param emu the emulator
*/
- void running(CachedEmulator emu);
+ default void running(CachedEmulator emu) {
+ }
/**
* An emulator has stopped
*
* @param emu the emulator
*/
- void stopped(CachedEmulator emu);
+ default void stopped(CachedEmulator emu) {
+ }
}
/**
@@ -140,8 +149,7 @@ public interface DebuggerEmulationService {
*
* TODO: Should there be some opinion service for choosing default configs? Seems overly
* complicated for what it offers. For now, we won't save anything, we'll default to the
- * (built-in) {@link BytesDebuggerPcodeEmulatorFactory}, and we won't have configuration
- * options.
+ * (built-in) concrete emulator, and we won't have configuration options.
*
* @param factory the chosen factory
*/
@@ -228,6 +236,7 @@ public interface DebuggerEmulationService {
* @param monitor a monitor cancellation
* @param scheduler a thread scheduler for the emulator
* @return the result of emulation
+ * @throws CancelledException if the user cancels the task
*/
EmulationResult run(TracePlatform platform, TraceSchedule from, TaskMonitor monitor,
Scheduler scheduler) throws CancelledException;
@@ -268,8 +277,8 @@ public interface DebuggerEmulationService {
* Get the cached emulator for the given trace and time
*
*
- * To guarantee the emulator is present, call {@link #backgroundEmulate(Trace, TraceSchedule)}
- * first.
+ * To guarantee the emulator is present, call
+ * {@link #backgroundEmulate(TracePlatform, TraceSchedule)} first.
*
* WARNING: This emulator belongs to this service. Stepping it, or otherwise manipulating
* it without the service's knowledge can lead to unintended consequences.
@@ -290,6 +299,11 @@ public interface DebuggerEmulationService {
*/
Collection getBusyEmulators();
+ /**
+ * Invalidate the trace's cache of emulated states.
+ */
+ void invalidateCache();
+
/**
* Add a listener for emulator state changes
*
diff --git a/Ghidra/Debug/Debugger/src/main/java/ghidra/app/plugin/core/debug/service/emulation/DebuggerEmulationServicePlugin.java b/Ghidra/Debug/Debugger/src/main/java/ghidra/app/plugin/core/debug/service/emulation/DebuggerEmulationServicePlugin.java
index e676146445..898754a2a7 100644
--- a/Ghidra/Debug/Debugger/src/main/java/ghidra/app/plugin/core/debug/service/emulation/DebuggerEmulationServicePlugin.java
+++ b/Ghidra/Debug/Debugger/src/main/java/ghidra/app/plugin/core/debug/service/emulation/DebuggerEmulationServicePlugin.java
@@ -554,6 +554,16 @@ public class DebuggerEmulationServicePlugin extends Plugin implements DebuggerEm
}
private void invalidateCacheActivated(ActionContext ignored) {
+ invalidateCache();
+ }
+
+ private void configureEmulatorActivated(DebuggerPcodeEmulatorFactory factory) {
+ // TODO: Pull up config page. Tool Options? Program/Trace Options?
+ setEmulatorFactory(factory);
+ }
+
+ @Override
+ public void invalidateCache() {
DebuggerCoordinates current = traceManager.getCurrent();
Trace trace = current.getTrace();
long version = trace.getEmulatorCacheVersion();
@@ -567,11 +577,6 @@ public class DebuggerEmulationServicePlugin extends Plugin implements DebuggerEm
traceManager.materialize(current);
}
- private void configureEmulatorActivated(DebuggerPcodeEmulatorFactory factory) {
- // TODO: Pull up config page. Tool Options? Program/Trace Options?
- setEmulatorFactory(factory);
- }
-
@Override
public Collection getEmulatorFactories() {
return ClassSearcher.getInstances(DebuggerPcodeEmulatorFactory.class);
diff --git a/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/IndependentPairedTracePcodeExecutorState.java b/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/IndependentPairedTracePcodeExecutorState.java
new file mode 100644
index 0000000000..12a6bdc308
--- /dev/null
+++ b/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/IndependentPairedTracePcodeExecutorState.java
@@ -0,0 +1,60 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.exec.trace;
+
+import org.apache.commons.lang3.tuple.Pair;
+
+import ghidra.pcode.exec.IndependentPairedPcodeExecutorState;
+import ghidra.pcode.exec.PairedPcodeExecutorState;
+import ghidra.pcode.exec.trace.data.PcodeTraceDataAccess;
+
+/**
+ * A trace-bound state composed of another trace-bound state and a piece
+ *
+ * @param the type of values for the left state
+ * @param the type of values for the right piece
+ * @see PairedPcodeExecutorState
+ */
+public class IndependentPairedTracePcodeExecutorState
+ extends IndependentPairedPcodeExecutorState
+ implements TracePcodeExecutorState> {
+
+ private final TracePcodeExecutorStatePiece left;
+ private final TracePcodeExecutorStatePiece right;
+
+ public IndependentPairedTracePcodeExecutorState(TracePcodeExecutorStatePiece left,
+ TracePcodeExecutorStatePiece right) {
+ super(left, right);
+ this.left = left;
+ this.right = right;
+ }
+
+ @Override
+ public PcodeTraceDataAccess getData() {
+ return left.getData();
+ }
+
+ @Override
+ public void writeDown(PcodeTraceDataAccess into) {
+ left.writeDown(into);
+ right.writeDown(into);
+ }
+
+ @Override
+ public IndependentPairedTracePcodeExecutorState fork() {
+ return new IndependentPairedTracePcodeExecutorState<>(left.fork(), right.fork());
+ }
+}
diff --git a/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/data/DefaultPcodeTracePropertyAccess.java b/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/data/DefaultPcodeTracePropertyAccess.java
index a72eeaed47..81311aa29a 100644
--- a/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/data/DefaultPcodeTracePropertyAccess.java
+++ b/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/data/DefaultPcodeTracePropertyAccess.java
@@ -4,9 +4,9 @@
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
- *
+ *
* http://www.apache.org/licenses/LICENSE-2.0
- *
+ *
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
@@ -16,6 +16,7 @@
package ghidra.pcode.exec.trace.data;
import ghidra.program.model.address.*;
+import ghidra.program.model.lang.Language;
import ghidra.trace.model.Lifespan;
import ghidra.trace.model.property.*;
@@ -49,6 +50,11 @@ public class DefaultPcodeTracePropertyAccess
this.po = data.getPropertyOps(name, type, false);
}
+ @Override
+ public Language getLanguage() {
+ return data.getLanguage();
+ }
+
/**
* Get the interface for accessing the trace property on memory or registers
*
@@ -114,6 +120,21 @@ public class DefaultPcodeTracePropertyAccess
ops.clear(span, toOverlay(ops, hostRange));
}
+ @Override
+ public boolean hasSpace(AddressSpace space) {
+ TracePropertyMapOperations ops = getPropertyOperations(false);
+ if (ops == null) {
+ return false;
+ }
+ if (ops instanceof TracePropertyMapSpace propSpace) {
+ return propSpace.getAddressSpace() == space;
+ }
+ if (ops instanceof TracePropertyMap propMap) {
+ return propMap.getPropertyMapSpace(space, false) != null;
+ }
+ throw new AssertionError();
+ }
+
/**
* If this provides access to an overlay space, translate the physical address to it
*
diff --git a/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/data/PcodeTracePropertyAccess.java b/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/data/PcodeTracePropertyAccess.java
index 2a185f3982..0439fbc29d 100644
--- a/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/data/PcodeTracePropertyAccess.java
+++ b/Ghidra/Debug/Framework-TraceModeling/src/main/java/ghidra/pcode/exec/trace/data/PcodeTracePropertyAccess.java
@@ -4,9 +4,9 @@
* Licensed under the Apache License, Version 2.0 (the "License");
* you may not use this file except in compliance with the License.
* You may obtain a copy of the License at
- *
+ *
* http://www.apache.org/licenses/LICENSE-2.0
- *
+ *
* Unless required by applicable law or agreed to in writing, software
* distributed under the License is distributed on an "AS IS" BASIS,
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
@@ -15,8 +15,8 @@
*/
package ghidra.pcode.exec.trace.data;
-import ghidra.program.model.address.Address;
-import ghidra.program.model.address.AddressRange;
+import ghidra.program.model.address.*;
+import ghidra.program.model.lang.Language;
/**
* A trace-property access shim for a specific property
@@ -27,6 +27,11 @@ import ghidra.program.model.address.AddressRange;
* @param the type of the property's values
*/
public interface PcodeTracePropertyAccess {
+ /**
+ * @see PcodeTraceDataAccess#getLanguage()
+ */
+ Language getLanguage();
+
/**
* Get the property's value at the given address
*
@@ -57,4 +62,18 @@ public interface PcodeTracePropertyAccess {
* @param range the range
*/
void clear(AddressRange range);
+
+ /**
+ * Check if the trace has allocated property space for the given address space
+ *
+ *
+ * This is available for optimizations when it may take effort to compute an address. If the
+ * space is not allocated, then no matter the offset, the property will not have a value.
+ * Clients can check this method to avoid the address computation, if they already know the
+ * address space.
+ *
+ * @param space the address space
+ * @return true if there is a property space
+ */
+ boolean hasSpace(AddressSpace space);
}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/Module.manifest b/Ghidra/Debug/SymbolicSummaryZ3/Module.manifest
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/README.md b/Ghidra/Debug/SymbolicSummaryZ3/README.md
new file mode 100644
index 0000000000..717dc4afe0
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/README.md
@@ -0,0 +1,5 @@
+# Symbolic Summary Z3 Module
+
+This module is shipped with the pre-built Z3 version 4.13.0 libraries and java bindings from [the Z3Prover repository](https://github.com/Z3Prover/z3).
+If the native components are not suitably linked for your system, you may need to build from source.
+If so, download the source bundle and follow the instructions for building it on your platform.
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/build.gradle b/Ghidra/Debug/SymbolicSummaryZ3/build.gradle
new file mode 100644
index 0000000000..88681fb829
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/build.gradle
@@ -0,0 +1,138 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+apply from: "$rootProject.projectDir/gradle/javaProject.gradle"
+apply from: "$rootProject.projectDir/gradle/jacocoProject.gradle"
+apply from: "$rootProject.projectDir/gradle/javaTestProject.gradle"
+apply from: "$rootProject.projectDir/gradle/distributableGhidraModule.gradle"
+
+apply plugin: 'eclipse'
+eclipse.project.name = 'Debug SymbolicSummaryZ3'
+
+ext.Z3_VER = "4.13.0"
+ext.Z3_ARM64_OSX_VER = "11.0"
+ext.Z3_X64_OSX_VER = "11.7.10"
+ext.Z3_X64_GLIBC_VER = "2.31"
+// NO Z3_WIN_VER
+
+dependencies {
+ api project(':Debugger')
+ api project(':SystemEmulation')
+ //api "com.microsoft.z3:java-jar:${Z3_VER}"
+ api ":com.microsoft.z3:"
+
+ // Oof. Apparently, this doesn't work transitively....
+ testImplementation project(path: ':ProposedUtils', configuration: 'testArtifacts')
+ testImplementation project(path: ':Framework-TraceModeling', configuration: 'testArtifacts')
+ testImplementation project(path: ':Debugger', configuration: 'testArtifacts')
+}
+
+ext.PLATFORM_BINDINGS = [
+ [
+ name: "mac_arm_64",
+ zip: "z3-${Z3_VER}-arm64-osx-${Z3_ARM64_OSX_VER}.zip",
+ files: [
+ "z3-${Z3_VER}-arm64-osx-${Z3_ARM64_OSX_VER}/bin/libz3.dylib",
+ "z3-${Z3_VER}-arm64-osx-${Z3_ARM64_OSX_VER}/bin/libz3java.dylib"
+ ]
+ ],
+ [
+ name: "linux_x86_64",
+ zip: "z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}.zip",
+ files: [
+ "z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}/bin/libz3.so",
+ "z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}/bin/libz3java.so"
+ ]
+ ],
+ [
+ name: "mac_x86_64",
+ zip: "z3-${Z3_VER}-x64-osx-${Z3_X64_OSX_VER}.zip",
+ files: [
+ "z3-${Z3_VER}-x64-osx-${Z3_X64_OSX_VER}/bin/libz3.dylib",
+ "z3-${Z3_VER}-x64-osx-${Z3_X64_OSX_VER}/bin/libz3java.dylib"
+ ]
+ ],
+ [
+ name: "win_x86_64",
+ zip: "z3-${Z3_VER}-x64-win.zip",
+ files: [
+ "z3-${Z3_VER}-x64-win/bin/libz3.dll",
+ "z3-${Z3_VER}-x64-win/bin/libz3java.dll",
+
+ "z3-${Z3_VER}-x64-win/bin/msvcp140.dll",
+ "z3-${Z3_VER}-x64-win/bin/msvcp140_1.dll",
+ "z3-${Z3_VER}-x64-win/bin/msvcp140_2.dll",
+ "z3-${Z3_VER}-x64-win/bin/msvcp140_atomic_wait.dll",
+ "z3-${Z3_VER}-x64-win/bin/msvcp140_codecvt_ids.dll",
+ "z3-${Z3_VER}-x64-win/bin/vcomp140.dll",
+ "z3-${Z3_VER}-x64-win/bin/vcruntime140.dll",
+ "z3-${Z3_VER}-x64-win/bin/vcruntime140_1.dll"
+ ]
+ ]
+]
+
+// Note: jars vary among platform zips, but contain all the same file names
+// I'm presuming they vary only by java compiler and/or target JVM.
+ext.JAVA_JAR = [
+ zip: "z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}.zip",
+ files: [
+ "z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}/bin/com.microsoft.z3.jar",
+ ]
+]
+
+RelativePath computeInto(FileCopyDetails fcd) {
+ def dstSegs = fcd.relativePath.segments
+ def diff = dstSegs.length - fcd.relativeSourcePath.segments.length
+ RelativePath pre = new RelativePath(false, dstSegs.take(diff))
+ assert pre.append(fcd.relativeSourcePath).equals(fcd.relativePath)
+ return pre
+}
+
+CopySpec z3CopySpec = copySpec {
+ PLATFORM_BINDINGS.forEach { platform ->
+ File depsFile = file("${DEPS_DIR}/SymbolicSummaryZ3/${platform.zip}")
+ File binRepoFile = file("${BIN_REPO}/Ghidra/Debug/SymbolicSummaryZ3/${platform.zip}")
+ def z3ZipTree = depsFile.exists() ? zipTree(depsFile) : zipTree(binRepoFile)
+
+ from(z3ZipTree) {
+ include platform.files
+ eachFile { fcd ->
+ fcd.relativePath = computeInto(fcd).append(true, fcd.relativePath.lastName)
+ }
+ into("${platform.name}")
+ }
+ }
+}
+
+task z3DevUnpackPlatforms(type: Copy) {
+ description "Unpack Z3 archives for development use"
+ group = "Development Preparation"
+
+ with z3CopySpec
+ destinationDir file("build/os")
+}
+
+rootProject.assembleDistribution {
+ into(getZipPath(this.project) + "/os") {
+ with z3CopySpec
+ }
+ into(getZipPath(this.project)) {
+ from(this.project.file(".")) {
+ include("README.md")
+ }
+ }
+}
+
+rootProject.prepDev.dependsOn(z3DevUnpackPlatforms)
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/certification.manifest b/Ghidra/Debug/SymbolicSummaryZ3/certification.manifest
new file mode 100644
index 0000000000..97db3c3c58
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/certification.manifest
@@ -0,0 +1,4 @@
+##VERSION: 2.0
+##MODULE IP: JSch License
+Module.manifest||GHIDRA||||END|
+README.md||GHIDRA||||END|
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/AbstractSymZ3OffsetPcodeExecutorStatePiece.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/AbstractSymZ3OffsetPcodeExecutorStatePiece.java
new file mode 100644
index 0000000000..88a7fc6d7a
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/AbstractSymZ3OffsetPcodeExecutorStatePiece.java
@@ -0,0 +1,294 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import java.math.BigInteger;
+import java.util.*;
+
+import com.microsoft.z3.BitVecNum;
+import com.microsoft.z3.Context;
+
+import ghidra.pcode.exec.PcodeArithmetic;
+import ghidra.pcode.exec.PcodeExecutorStatePiece;
+import ghidra.program.model.address.AddressSpace;
+import ghidra.program.model.lang.Language;
+import ghidra.symz3.model.SymValueZ3;
+import ghidra.util.Msg;
+
+/**
+ * An abstract executor state piece which internally uses SymZ3Value to address contents
+ *
+ *
+ * This also provides an internal mechanism for breaking the piece down into the spaces defined by a
+ * language. It also provides for the special treatment of the {@code unique} space.
+ *
+ * @param the type of an execute state space, internally associated with an address space
+ */
+public abstract class AbstractSymZ3OffsetPcodeExecutorStatePiece
+ implements PcodeExecutorStatePiece {
+ /**
+ * A map of address spaces to objects which store or cache state for that space
+ *
+ * @param the type of object for each address space
+ */
+ public abstract static class AbstractSpaceMap {
+ protected final Map spaces = new HashMap<>();
+
+ public abstract S getForSpace(AddressSpace space, boolean toWrite);
+
+ public Collection values() {
+ return spaces.values();
+ }
+ }
+
+ /**
+ * Use this when each S contains the complete state for the address space
+ *
+ * @param the type of object for each address space
+ */
+ public abstract static class SimpleSpaceMap extends AbstractSpaceMap {
+ /**
+ * Construct a new space internally associated with the given address space
+ *
+ *
+ * As the name implies, this often simply wraps {@code S}'s constructor
+ *
+ * @param space the address space
+ * @return the new space
+ */
+ protected abstract S newSpace(AddressSpace space);
+
+ @Override
+ public S getForSpace(AddressSpace space, boolean toWrite) {
+ return spaces.computeIfAbsent(space, s -> newSpace(s));
+ }
+ }
+
+ /**
+ * Use this when each S is possibly a cache to some other state (backing) object
+ *
+ * @param the type of the object backing the cache for each address space
+ * @param the type of cache for each address space
+ */
+ public abstract static class CacheingSpaceMap extends AbstractSpaceMap {
+ /**
+ * Get the object backing the cache for the given address space
+ *
+ * @param space the space
+ * @return the backing object
+ */
+ protected abstract B getBacking(AddressSpace space);
+
+ /**
+ * Construct a new space internally associated with the given address space, having the
+ * given backing
+ *
+ *
+ * As the name implies, this often simply wraps {@code S}'s constructor
+ *
+ * @param space the address space
+ * @param backing the backing, if applicable. null for the unique space
+ * @return the new space
+ */
+ protected abstract S newSpace(AddressSpace space, B backing);
+
+ @Override
+ public S getForSpace(AddressSpace space, boolean toWrite) {
+ return spaces.computeIfAbsent(space,
+ s -> newSpace(s, s.isUniqueSpace() ? null : getBacking(s)));
+ }
+ }
+
+ protected final Language language;
+ protected final PcodeArithmetic addressArithmetic;
+ protected final PcodeArithmetic arithmetic;
+ protected final AddressSpace uniqueSpace;
+
+ /**
+ * Construct a state piece for the given language and arithmetic
+ *
+ * @param language the language (used for its memory model)
+ * @param addressArithmetic the arithmetic used for addresses
+ * @param arithmetic an arithmetic used to generate default values of {@code T}
+ */
+ public AbstractSymZ3OffsetPcodeExecutorStatePiece(Language language,
+ PcodeArithmetic addressArithmetic, PcodeArithmetic arithmetic) {
+ this.language = language;
+ this.addressArithmetic = addressArithmetic;
+ this.arithmetic = arithmetic;
+ uniqueSpace = language.getAddressFactory().getUniqueSpace();
+ }
+
+ @Override
+ public Language getLanguage() {
+ return language;
+ }
+
+ @Override
+ public PcodeArithmetic getAddressArithmetic() {
+ return addressArithmetic;
+ }
+
+ @Override
+ public PcodeArithmetic getArithmetic() {
+ return arithmetic;
+ }
+
+ /**
+ * Set a value in the unique space
+ *
+ *
+ * Some state pieces treat unique values in a way that merits a separate implementation. This
+ * permits the standard path to be overridden.
+ *
+ * @param offset the offset in unique space to store the value
+ * @param size the number of bytes to write (the size of the value)
+ * @param val the value to store
+ */
+ protected void setUnique(SymValueZ3 offset, int size, SymValueZ3 val) {
+ S s = getForSpace(uniqueSpace, true);
+ setInSpace(s, offset, size, val);
+ }
+
+ /**
+ * Get a value from the unique space
+ *
+ * Some state pieces treat unique values in a way that merits a separate implementation. This
+ * permits the standard path to be overridden.
+ *
+ * @param offset the offset in unique space to get the value
+ * @param size the number of bytes to read (the size of the value)
+ * @return the read value
+ */
+ protected SymValueZ3 getUnique(SymValueZ3 offset, int size) {
+ S s = getForSpace(uniqueSpace, false);
+ return getFromSpace(s, offset, size);
+ }
+
+ /**
+ * Get the internal space for the given address space
+ *
+ * @param space the address space
+ * @param toWrite in case internal spaces are generated lazily, this indicates the space must be
+ * present, because it is going to be written to.
+ * @return the space, or {@code null}
+ * @see AbstractSpaceMap
+ */
+ protected abstract S getForSpace(AddressSpace space, boolean toWrite);
+
+ /**
+ * Set a value in the given space
+ *
+ * @param space the address space
+ * @param offset the offset within the space
+ * @param size the number of bytes to write (the size of the value)
+ * @param val the value to store
+ */
+ protected abstract void setInSpace(S space, SymValueZ3 offset, int size, SymValueZ3 val);
+
+ /**
+ * Get a value from the given space
+ *
+ * @param space the address space
+ * @param offset the offset within the space
+ * @param size the number of bytes to read (the size of the value)
+ * @return the read value
+ */
+ protected abstract SymValueZ3 getFromSpace(S space, SymValueZ3 offset, int size);
+
+ /**
+ * In case spaces are generated lazily, and we're reading from a space that doesn't yet exist,
+ * "read" a default value.
+ *
+ *
+ * By default, the returned value is 0, which should be reasonable for all implementations.
+ *
+ * @param size the number of bytes to read (the size of the value)
+ * @return the default value
+ */
+ protected SymValueZ3 getFromNullSpace(int size) {
+ Msg.warn(this,
+ "getFromNullSpace is returning 0 but that might not be what we want for symz3");
+ return arithmetic.fromConst(0, size);
+ }
+
+ @Override
+ public void setVar(AddressSpace space, SymValueZ3 offset, int size, boolean quantize,
+ SymValueZ3 val) {
+
+ //Msg.info(this, "setVar for space: " + space + " offset: " + offset + " size: " + size + " val: " + val);
+ assert val != null;
+ assert offset != null;
+
+ //checkRange(space, offset, size);
+ /**
+ * FROM DAN: If you care to check that the offset makes sense within a given space, then fix
+ * this
+ *
+ * My suggestion: If offset is constant, convert to long and invoke checkRange. If not, just
+ * don't check. Note that the default implementation of setVar(space, long, size, quantize,
+ * val) will already call checkRange.
+ */
+ if (space.isConstantSpace()) {
+ throw new IllegalArgumentException("Cannot write to constant space");
+ }
+ if (space.isUniqueSpace()) {
+ setUnique(offset, size, val);
+ return;
+ }
+ S s = getForSpace(space, true);
+ //offset = quantizeOffset(space, offset);
+ /**
+ * FROM DAN: quantize probably doesn't make sense for you. You could check if concrete,
+ * convert to long, and quantize. You could also express the quantization symbolically, but
+ * it rarely comes up.
+ */
+ setInSpace(s, offset, size, val);
+ }
+
+ @Override
+ public SymValueZ3 getVar(AddressSpace space, SymValueZ3 offset, int size, boolean quantize,
+ Reason reason) {
+ //checkRange(space, offset, size);
+ //Msg.info(this, "getVar for space: " + space + " offset: " + offset + " size: " + size + " quantize: " + quantize);
+ if (space.isConstantSpace()) {
+ /**
+ * Totally clueless what "quantize" does and we are perhaps improperly ignoring it
+ *
+ * For architectures that can't address any arbitrary byte, it adjusts the offset and
+ * size to the floor addressable word. Not applicable to x86, so you can get away
+ * ignoring it there.
+ **/
+ //Msg.debug(this, "request of constant from offset: " + offset + " size: " + size);
+ try (Context ctx = new Context()) {
+ assert offset.getBitVecExpr(ctx).isNumeral();
+ BitVecNum bvn = (BitVecNum) offset.getBitVecExpr(ctx);
+ BigInteger b = bvn.getBigInteger();
+ return new SymValueZ3(ctx, ctx.mkBV(b.toString(), size * 8));
+ }
+ }
+ if (space.isUniqueSpace()) {
+ return getUnique(offset, size);
+ }
+ S s = getForSpace(space, false);
+ //Msg.info(this, "Now we likely have a space to get from: " + s);
+ if (s == null) {
+ return getFromNullSpace(size);
+ }
+ //offset = quantizeOffset(space, offset);
+ return getFromSpace(s, offset, size);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/AbstractSymZ3PcodeExecutorStatePiece.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/AbstractSymZ3PcodeExecutorStatePiece.java
new file mode 100644
index 0000000000..a2e7486277
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/AbstractSymZ3PcodeExecutorStatePiece.java
@@ -0,0 +1,194 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import java.io.PrintStream;
+import java.util.*;
+import java.util.stream.Stream;
+
+import com.microsoft.z3.Context;
+
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.pcode.emu.symz3.plain.SymZ3Preconditions;
+import ghidra.pcode.emu.symz3.plain.SymZ3Space;
+import ghidra.pcode.exec.ConcretionError;
+import ghidra.pcode.exec.PcodeArithmetic;
+import ghidra.pcode.exec.PcodeArithmetic.Purpose;
+import ghidra.program.model.address.Address;
+import ghidra.program.model.address.AddressSpace;
+import ghidra.program.model.lang.Language;
+import ghidra.program.model.listing.Instruction;
+import ghidra.program.model.mem.MemBuffer;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * An abstract SymZ3 state piece
+ *
+ *
+ * Because we want to reduce code repetition, we use the type hierarchy to increase the capabilities
+ * of the state piece as we progress from stand-alone to Debugger-integrated. The framework-provided
+ * class from which this derives, however, introduces the idea of a space map, whose values have
+ * type {@code }. We'll be using types derived from {@link SymZ3Space}, which is where all the
+ * storage logic is actually located. Because that logic is what we're actually extending with each
+ * more capable state piece, we have to ensure that type can be substituted. Thus, we have to create
+ * these abstract classes from which the actual state pieces are derived, leaving {@code }
+ * bounded, but unspecified.
+ *
+ * @param the type of spaces
+ */
+public abstract class AbstractSymZ3PcodeExecutorStatePiece
+ extends AbstractSymZ3OffsetPcodeExecutorStatePiece
+ implements InternalSymZ3RecordsPreconditions, InternalSymZ3RecordsExecution {
+
+ /**
+ * The map from address space to storage space
+ *
+ *
+ * While the concept is introduced in the super class, we're not required to actually use one.
+ * We just have to implement {@link #getForSpace(AddressSpace, boolean)}. Nevertheless, the
+ * provided map is probably the best way, so we'll follow the pattern.
+ */
+ protected final AbstractSpaceMap spaceMap = newSpaceMap(this.language);
+
+ protected final SymZ3Preconditions preconditions = new SymZ3Preconditions();
+ // LATER: These two are a recurring concern, and should be separated out
+ protected final List ops = new ArrayList();
+ protected final List instructions = new ArrayList();
+
+ /**
+ * Create a state piece
+ *
+ * @param language the emulator's language
+ * @param addressArithmetic the arithmetic for the address type
+ * @param arithmetic the arithmetic for the value type
+ */
+ public AbstractSymZ3PcodeExecutorStatePiece(Language language,
+ PcodeArithmetic addressArithmetic, PcodeArithmetic arithmetic) {
+ super(language, addressArithmetic, arithmetic);
+ }
+
+ /**
+ * Extension point: Create the actual space map
+ *
+ *
+ * This will need to be implemented by each state piece, i.e., non-abstract derivating class.
+ * The space map will provide instances of {@code }, which will provide the actual (extended)
+ * storage logic.
+ *
+ * @return the space map
+ */
+ protected abstract AbstractSpaceMap newSpaceMap(Language language);
+
+ @Override
+ public MemBuffer getConcreteBuffer(Address address, Purpose purpose) {
+ throw new ConcretionError("Cannot make Symbolic concrete", purpose);
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * Here, we just follow the pattern: delegate to the space map.
+ */
+ @Override
+ protected S getForSpace(AddressSpace space, boolean toWrite) {
+ return spaceMap.getForSpace(space, toWrite);
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * Because the super class places no bound on {@code }, we have to provide the delegation to
+ * the storage space.
+ */
+ @Override
+ protected void setInSpace(SymZ3Space space, SymValueZ3 offset, int size, SymValueZ3 val) {
+ space.set(offset, size, val);
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * Because the super class places no bound on {@code }, we have to provide the delegation to
+ * the storage space.
+ */
+ @Override
+ protected SymValueZ3 getFromSpace(SymZ3Space space, SymValueZ3 offset, int size) {
+ return space.get(offset, size);
+ }
+
+ public String printableSummary() {
+ StringBuilder result = new StringBuilder();
+ for (S space : spaceMap.values()) {
+ result.append(space.printableSummary());
+ }
+ result.append(this.preconditions.printableSummary());
+ return result.toString();
+ }
+
+ public void printSymbolicSummary(PrintStream out) {
+ out.println(this.printableSummary());
+ }
+
+ public Stream> streamValuations(Context ctx, Z3InfixPrinter z3p) {
+ return spaceMap.values().stream().flatMap(s -> s.streamValuations(ctx, z3p));
+ }
+
+ @Override
+ public void addPrecondition(String precondition) {
+ preconditions.addPrecondition(precondition);
+ }
+
+ @Override
+ public void addInstruction(SymZ3PcodeThread thread, Instruction instruction) {
+ instructions.add(new RecInstruction(instructions.size(), thread, instruction));
+ }
+
+ @Override
+ public List getInstructions() {
+ return Collections.unmodifiableList(instructions);
+ }
+
+ @Override
+ public void addOp(SymZ3PcodeThread thread, PcodeOp op) {
+ ops.add(new RecOp(ops.size(), thread, op));
+ }
+
+ @Override
+ public List getOps() {
+ return Collections.unmodifiableList(ops);
+ }
+
+ @Override
+ public List getPreconditions() {
+ return preconditions.getPreconditions();
+ }
+
+ @Override
+ public void clear() {
+ spaceMap.spaces.clear();
+ preconditions.clear();
+ ops.clear();
+ instructions.clear();
+ }
+
+ protected Stream streamPreconditions(Context ctx, Z3InfixPrinter z3p) {
+ return preconditions.streamPreconditions(ctx, z3p);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/InternalSymZ3RecordsExecution.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/InternalSymZ3RecordsExecution.java
new file mode 100644
index 0000000000..70e7b01690
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/InternalSymZ3RecordsExecution.java
@@ -0,0 +1,26 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import ghidra.program.model.listing.Instruction;
+import ghidra.program.model.pcode.PcodeOp;
+
+public interface InternalSymZ3RecordsExecution extends SymZ3RecordsExecution {
+ public void addInstruction(SymZ3PcodeThread thread, Instruction inst);
+
+ public void addOp(SymZ3PcodeThread thread, PcodeOp op);
+
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/InternalSymZ3RecordsPreconditions.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/InternalSymZ3RecordsPreconditions.java
new file mode 100644
index 0000000000..a2cde905df
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/InternalSymZ3RecordsPreconditions.java
@@ -0,0 +1,25 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+public interface InternalSymZ3RecordsPreconditions extends SymZ3RecordsPreconditions {
+ /**
+ * Record a precondition
+ *
+ * @param precondition the serialized Z3 bool expression
+ */
+ public void addPrecondition(String precondition);
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3.java
new file mode 100644
index 0000000000..d2a4d48ffe
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3.java
@@ -0,0 +1,33 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import ghidra.framework.*;
+
+public class SymZ3 {
+ public static void loadZ3Libs() {
+ // Load the libraries using a custom search path before the system tries
+ String ext = Platform.CURRENT_PLATFORM.getLibraryExtension();
+ try {
+ System.load(Application.getOSFile("libz3" + ext).getPath());
+ System.load(Application.getOSFile("libz3java" + ext).getPath());
+ }
+ catch (OSFileNotFoundException e) {
+ throw new UnsatisfiedLinkError("Z3 libs not found: " + e);
+ }
+ System.setProperty("z3.skipLibraryLoad", Boolean.toString(true));
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3MemoryMap.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3MemoryMap.java
new file mode 100644
index 0000000000..57a76b6c8d
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3MemoryMap.java
@@ -0,0 +1,317 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import java.util.*;
+import java.util.Map.Entry;
+import java.util.stream.Stream;
+
+import com.microsoft.z3.*;
+
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.pcode.emu.symz3.lib.Z3MemoryWitness;
+import ghidra.pcode.emu.symz3.lib.Z3MemoryWitness.WitnessType;
+import ghidra.program.model.lang.Language;
+import ghidra.symz3.model.SymValueZ3;
+import ghidra.util.Msg;
+
+/**
+ * A class that can store SymZ3Values in memory
+ *
+ *
+ * NOTE: DELIBERATELY NO KNOWLEDGE OF SPACES, Languages, or "get" and "set"
+ *
+ * The core idea is that quite often the code we are summarizing will load from memory arbitrary
+ * values. We want to allow those values to exist as a unit. E.g., if the user loads 64 unknown bits
+ * from an address 0xdeadbeef, we want the name of those bits to be "MEM[0xdeadbeef]:64" -- instead
+ * of for example, a concat of each unknown byte. However, the 64 bit value might later be sliced
+ * and diced. If we store a 64 bit symbolic value "RBX" into MEM[0xdeadbeef] and then later load
+ * just an interior byte, we want to detect this. Of course if we load MEM[RCX] and we don't know
+ * what RCX is, the value simply has to stay symbolic.
+ *
+ * In terms of storage, we have two options:
+ *
+ * first, we could have our "memvals" map always store values that are bytes. If you store a 64 bit
+ * value to MEM[RAX] we would create 8 entries in our map, for MEM[RAX], MEM[RAX+1], etc.
+ *
+ * second, we could be willing to store arbitrary sizes. This will require more searching and would
+ * be problematic when we say wrote to MEM[RAX+3] having previously stored a large value at
+ * MEM[RAX].
+ *
+ * For now, we went with option 2 but then didn't implement anything tricky, so we have bugs. If we
+ * move to option 1, the usecase we might worry about is something like: "{@code MEM[RAX] = RBX}"
+ * how will we see this summary? We would write:
+ *
+ *
+ * MEM[RAX]:8 = extract(RBX,?,?)
+ * MEM[RAX+1]:8 = extract(RBX,?,?)
+ *
+ *
+ * Note than endness would come into play, whereas right now we also sidestep this issue. Probably
+ * should see if I get a simple test to pass and the simplification to work, before we fully commit
+ * to option 1.
+ */
+public class SymZ3MemoryMap {
+ // TODO ... encapsulate traversal of memvals so it can become private
+ public Map memvals;
+ private List witnesses;
+
+ private Language language;
+
+ private static final boolean USE_BYTE_MODEL = true;
+
+ public static FuncDecl buildLoad(Context ctx, int addressSize, int dataSize) {
+ BitVecSort addressSort = ctx.mkBitVecSort(addressSize);
+ BitVecSort dataSort = ctx.mkBitVecSort(dataSize);
+ return ctx.mkFuncDecl("load_" + addressSize + "_" + dataSize, addressSort, dataSort);
+ }
+
+ public SymZ3MemoryMap(Language language) {
+ memvals = new HashMap();
+ this.language = language;
+ witnesses = new ArrayList();
+ }
+
+ protected Entry valuationForMemval(Context ctx, Z3InfixPrinter z3p,
+ Entry entry) {
+ String address = entry.getKey();
+ SymValueZ3 vv = entry.getValue();
+ BitVecExpr addressExpr = SymValueZ3.deserializeBitVecExpr(ctx, address);
+ if (vv == null) {
+ return Map.entry("MEM " + z3p.infixWithBrackets(addressExpr), "null");
+ }
+ BitVecExpr v = vv.getBitVecExpr(ctx);
+ if (v == null) {
+ return Map.entry("MEM " + z3p.infixWithBrackets(addressExpr), "null (?) " + vv);
+ }
+ v = (BitVecExpr) v.simplify();
+ int bitSize = v.getSortSize();
+ String sizeString = ":" + Integer.toString(bitSize);
+ return Map.entry("MEM " + z3p.infixWithBrackets(addressExpr) + sizeString,
+ z3p.infixUnsigned(v));
+ }
+
+ protected Entry valuationForWitness(Context ctx, Z3InfixPrinter z3p,
+ Set reported, Z3MemoryWitness w) {
+ BitVecExpr addressExpr = w.address().getBitVecExpr(ctx);
+ if (!reported.add(addressExpr)) {
+ return null;
+ }
+ SymValueZ3 vv = load(w.address(), w.bytesMoved(), false);
+ BitVecExpr v = vv.getBitVecExpr(ctx);
+ if (v == null) {
+ return Map.entry("MEM " + z3p.infixWithBrackets(addressExpr), "null (?)");
+ }
+ v = (BitVecExpr) v.simplify();
+ int bitSize = v.getSortSize();
+ String sizeString = ":" + Integer.toString(bitSize);
+ return Map.entry("MEM " + z3p.infixWithBrackets(addressExpr) + sizeString,
+ z3p.infixUnsigned(v));
+ }
+
+ public String printableSummary() {
+ StringBuilder result = new StringBuilder();
+ try (Context ctx = new Context()) {
+ Z3InfixPrinter z3p = new Z3InfixPrinter(ctx);
+ for (Map.Entry entry : memvals.entrySet()) {
+ String address = entry.getKey();
+ SymValueZ3 vv = memvals.get(address);
+ BitVecExpr addressExpr = SymValueZ3.deserializeBitVecExpr(ctx, address);
+ if (vv == null) {
+ result.append("MEM " + z3p.infixWithBrackets(addressExpr) + " is null");
+ result.append(System.lineSeparator());
+ }
+ else {
+ BitVecExpr v = vv.getBitVecExpr(ctx);
+ if (v == null) {
+ result.append("MEM " + z3p.infixWithBrackets(addressExpr) +
+ " is null (?)" + memvals.get(address));
+ result.append(System.lineSeparator());
+ }
+ else {
+ v = (BitVecExpr) v.simplify();
+ int bitSize = v.getSortSize();
+ String sizeString = ":" + Integer.toString(bitSize);
+ result.append("MEM " + z3p.infixWithBrackets(addressExpr) + sizeString +
+ " = " + z3p.infixUnsigned(v));
+ result.append(System.lineSeparator());
+ }
+ }
+ }
+
+ ArrayList reported = new ArrayList();
+ for (Z3MemoryWitness w : witnesses) {
+ BitVecExpr addressExpr = w.address().getBitVecExpr(ctx);
+ if (reported.contains(addressExpr)) {
+ continue;
+ }
+ reported.add(addressExpr);
+ SymValueZ3 value = load(w.address(), w.bytesMoved(), false);
+ BitVecExpr vexpr = value.getBitVecExpr(ctx);
+ if (vexpr == null) {
+ result.append("MEM " + z3p.infixWithBrackets(addressExpr) + " is null (?)");
+ result.append(System.lineSeparator());
+ }
+ else {
+ BitVecExpr v = (BitVecExpr) vexpr.simplify();
+ int bitSize = v.getSortSize();
+ String sizeString = ":" + Integer.toString(bitSize);
+ result.append("MEM " + z3p.infixWithBrackets(addressExpr) + sizeString +
+ " = " + z3p.infixUnsigned(v));
+ result.append(System.lineSeparator());
+ }
+ }
+ }
+ return result.toString();
+ }
+
+ public Stream> streamValuations(Context ctx, Z3InfixPrinter z3p) {
+ Stream> forMemVals = memvals.entrySet().stream().map(entry -> {
+ return valuationForMemval(ctx, z3p, entry);
+ });
+ Set reported = new HashSet<>();
+ Stream> forWitnesses = witnesses.stream().mapMulti((w, mapper) -> {
+ Entry result = valuationForWitness(ctx, z3p, reported, w);
+ if (result != null) {
+ mapper.accept(result);
+ }
+ });
+ return Stream.concat(forMemVals, forWitnesses);
+ }
+
+ public SymValueZ3 load(SymValueZ3 offset, int size, boolean addWitness) {
+ try (Context ctx = new Context()) {
+ if (addWitness) {
+ witnesses.add(new Z3MemoryWitness(offset, size, WitnessType.LOAD));
+ }
+ BitVecExpr address = offset.getBitVecExpr(ctx);
+
+ if (!USE_BYTE_MODEL) {
+ // this is the primary disadvantage of the non-byte based model. on a load, the value we need to build
+ // might not simply be stored... it could even be in other locations in the store... so this is really
+ // difficult to get right, but super easy if you are willing to not care...
+ if (memvals.containsKey(offset.bitVecExprString)) {
+ // TODO Ignoring the SIZE... that might be really important... TO DO
+ SymValueZ3 value = memvals.get(offset.bitVecExprString);
+ assert value != null;
+ BitVecExpr valueb = value.getBitVecExpr(ctx);
+ if (valueb.getSortSize() != size * 8) {
+ // could do the stupid thing and just return a symbolic value...
+ Msg.error(this, "Performed a load of " + size +
+ " bytes but stored value was of size: " + valueb.getSortSize());
+ throw new AssertionError(
+ "size based memory model needs more code to fetch a portion of what was written");
+ }
+ return value;
+ }
+ // this symbolic load might totally miss out on the fact that we actually know more
+ FuncDecl f = buildLoad(ctx, address.getSortSize(), size * 8);
+ BitVecExpr expression = (BitVecExpr) ctx.mkApp(f, address);
+
+ return new SymValueZ3(ctx, expression);
+
+ }
+ // essentially, we load each byte separately ... each byte may or may not have a known value.
+ // we have to assume that whatever our offset is, when we add one to it, the result is how it was stored.
+ // that might not technically be true. Ideally there would be some sort of normalization.
+ // NOTE: CURRENTLY IGNORING ENDNESS
+ List result_pieces = new ArrayList();
+ BitVecExpr one = ctx.mkBV(1, address.getSortSize());
+ BitVecExpr byteAddress = address;
+ for (int byte_offset = 0; byte_offset < size; byte_offset = byte_offset + 1) {
+ if (byte_offset > 0) {
+ byteAddress = ctx.mkBVAdd(byteAddress, one);
+ }
+ byteAddress = (BitVecExpr) byteAddress.simplify(); // a form of normalization
+ String byteAddressAsString = SymValueZ3.serialize(ctx, byteAddress);
+ if (memvals.containsKey(byteAddressAsString)) {
+ result_pieces.add(memvals.get(byteAddressAsString).getBitVecExpr(ctx));
+ }
+ else {
+ FuncDecl f = buildLoad(ctx, address.getSortSize(), 8);
+ BitVecExpr expression = (BitVecExpr) ctx.mkApp(f, byteAddress);
+ result_pieces.add(expression);
+ }
+ }
+ BitVecExpr result = null;
+ // for the other ENDIAN, don't reverse
+ if (!language.isBigEndian()) {
+ Collections.reverse(result_pieces);
+ }
+ for (BitVecExpr piece : result_pieces) {
+ if (result == null) {
+ result = piece;
+ }
+ else {
+ result = ctx.mkConcat(result, piece);
+ }
+ }
+ return new SymValueZ3(ctx, result);
+ }
+ }
+
+ public void store(SymValueZ3 offset, int size, SymValueZ3 val) {
+ witnesses.add(new Z3MemoryWitness(offset, size, WitnessType.STORE));
+ try (Context ctx = new Context()) {
+ BitVecExpr bval = val.getBitVecExpr(ctx);
+ BitVecExpr address = offset.getBitVecExpr(ctx);
+ assert bval.getSortSize() == size * 8;
+ if (!USE_BYTE_MODEL) {
+ // this is the primary advantage of the non-byte based model, storage is super easy
+ Msg.debug(this, "set memory location " + address + " size " + size + " to " + val);
+ memvals.put(offset.bitVecExprString, val);
+ }
+ else {
+ // for the byte-based model, we simply must store each byte separately.
+ // NOTE: CURRENTLY IGNORING ENDNeSS
+ BitVecExpr one = ctx.mkBV(1, address.getSortSize());
+ BitVecExpr byteAddress = address;
+ for (int byte_offset = 0; byte_offset < size; byte_offset = byte_offset + 1) {
+ if (byte_offset > 0) {
+ byteAddress = ctx.mkBVAdd(byteAddress, one);
+ }
+ byteAddress = (BitVecExpr) byteAddress.simplify(); // a form of normalization
+ String byteAddressAsString = SymValueZ3.serialize(ctx, byteAddress);
+
+ int bit_size = size * 8;
+ int high;
+ int low;
+ if (language.isBigEndian()) {
+ high = bit_size - (byte_offset * 8) - 1;
+ low = bit_size - ((byte_offset + 1) * 8);
+ }
+ else {
+ high = byte_offset * 8 + 7;
+ low = byte_offset * 8;
+ }
+ BitVecExpr valportion = ctx.mkExtract(high, low, bval);
+ memvals.put(byteAddressAsString, new SymValueZ3(ctx, valportion));
+ }
+ }
+ }
+ }
+
+ public boolean hasValueFor(SymValueZ3 offset, int size) {
+ // TODO need to think about the size
+ //BitVecExpr address = offset.getBitVecExpr();
+ if (memvals.containsKey(offset.bitVecExprString)) {
+ //SymValueZ3 result = memvals.get(address);
+ // TODO could assert size is what we request??
+ return true;
+ }
+ return false;
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PairedPcodeExecutorState.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PairedPcodeExecutorState.java
new file mode 100644
index 0000000000..8a4d77ed85
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PairedPcodeExecutorState.java
@@ -0,0 +1,31 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import org.apache.commons.lang3.tuple.Pair;
+
+import ghidra.pcode.emu.symz3.plain.SymZ3Space;
+import ghidra.pcode.exec.PcodeExecutorState;
+import ghidra.pcode.exec.PcodeExecutorStatePiece;
+import ghidra.symz3.model.SymValueZ3;
+
+public interface SymZ3PairedPcodeExecutorState
+ extends PcodeExecutorState> {
+
+ PcodeExecutorStatePiece getLeft();
+
+ AbstractSymZ3PcodeExecutorStatePiece getRight();
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PartsFactory.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PartsFactory.java
new file mode 100644
index 0000000000..980d3995f8
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PartsFactory.java
@@ -0,0 +1,183 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import org.apache.commons.lang3.tuple.Pair;
+
+import ghidra.app.plugin.core.debug.service.emulation.RWTargetMemoryPcodeExecutorStatePiece;
+import ghidra.app.plugin.core.debug.service.emulation.RWTargetRegistersPcodeExecutorStatePiece;
+import ghidra.pcode.emu.*;
+import ghidra.pcode.emu.DefaultPcodeThread.PcodeThreadExecutor;
+import ghidra.pcode.emu.auxiliary.AuxPcodeEmulator;
+import ghidra.pcode.emu.symz3.plain.SymZ3PcodeExecutorState;
+import ghidra.pcode.emu.symz3.trace.SymZ3TracePcodeExecutorState;
+import ghidra.pcode.exec.*;
+import ghidra.pcode.exec.debug.auxiliary.AuxDebuggerEmulatorPartsFactory;
+import ghidra.pcode.exec.debug.auxiliary.AuxDebuggerPcodeEmulator;
+import ghidra.pcode.exec.trace.BytesTracePcodeExecutorStatePiece;
+import ghidra.pcode.exec.trace.TracePcodeExecutorState;
+import ghidra.pcode.exec.trace.auxiliary.AuxTracePcodeEmulator;
+import ghidra.program.model.lang.Language;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * The parts factory for creating emulators with symbolic summaries using Z3
+ *
+ *
+ * This is probably the most straightforward means of implementing a concrete-plus-auxiliary
+ * emulator in Ghidra. For our case, the auxiliary piece is the {@link SymValueZ3}. For an overview
+ * of the parts of a p-code emulator, see {@link PcodeEmulator}.
+ *
+ *
+ * As recommended by the documentation, we've implemented the factory as a singleton. As presented
+ * in the source, we'll visit each component in this order:
+ *
+ * - P-code Arithmetic: {@link SymZ3PcodeArithmetic}
+ * - Userop Library: {@link SymZ3PcodeUseropLibrary}
+ * - P-code Executor: {@link SymZ3PcodeThreadExecutor}
+ * - Machine State
+ *
+ * - Stand alone: {@link SymZ3PcodeExecutorState}
+ * - Trace integrated: {@link SymZ3TracePcodeExecutorState}
+ * - Debugger integrated: Not applicable. Uses trace integration only.
+ *
+ *
+ *
+ *
+ * If you're following from the {@link ghidra.symz3} package documentation, you'll want to return to
+ * {@link ghidra.pcode.emu.symz3.plain} before you examine the trace-integrated state. Similarly,
+ * you'll want to return to {@link ghidra.pcode.emu.symz3.trace} before you examine the
+ * Debugger-integrated state.
+ */
+public enum SymZ3PartsFactory implements AuxDebuggerEmulatorPartsFactory {
+ /** This singleton factory instance */
+ INSTANCE;
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * Here we simply return the arithmetic for symbolic values for the emulator's language.
+ */
+ @Override
+ public PcodeArithmetic getArithmetic(Language language) {
+ return SymZ3PcodeArithmetic.forLanguage(language);
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * We introduce two userops for obtaining symbolic values. Aside from initializing a trace
+ * (assuming a trace-integrated emulator), or writing directly to the state in the script, this
+ * library will allow clients to quickly initialize symbolic values in the machine. Furthermore,
+ * this can permit the placement of symbolic values in intermediate states of the machine during
+ * its execution. We construct and return the library here.
+ */
+ @Override
+ public PcodeUseropLibrary> createSharedUseropLibrary(
+ AuxPcodeEmulator emulator) {
+ return new SymZ3PcodeUseropLibrary();
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * We have no thread-specific userops to add, which means we also have no need to stubs, so here
+ * we just return the empty library.
+ */
+ @Override
+ public PcodeUseropLibrary> createLocalUseropStub(
+ AuxPcodeEmulator emulator) {
+ return PcodeUseropLibrary.nil();
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * We have no thread-specific userops to add, so here we just return the empty library.
+ */
+ @Override
+ public PcodeUseropLibrary> createLocalUseropLibrary(
+ AuxPcodeEmulator emulator, PcodeThread> thread) {
+ return PcodeUseropLibrary.nil();
+ }
+
+ @Override
+ public PcodeThread> createThread(AuxPcodeEmulator emulator,
+ String name) {
+ return new SymZ3PcodeThread(name, emulator);
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * We'd like to instrument conditional branches to record preconditions, so we'll need a custom
+ * executor. We construct it here.
+ */
+ @Override
+ public PcodeThreadExecutor> createExecutor(
+ AuxPcodeEmulator emulator,
+ DefaultPcodeThread> thread) {
+ return new SymZ3PcodeThreadExecutor((SymZ3PcodeThread) thread);
+ }
+
+ @Override
+ public PcodeExecutorState> createSharedState(
+ AuxPcodeEmulator emulator, BytesPcodeExecutorStatePiece concrete) {
+ return new SymZ3PcodeExecutorState(emulator.getLanguage(), concrete);
+ }
+
+ @Override
+ public PcodeExecutorState> createLocalState(
+ AuxPcodeEmulator emulator, PcodeThread> thread,
+ BytesPcodeExecutorStatePiece concrete) {
+ return new SymZ3PcodeExecutorState(emulator.getLanguage(), concrete);
+ }
+
+ @Override
+ public TracePcodeExecutorState> createTraceSharedState(
+ AuxTracePcodeEmulator emulator,
+ BytesTracePcodeExecutorStatePiece concrete) {
+ return new SymZ3TracePcodeExecutorState(concrete);
+ }
+
+ @Override
+ public TracePcodeExecutorState> createTraceLocalState(
+ AuxTracePcodeEmulator emulator,
+ PcodeThread> emuThread,
+ BytesTracePcodeExecutorStatePiece concrete) {
+ return new SymZ3TracePcodeExecutorState(concrete);
+ }
+
+ @Override
+ public TracePcodeExecutorState> createDebuggerSharedState(
+ AuxDebuggerPcodeEmulator emulator,
+ RWTargetMemoryPcodeExecutorStatePiece concrete) {
+ return new SymZ3TracePcodeExecutorState(concrete);
+ }
+
+ @Override
+ public TracePcodeExecutorState> createDebuggerLocalState(
+ AuxDebuggerPcodeEmulator emulator,
+ PcodeThread> emuThread,
+ RWTargetRegistersPcodeExecutorStatePiece concrete) {
+ return new SymZ3TracePcodeExecutorState(concrete);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeArithmetic.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeArithmetic.java
new file mode 100644
index 0000000000..9253dbb49d
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeArithmetic.java
@@ -0,0 +1,266 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import java.math.BigInteger;
+import java.util.Objects;
+
+import com.microsoft.z3.*;
+
+import ghidra.pcode.exec.ConcretionError;
+import ghidra.pcode.exec.PcodeArithmetic;
+import ghidra.pcode.utils.Utils;
+import ghidra.program.model.address.AddressSpace;
+import ghidra.program.model.lang.Endian;
+import ghidra.program.model.lang.Language;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.symz3.model.SymValueZ3;
+import ghidra.util.Msg;
+
+public enum SymZ3PcodeArithmetic implements PcodeArithmetic {
+
+ /** The instance for big-endian languages */
+ BIG_ENDIAN(Endian.BIG),
+ /** The instance for little-endian languages */
+ LITTLE_ENDIAN(Endian.LITTLE);
+
+ static {
+ SymZ3.loadZ3Libs();
+ Msg.info(SymZ3PcodeArithmetic.class,
+ "Z3 Version: " + com.microsoft.z3.Version.getFullVersion());
+ }
+
+ /**
+ * Get the arithmetic for the given endianness
+ *
+ *
+ * This method is provided since clients of this class may expect it, as they would for any
+ * realization of {@link PcodeArithmetic}.
+ *
+ * @param bigEndian true for big endian, false for little
+ * @return the arithmetic
+ */
+ public static SymZ3PcodeArithmetic forEndian(boolean bigEndian) {
+ return bigEndian ? BIG_ENDIAN : LITTLE_ENDIAN;
+ }
+
+ /**
+ * Get the symbolic arithmetic for the given language
+ *
+ *
+ * This method is provided since clients of this class may expect it, as they would for any
+ * realization of {@link PcodeArithmetic}.
+ *
+ * @param language the language
+ * @return the arithmetic
+ */
+ public static SymZ3PcodeArithmetic forLanguage(Language language) {
+ return forEndian(language.isBigEndian());
+ }
+
+ private final Endian endian;
+
+ private SymZ3PcodeArithmetic(Endian endian) {
+ this.endian = endian;
+ }
+
+ @Override
+ public Endian getEndian() {
+ return endian;
+ }
+
+ public static BitVecNum zero(Context ctx) {
+ return ctx.mkBV(0, 8);
+ }
+
+ public static BitVecNum one(Context ctx) {
+ return ctx.mkBV(1, 8);
+ }
+
+ public static BitVecNum isNumeral(BitVecExpr eb, Purpose purpose) {
+ if (!eb.isNumeral()) {
+ throw new ConcretionError("Not a numeral", purpose);
+ }
+ return (BitVecNum) eb;
+ }
+
+ public static int isInt(BitVecExpr eb, Purpose purpose) {
+ return isNumeral(eb, purpose).getInt();
+ }
+
+ public static long isLong(BitVecExpr eb, Purpose purpose) {
+ return isNumeral(eb, purpose).getLong();
+ }
+
+ @Override
+ public long toLong(SymValueZ3 value, Purpose purpose) {
+ try (Context ctx = new Context()) {
+ return isLong(value.getBitVecExpr(ctx), purpose);
+ }
+ }
+
+ public static BigInteger isBigInteger(BitVecExpr eb, Purpose purpose) {
+ return isNumeral(eb, purpose).getBigInteger();
+ }
+
+ @Override
+ public BigInteger toBigInteger(SymValueZ3 value, Purpose purpose) {
+ try (Context ctx = new Context()) {
+ return isBigInteger(value.getBitVecExpr(ctx), purpose);
+ }
+ }
+
+ public static byte[] isConcrete(BitVecExpr eb, Purpose purpose, Endian endian) {
+ BigInteger bi = isBigInteger(eb, purpose);
+ return Utils.bigIntegerToBytes(bi, eb.getSortSize() * 8, endian.isBigEndian());
+ }
+
+ @Override
+ public byte[] toConcrete(SymValueZ3 value, Purpose purpose) {
+ try (Context ctx = new Context()) {
+ return isConcrete(value.getBitVecExpr(ctx), purpose, endian);
+ }
+ }
+
+ @Override
+ public boolean isTrue(SymValueZ3 cond, Purpose purpose) {
+ try (Context ctx = new Context()) {
+ if (cond.hasBoolExpr()) {
+ BoolExpr boolExpr = cond.getBoolExpr(ctx);
+ if (boolExpr.isTrue()) {
+ return true;
+ }
+ if (boolExpr.isFalse()) {
+ return false;
+ }
+ throw new ConcretionError("Condition is not constant", purpose);
+ }
+ BitVecExpr bvExpr = cond.getBitVecExpr(ctx);
+ if (bvExpr.isBVBitOne()) {
+ return true;
+ }
+ if (bvExpr.isBVBitZero()) {
+ return false;
+ }
+ throw new ConcretionError("Condition is not constant", purpose);
+ }
+ }
+
+ @Override
+ public SymValueZ3 unaryOp(int opcode, int sizeout, int sizein1, SymValueZ3 in1) {
+ Objects.requireNonNull(in1);
+ try (Context ctx = new Context()) {
+ return switch (opcode) {
+ case PcodeOp.COPY -> in1;
+ case PcodeOp.INT_ZEXT -> in1.intZExt(ctx, sizeout);
+ case PcodeOp.INT_SEXT -> in1.intSExt(ctx, sizeout);
+ case PcodeOp.BOOL_NEGATE -> in1.boolNegate(ctx);
+ case PcodeOp.POPCOUNT -> in1.popcount(ctx, sizeout);
+ default -> throw new AssertionError(
+ "need to implement unary op: " + PcodeOp.getMnemonic(opcode));
+ };
+ } // ctx
+ }
+
+ @Override
+ public SymValueZ3 binaryOp(int opcode, int sizeout, int sizein1, SymValueZ3 in1, int sizein2,
+ SymValueZ3 in2) {
+ Objects.requireNonNull(in1);
+ Objects.requireNonNull(in2);
+ try (Context ctx = new Context()) {
+ return switch (opcode) {
+ case PcodeOp.INT_EQUAL -> in1.intEqual(ctx, in2);
+ case PcodeOp.INT_NOTEQUAL -> in1.intNotEqual(ctx, in2);
+ case PcodeOp.INT_SLESS -> in1.intSLess(ctx, in2);
+ case PcodeOp.INT_SLESSEQUAL -> in1.intSLessEqual(ctx, in2);
+ case PcodeOp.INT_LESS -> in1.intLess(ctx, in2);
+ case PcodeOp.INT_LESSEQUAL -> in1.intLessEqual(ctx, in2);
+
+ case PcodeOp.INT_ADD -> in1.intAdd(ctx, in2);
+ case PcodeOp.INT_SUB -> in1.intSub(ctx, in2);
+ case PcodeOp.INT_CARRY -> in1.intCarry(ctx, in2);
+ case PcodeOp.INT_SCARRY -> in1.intSCarry(ctx, in2);
+ case PcodeOp.INT_SBORROW -> in1.intSBorrow(ctx, in2);
+
+ case PcodeOp.INT_XOR -> in1.intXor(ctx, in2);
+ case PcodeOp.INT_AND -> in1.intAnd(ctx, in2);
+ case PcodeOp.INT_OR -> in1.intOr(ctx, in2);
+
+ case PcodeOp.INT_LEFT -> in1.intLeft(ctx, in2);
+ case PcodeOp.INT_RIGHT -> in1.intRight(ctx, in2);
+ case PcodeOp.INT_SRIGHT -> in1.intSRight(ctx, in2);
+
+ case PcodeOp.INT_MULT -> in1.intMult(ctx, in2);
+ case PcodeOp.INT_DIV -> in1.intDiv(ctx, in2);
+ case PcodeOp.INT_SDIV -> in1.intSDiv(ctx, in2);
+
+ case PcodeOp.BOOL_XOR -> in1.boolXor(ctx, in2);
+ case PcodeOp.BOOL_AND -> in1.boolAnd(ctx, in2);
+ case PcodeOp.BOOL_OR -> in1.boolOr(ctx, in2);
+
+ // NOTE: Seeing these in low p-code would be unusual
+ case PcodeOp.PIECE -> in1.piece(ctx, in2);
+ case PcodeOp.SUBPIECE -> in1.subpiece(ctx, sizeout, in2);
+ default -> throw new AssertionError(
+ "need to implement binary op: " + PcodeOp.getMnemonic(opcode));
+ };
+ } // ctx
+ }
+
+ @Override
+ public SymValueZ3 fromConst(long value, int size) {
+ try (Context ctx = new Context()) {
+ return new SymValueZ3(ctx, ctx.mkBV(value, size * 8));
+ }
+ }
+
+ @Override
+ public SymValueZ3 fromConst(BigInteger value, int size, boolean isContextreg) {
+ try (Context ctx = new Context()) {
+ return new SymValueZ3(ctx, ctx.mkBV(value.toString(), size * 8));
+ }
+ }
+
+ @Override
+ public SymValueZ3 fromConst(BigInteger value, int size) {
+ return fromConst(value, size, false);
+ }
+
+ @Override
+ public SymValueZ3 fromConst(byte[] value) {
+ return fromConst(Utils.bytesToBigInteger(value, value.length, endian.isBigEndian(), false),
+ value.length);
+ }
+
+ @Override
+ public long sizeOf(SymValueZ3 value) {
+ try (Context ctx = new Context()) {
+ return value.getBitVecExpr(ctx).getSortSize() / 8;
+ }
+ }
+
+ @Override
+ public SymValueZ3 modBeforeStore(int sizeinOffset, AddressSpace space, SymValueZ3 inOffset,
+ int sizeinValue, SymValueZ3 inValue) {
+ return inValue;
+ }
+
+ @Override
+ public SymValueZ3 modAfterLoad(int sizeinOffset, AddressSpace space, SymValueZ3 inOffset,
+ int sizeinValue, SymValueZ3 inValue) {
+ return inValue;
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeEmulatorTrait.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeEmulatorTrait.java
new file mode 100644
index 0000000000..e0ab9624c5
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeEmulatorTrait.java
@@ -0,0 +1,135 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import java.io.PrintStream;
+import java.util.Collection;
+import java.util.List;
+import java.util.Map.Entry;
+import java.util.stream.Collectors;
+import java.util.stream.Stream;
+
+import org.apache.commons.lang3.tuple.Pair;
+
+import com.microsoft.z3.Context;
+
+import ghidra.app.plugin.processors.sleigh.template.OpTpl;
+import ghidra.app.util.pcode.StringPcodeFormatter;
+import ghidra.pcode.emu.PcodeMachine;
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.pcode.emu.symz3.plain.SymZ3Space;
+import ghidra.symz3.model.SymValueZ3;
+
+public interface SymZ3PcodeEmulatorTrait
+ extends PcodeMachine>, SymZ3RecordsExecution {
+
+ @Override
+ SymZ3PcodeThread newThread();
+
+ @Override
+ SymZ3PcodeThread newThread(String name);
+
+ @Override
+ Collection getAllThreads();
+
+ @Override
+ SymZ3PairedPcodeExecutorState getSharedState();
+
+ default AbstractSymZ3PcodeExecutorStatePiece getSharedSymbolicState() {
+ return getSharedState().getRight();
+ }
+
+ @Override
+ default List getInstructions() {
+ return getSharedSymbolicState().getInstructions();
+ }
+
+ @Override
+ default List getOps() {
+ return getSharedSymbolicState().getOps();
+ }
+
+ default String printableSummary() {
+ StringBuilder result = new StringBuilder();
+ for (SymZ3PcodeThread thread : this.getAllThreads()) {
+ result.append(thread.getLocalSymbolicState().printableSummary());
+ result.append(System.lineSeparator());
+ }
+ result.append(getSharedSymbolicState().printableSummary());
+ result.append(System.lineSeparator());
+ return result.toString();
+ }
+
+ default void printSymbolicSummary(PrintStream out) {
+ out.println(this.printableSummary());
+ }
+
+ default String formatOps() {
+ List ops = getOps();
+ StringPcodeFormatter formatter = new StringPcodeFormatter() {
+ int i = 0;
+
+ @Override
+ protected FormatResult formatOpTemplate(ToStringAppender appender, OpTpl op) {
+ appender.appendLabel("[%s] ".formatted(ops.get(i++).thread().getName()));
+ return super.formatOpTemplate(appender, op);
+ }
+ };
+ return formatter.formatOps(getLanguage(), ops.stream().map(RecOp::op).toList());
+ }
+
+ default void printOps(PrintStream out) {
+ out.println(formatOps());
+ }
+
+ default String formatInstructions() {
+ return getInstructions().stream()
+ .map(RecInstruction::toString)
+ .collect(Collectors.joining(System.lineSeparator()));
+ }
+
+ default void printInstructions(PrintStream out) {
+ out.println(formatInstructions());
+ }
+
+ default void printCompleteSummary(PrintStream out) {
+ out.println("Instructions emulated:");
+ out.println("----------------------");
+ printInstructions(out);
+ out.println("");
+ out.println("Pcode emulated:");
+ out.println("---------------");
+ printOps(out);
+ out.println("");
+ out.println("Summary:");
+ printSymbolicSummary(out);
+ }
+
+ default Stream streamPreconditions(Context ctx, Z3InfixPrinter z3p) {
+ Stream shared = getSharedState().getRight().streamPreconditions(ctx, z3p);
+ Stream locals = getAllThreads().stream()
+ .flatMap(t -> t.getLocalSymbolicState().streamPreconditions(ctx, z3p));
+ return Stream.concat(shared, locals);
+ }
+
+ default Stream> streamValuations(Context ctx, Z3InfixPrinter z3p) {
+ Stream> shared =
+ getSharedState().getRight().streamValuations(ctx, z3p);
+ Stream> locals = getAllThreads().stream()
+ .flatMap(t -> t.getLocalSymbolicState().streamValuations(ctx, z3p));
+ return Stream.concat(shared, locals);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeThread.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeThread.java
new file mode 100644
index 0000000000..d7c501bf4c
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeThread.java
@@ -0,0 +1,159 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import java.io.PrintStream;
+import java.util.List;
+
+import org.apache.commons.lang3.tuple.ImmutablePair;
+import org.apache.commons.lang3.tuple.Pair;
+
+import com.microsoft.z3.BitVecExpr;
+import com.microsoft.z3.Context;
+
+import ghidra.app.util.PseudoInstruction;
+import ghidra.pcode.emu.SleighInstructionDecoder;
+import ghidra.pcode.emu.ThreadPcodeExecutorState;
+import ghidra.pcode.emu.auxiliary.AuxPcodeEmulator;
+import ghidra.pcode.emu.auxiliary.AuxPcodeThread;
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.pcode.emu.symz3.plain.SymZ3Space;
+import ghidra.pcode.exec.*;
+import ghidra.pcode.exec.PcodeArithmetic.Purpose;
+import ghidra.pcode.exec.PcodeExecutorStatePiece.Reason;
+import ghidra.program.model.address.Address;
+import ghidra.program.model.address.AddressSpace;
+import ghidra.program.model.lang.*;
+import ghidra.program.model.listing.Instruction;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.symz3.model.SymValueZ3;
+
+public class SymZ3PcodeThread extends AuxPcodeThread
+ implements InternalSymZ3RecordsPreconditions {
+ public SymZ3PcodeThread(String name, AuxPcodeEmulator emulator) {
+ super(name, emulator);
+ }
+
+ @Override
+ protected SleighInstructionDecoder createInstructionDecoder(
+ PcodeExecutorState> sharedState) {
+ return new SleighInstructionDecoder(language, sharedState) {
+ @Override
+ public PseudoInstruction decodeInstruction(Address address, RegisterValue context) {
+ PseudoInstruction instruction = super.decodeInstruction(address, context);
+ addInstruction(instruction);
+ return instruction;
+ }
+ };
+ }
+
+ @Override
+ protected ThreadPcodeExecutorState> createThreadState(
+ PcodeExecutorState> sharedState,
+ PcodeExecutorState> localState) {
+ return new SymZ3ThreadPcodeExecutorState(sharedState, localState);
+ }
+
+ @Override
+ public SymZ3ThreadPcodeExecutorState getState() {
+ return (SymZ3ThreadPcodeExecutorState) super.getState();
+ }
+
+ public PcodeExecutorStatePiece getSharedConcreteState() {
+ return getState().getSharedState().getLeft();
+ }
+
+ public AbstractSymZ3PcodeExecutorStatePiece getSharedSymbolicState() {
+ return getState().getSharedState().getRight();
+ }
+
+ public PcodeExecutorStatePiece getLocalConcreteState() {
+ return getState().getLocalState().getLeft();
+ }
+
+ public AbstractSymZ3PcodeExecutorStatePiece getLocalSymbolicState() {
+ return getState().getLocalState().getRight();
+ }
+
+ @Override
+ public void addPrecondition(String precondition) {
+ getLocalSymbolicState().addPrecondition(precondition);
+ }
+
+ @Override
+ public List getPreconditions() {
+ return getLocalSymbolicState().getPreconditions();
+ }
+
+ public void addInstruction(Instruction inst) {
+ getSharedSymbolicState().addInstruction(this, inst);
+ }
+
+ public void addOp(PcodeOp op) {
+ getSharedSymbolicState().addOp(this, op);
+ }
+
+ public void printRegisterComparison(PrintStream out, String reg) {
+ ImmutablePair p = registerComparison(reg);
+ out.println(reg + " concrete: " + p.getLeft() + " whereas symbolic: " + p.getRight());
+ }
+
+ public ImmutablePair registerComparison(String reg) {
+ Register register = getLanguage().getRegister(reg);
+ PcodeArithmetic concreteArithmetic = getLocalConcreteState().getArithmetic();
+ long regValConcrete = concreteArithmetic
+ .toLong(getLocalConcreteState().getVar(register, Reason.INSPECT), Purpose.INSPECT);
+ SymValueZ3 regValSymbolic = getLocalSymbolicState().getVar(register, Reason.INSPECT);
+ try (Context ctx = new Context()) {
+ BitVecExpr bval = regValSymbolic.getBitVecExpr(ctx);
+ BitVecExpr bvals = (BitVecExpr) bval.simplify();
+ Z3InfixPrinter z3p = new Z3InfixPrinter(ctx);
+ return ImmutablePair.of(Long.toHexString(regValConcrete), z3p.infixUnsigned(bvals));
+ }
+ }
+
+ public void printMemoryComparisonRegPlusOffset(PrintStream out, String reg, int offset) {
+ ImmutablePair p = memoryComparisonRegPlusOffset(reg, offset);
+ out.println("MEM[" + reg + "+" + offset + "]" + " concrete: " + p.getLeft() +
+ " whereas symbolic: " + p.getRight());
+ }
+
+ public ImmutablePair memoryComparisonRegPlusOffset(String reg, int offset) {
+ Language language = this.getLanguage();
+ Register register = language.getRegister(reg);
+ PcodeArithmetic concreteArithmetic = getSharedConcreteState().getArithmetic();
+ long regValConcrete = concreteArithmetic
+ .toLong(getLocalConcreteState().getVar(register, Reason.INSPECT), Purpose.INSPECT);
+ SymValueZ3 regValSymbolic = getLocalSymbolicState().getVar(register, Reason.INSPECT);
+ AddressSpace ram = this.language.getAddressFactory().getDefaultAddressSpace();
+ Address concreteAddress = ram.getAddress(regValConcrete + offset);
+ try (Context ctx = new Context()) {
+ BitVecExpr bval = regValSymbolic.getBitVecExpr(ctx);
+ long memValConcrete = concreteArithmetic.toLong(getSharedConcreteState()
+ .getVar(concreteAddress, 1, false, Reason.INSPECT),
+ Purpose.INSPECT);
+ BitVecExpr bvals = (BitVecExpr) bval.simplify();
+ SymValueZ3 offseteq =
+ new SymValueZ3(ctx, ctx.mkBVAdd(bvals, ctx.mkBV(offset, bval.getSortSize())));
+ SymValueZ3 memValSymbolic =
+ getSharedSymbolicState().getVar(ram, offseteq, 1, false, Reason.INSPECT);
+ BitVecExpr mv = memValSymbolic.getBitVecExpr(ctx);
+ BitVecExpr mvs = (BitVecExpr) mv.simplify();
+ Z3InfixPrinter z3p = new Z3InfixPrinter(ctx);
+ return ImmutablePair.of(Long.toString(memValConcrete, 16), z3p.infixUnsigned(mvs));
+ }
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeThreadExecutor.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeThreadExecutor.java
new file mode 100644
index 0000000000..93ed8d31a0
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeThreadExecutor.java
@@ -0,0 +1,89 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import org.apache.commons.lang3.tuple.Pair;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+
+import ghidra.pcode.emu.DefaultPcodeThread.PcodeThreadExecutor;
+import ghidra.pcode.exec.*;
+import ghidra.pcode.exec.PcodeArithmetic.Purpose;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.program.model.pcode.Varnode;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * An instrumented executor for the Symbolic Summarizer
+ *
+ *
+ * This part is responsible for executing all the actual p-code operations generated by each decoded
+ * instruction. Each thread in the emulator gets a distinct executor. So far, we haven't actually
+ * added any instrumentation, but the conditions of {@link PcodeOp#CBRANCH} operations will likely
+ * be examined by the user, so we set up the skeleton here.
+ */
+public class SymZ3PcodeThreadExecutor extends PcodeThreadExecutor> {
+ /**
+ * Create the executor
+ *
+ * @param thread the thread being created
+ */
+ public SymZ3PcodeThreadExecutor(SymZ3PcodeThread thread) {
+ super(thread);
+ }
+
+ @Override
+ public SymZ3PcodeThread getThread() {
+ return (SymZ3PcodeThread) super.getThread();
+ }
+
+ @Override
+ public void stepOp(PcodeOp op, PcodeFrame frame,
+ PcodeUseropLibrary> library) {
+ getThread().addOp(op);
+ super.stepOp(op, frame, library);
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * This is invoked on every {@link PcodeOp#CBRANCH}, allowing us a decent place to instrument
+ * the emulator and add preconditions to the symbolic state, as we follow along concretely.
+ * Refer to {@link PcodeExecutor#executeConditionalBranch(PcodeOp, PcodeFrame)} to see the
+ * operations inputs.
+ */
+ @Override
+ public void executeConditionalBranch(PcodeOp op, PcodeFrame frame) {
+ Varnode condVar = op.getInput(1);
+ Pair cond = state.getVar(condVar, reason);
+ try (Context ctx = new Context()) {
+ BoolExpr symCond = cond.getRight().getBoolExpr(ctx);
+ /**
+ * The decision is driven by the concrete (left) side of the emulator, but we should
+ * still figure the equivalent precondition for the symbolic (right) side.
+ */
+ if (arithmetic.isTrue(cond, Purpose.CONDITION)) {
+ getThread().addPrecondition(SymValueZ3.serialize(ctx, symCond));
+ }
+ else {
+ getThread().addPrecondition(SymValueZ3.serialize(ctx, ctx.mkNot(symCond)));
+ }
+ }
+ super.executeConditionalBranch(op, frame);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeUseropLibrary.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeUseropLibrary.java
new file mode 100644
index 0000000000..b11db2fbe4
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3PcodeUseropLibrary.java
@@ -0,0 +1,25 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import org.apache.commons.lang3.tuple.Pair;
+
+import ghidra.pcode.exec.AnnotatedPcodeUseropLibrary;
+import ghidra.symz3.model.*;
+
+public class SymZ3PcodeUseropLibrary extends AnnotatedPcodeUseropLibrary> {
+
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3RecordsExecution.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3RecordsExecution.java
new file mode 100644
index 0000000000..98143ae72a
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3RecordsExecution.java
@@ -0,0 +1,54 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import java.util.List;
+
+import ghidra.program.model.address.Address;
+import ghidra.program.model.listing.Instruction;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.trace.model.target.path.KeyPath;
+
+public interface SymZ3RecordsExecution {
+ record RecInstruction(int index, SymZ3PcodeThread thread, Instruction instruction) {
+ @Override
+ public final String toString() {
+ return "[%s]: %s".formatted(thread.getName(), instruction);
+ }
+
+ public String getThreadName() {
+ return KeyPath.parse(thread.getName()).index();
+ }
+
+ public Address getAddress() {
+ return instruction.getAddress();
+ }
+ }
+
+ record RecOp(int index, SymZ3PcodeThread thread, PcodeOp op) {
+ public String getThreadName() {
+ return KeyPath.parse(thread.getName()).index();
+ }
+
+ public Address getAddress() {
+ return op.getSeqnum().getTarget();
+ }
+ }
+
+ public List getInstructions();
+
+ public List getOps();
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3RecordsPreconditions.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3RecordsPreconditions.java
new file mode 100644
index 0000000000..701dc7ffcc
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3RecordsPreconditions.java
@@ -0,0 +1,22 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import java.util.List;
+
+public interface SymZ3RecordsPreconditions {
+ public List getPreconditions();
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3RegisterMap.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3RegisterMap.java
new file mode 100644
index 0000000000..d2e9c13cdb
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3RegisterMap.java
@@ -0,0 +1,231 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import java.util.*;
+import java.util.Map.Entry;
+import java.util.stream.Stream;
+
+import com.microsoft.z3.*;
+
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.program.model.lang.Register;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * A class that can store SymZ3Values in registers /*
+ *
+ * NOTE: DELIBERATELY NO KNOWLEDGE OF SPACES, Languages, or "get" and "set"
+ */
+public class SymZ3RegisterMap {
+
+ // TODO: make this be private and provide appropriate methods
+ // in the map, all registers are base registers.
+ public Map regvals = new HashMap();
+
+ //private List createdSymbolics = new ArrayList();
+ private final Set registerNamesRead = new HashSet();
+ private final Set registerNamesUpdated = new HashSet();
+ private final Map knownRegisters = new HashMap();
+
+ public List getRegisterNamesRead() {
+ ArrayList result = new ArrayList(registerNamesRead);
+ Collections.sort(result);
+ return result;
+ }
+
+ public List getRegisterNamesUpdated() {
+ ArrayList result = new ArrayList(registerNamesUpdated);
+ Collections.sort(result);
+ return result;
+
+ }
+
+ public List getRegisterNamesReadOrUpdated() {
+ HashSet both = new HashSet(registerNamesRead);
+ both.addAll(registerNamesUpdated);
+ ArrayList result = new ArrayList(both);
+ Collections.sort(result);
+ return result;
+ }
+
+ public List getRegisterNames() {
+ // make this recursive later and get children???
+ List result = new ArrayList();
+ for (Map.Entry entry : regvals.entrySet()) {
+ Register r = entry.getKey();
+ result.add(r.getName());
+ }
+ return result;
+ }
+
+ public void updateRegister(Register r, SymValueZ3 update) {
+ try (Context ctx = new Context()) {
+ registerNamesUpdated.add(r.getName());
+ updateRegisterHelper(ctx, r, update);
+ if (!this.knownRegisters.containsKey(r.getName())) {
+ this.knownRegisters.put(r.getName(), r);
+ }
+ }
+ }
+
+ private void updateRegisterHelper(Context ctx, Register r, SymValueZ3 update) {
+ if (r.isBaseRegister()) {
+ regvals.put(r, update);
+ return;
+ }
+ // so, we want to update the base, but also need to keep portions of it.
+ // 3 cases, the base might contribute at left, right, or both
+
+ BitVecExpr bv = update.getBitVecExpr(ctx);
+ Register base = r.getBaseRegister();
+ SymValueZ3 baseVal = this.getRegisterHelper(ctx, base);
+ BitVecExpr result = null;
+ int lsbInBase = r.getLeastSignificantBitInBaseRegister();
+ // consider whether some portion of base remains on the left
+ if (r.getBitLength() + lsbInBase < base.getBitLength()) {
+ int high = base.getBitLength() - 1;
+ int low = r.getBitLength() + lsbInBase;
+ BitVecExpr left = ctx.mkExtract(high, low, baseVal.getBitVecExpr(ctx));
+ result = ctx.mkConcat(left, bv);
+ }
+ else {
+ result = bv;
+ }
+
+ // consider whether some portion of base remains on the right
+ if (result.getSortSize() < base.getBitLength()) {
+ int high = base.getBitLength() - result.getSortSize() - 1;
+ int low = 0;
+ BitVecExpr right = ctx.mkExtract(high, low, baseVal.getBitVecExpr(ctx));
+ result = ctx.mkConcat(result, right);
+ }
+ regvals.put(base, new SymValueZ3(ctx, result));
+ }
+
+ public SymValueZ3 getRegister(Register r) {
+ try (Context ctx = new Context()) {
+ this.registerNamesRead.add(r.getName());
+ if (!this.knownRegisters.containsKey(r.getName())) {
+ this.knownRegisters.put(r.getName(), r);
+ }
+ return getRegisterHelper(ctx, r);
+ }
+ }
+
+ // normally a call to get will create a symbolic, but we might
+ // want the ability to check if there is a value
+ public Boolean hasValueForRegister(Register r) {
+ if (r.isBaseRegister()) {
+ SymValueZ3 value = regvals.get(r);
+ return !(value == null);
+ }
+ Register base = r.getBaseRegister();
+ return this.hasValueForRegister(base);
+ }
+
+ private SymValueZ3 getRegisterHelper(Context ctx, Register r) {
+ if (r.isBaseRegister()) {
+ SymValueZ3 value = regvals.get(r);
+ if (value != null) {
+ return value;
+ }
+
+ if (r.getGroup() != null && r.getGroup().equals("FLAGS")) {
+ // we treat flags as special, because we create a single symbolic bit
+ BitVecExpr e = ctx.mkBVConst(r.getName(), 1);
+ BitVecExpr zeros = ctx.mkBV(0, r.getBitLength() - 1);
+ SymValueZ3 di = new SymValueZ3(ctx, ctx.mkConcat(zeros, e));
+ this.updateRegisterHelper(ctx, r, di);
+ return di;
+ }
+ BitVecExpr e = ctx.mkBVConst(r.getName(), r.getBitLength());
+ SymValueZ3 di = new SymValueZ3(ctx, e);
+ this.updateRegisterHelper(ctx, r, di);
+ return di;
+ }
+ int lsbInBase = r.getLeastSignificantBitInBaseRegister();
+ Register base = r.getBaseRegister();
+ SymValueZ3 baseVal = this.getRegisterHelper(ctx, base);
+
+ BitVecExpr b = ctx.mkExtract(lsbInBase + r.getBitLength() - 1, lsbInBase,
+ baseVal.getBitVecExpr(ctx));
+ SymValueZ3 result = new SymValueZ3(ctx, b);
+
+ return result;
+ }
+
+ public String printableRegister(Context ctx, Register r) {
+ Z3InfixPrinter z3p = new Z3InfixPrinter(ctx);
+ Entry valuation = valuationFor(ctx, z3p, r);
+ return valuation.getKey() + " = " + valuation.getValue();
+ }
+
+ public Entry valuationFor(Context ctx, Z3InfixPrinter z3p, Register r) {
+ String sizeString = ":" + r.getNumBytes() * 8;
+
+ SymValueZ3 rv = getRegisterHelper(ctx, r);
+
+ if (r.getNumBytes() == 1 && rv.hasBoolExpr()) {
+ BoolExpr e = rv.getBoolExpr(ctx);
+ e = (BoolExpr) e.simplify();
+ return Map.entry(r.toString() + sizeString, z3p.infixTopLevel(e));
+ }
+ BitVecExpr v = rv.getBitVecExpr(ctx);
+ v = (BitVecExpr) v.simplify();
+ return Map.entry(r.toString() + sizeString, z3p.infixTopLevel(v));
+ }
+
+ public String printableSummary() {
+ try (Context ctx = new Context()) {
+ Z3InfixPrinter z3p = new Z3InfixPrinter(ctx);
+ StringBuilder result = new StringBuilder();
+ result.append("----------------------------------------------------");
+ result.append(System.lineSeparator());
+ result.append("Registers that were read: ");
+ result.append(System.lineSeparator());
+ List registersRead = this.getRegisterNamesRead();
+ result.append(z3p.fetchListOfStringsHelper(registersRead));
+
+ result.append("Registers that were updated: ");
+ result.append(System.lineSeparator());
+ List registersUpdated = this.getRegisterNamesUpdated();
+ result.append(z3p.fetchListOfStringsHelper(registersUpdated));
+
+ result.append("Registers that were read or updated: ");
+ result.append(System.lineSeparator());
+ List registersReadOrUpdated = this.getRegisterNamesReadOrUpdated();
+ result.append(z3p.fetchListOfStringsHelper(registersReadOrUpdated));
+
+ result.append("Current Valuations (in terms of valuations at start)");
+ result.append(System.lineSeparator());
+
+ for (String name : this.getRegisterNamesReadOrUpdated()) {
+ Register r = this.knownRegisters.get(name);
+ result.append(printableRegister(ctx, r));
+ result.append(System.lineSeparator());
+ }
+ return result.toString();
+ }
+ }
+
+ public Stream> streamValuations(Context ctx, Z3InfixPrinter z3p) {
+ return getRegisterNamesReadOrUpdated().stream().map(n -> {
+ Register r = knownRegisters.get(n);
+ return valuationFor(ctx, z3p, r);
+ });
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3ThreadPcodeExecutorState.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3ThreadPcodeExecutorState.java
new file mode 100644
index 0000000000..ea28801045
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/SymZ3ThreadPcodeExecutorState.java
@@ -0,0 +1,40 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3;
+
+import org.apache.commons.lang3.tuple.Pair;
+
+import ghidra.pcode.emu.ThreadPcodeExecutorState;
+import ghidra.pcode.exec.PcodeExecutorState;
+import ghidra.symz3.model.SymValueZ3;
+
+public class SymZ3ThreadPcodeExecutorState
+ extends ThreadPcodeExecutorState> {
+ public SymZ3ThreadPcodeExecutorState(PcodeExecutorState> sharedState,
+ PcodeExecutorState> localState) {
+ super(sharedState, localState);
+ }
+
+ @Override
+ public SymZ3PairedPcodeExecutorState getSharedState() {
+ return (SymZ3PairedPcodeExecutorState) super.getSharedState();
+ }
+
+ @Override
+ public SymZ3PairedPcodeExecutorState getLocalState() {
+ return (SymZ3PairedPcodeExecutorState) super.getLocalState();
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/full/SymZ3DebuggerPcodeEmulator.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/full/SymZ3DebuggerPcodeEmulator.java
new file mode 100644
index 0000000000..0b4cecb164
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/full/SymZ3DebuggerPcodeEmulator.java
@@ -0,0 +1,76 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.full;
+
+import java.util.Collection;
+
+import ghidra.debug.api.emulation.PcodeDebuggerAccess;
+import ghidra.pcode.emu.symz3.*;
+import ghidra.pcode.emu.symz3.plain.SymZ3PcodeEmulator;
+import ghidra.pcode.exec.debug.auxiliary.AuxDebuggerEmulatorPartsFactory;
+import ghidra.pcode.exec.debug.auxiliary.AuxDebuggerPcodeEmulator;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * A Debugger-integrated emulator with symbolic z3 summarization
+ */
+public class SymZ3DebuggerPcodeEmulator extends AuxDebuggerPcodeEmulator
+ implements SymZ3PcodeEmulatorTrait {
+ /**
+ * Create an emulator
+ *
+ * @param access the trace-and-debugger access shim
+ */
+ public SymZ3DebuggerPcodeEmulator(PcodeDebuggerAccess access) {
+ super(access);
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * Here, we just return the singleton parts factory. This appears simple because all the
+ * complexity is encapsulated in the factory. See {@link SymZ3PartsFactory} to see everything
+ * the implementation actually entails. Notice that this is the same parts factory used by
+ * {@link SymZ3PcodeEmulator}. The {@link AuxDebugggerPcodeEmulator} knows to use the more
+ * capable state parts.
+ */
+ @Override
+ protected AuxDebuggerEmulatorPartsFactory getPartsFactory() {
+ return SymZ3PartsFactory.INSTANCE;
+ }
+
+ @Override
+ public SymZ3PcodeThread newThread() {
+ return (SymZ3PcodeThread) super.newThread();
+ }
+
+ @Override
+ public SymZ3PcodeThread newThread(String name) {
+ return (SymZ3PcodeThread) super.newThread(name);
+ }
+
+ @Override
+ @SuppressWarnings("unchecked")
+ public Collection getAllThreads() {
+ return (Collection) super.getAllThreads();
+ }
+
+ @Override
+ public SymZ3PairedPcodeExecutorState getSharedState() {
+ return (SymZ3PairedPcodeExecutorState) super.getSharedState();
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/full/SymZ3DebuggerPcodeEmulatorFactory.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/full/SymZ3DebuggerPcodeEmulatorFactory.java
new file mode 100644
index 0000000000..13ee57a27b
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/full/SymZ3DebuggerPcodeEmulatorFactory.java
@@ -0,0 +1,40 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.full;
+
+import ghidra.app.plugin.core.debug.service.emulation.AbstractDebuggerPcodeEmulatorFactory;
+import ghidra.debug.api.emulation.DebuggerPcodeMachine;
+import ghidra.debug.api.emulation.PcodeDebuggerAccess;
+
+/**
+ * An emulator factory for making the {@link SymZ3DebuggerPcodeEmulator} discoverable to the UI
+ *
+ *
+ * This is the final class to create a full Debugger-integrated emulator. This class is what makes
+ * it appear in the menu of possible emulators the user may configure.
+ */
+public class SymZ3DebuggerPcodeEmulatorFactory extends AbstractDebuggerPcodeEmulatorFactory {
+
+ @Override
+ public String getTitle() {
+ return "Symbolic Z3 Summary with Concrete Emulation";
+ }
+
+ @Override
+ public DebuggerPcodeMachine create(PcodeDebuggerAccess access) {
+ return new SymZ3DebuggerPcodeEmulator(access);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/SymZ3EmuUnixFileSystem.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/SymZ3EmuUnixFileSystem.java
new file mode 100644
index 0000000000..9f2a82694f
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/SymZ3EmuUnixFileSystem.java
@@ -0,0 +1,49 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.lib;
+
+import org.apache.commons.lang3.tuple.Pair;
+
+import ghidra.pcode.emu.sys.*;
+import ghidra.pcode.emu.unix.AbstractEmuUnixFile;
+import ghidra.pcode.emu.unix.AbstractEmuUnixFileSystem;
+import ghidra.symz3.model.SymValueZ3;
+
+public class SymZ3EmuUnixFileSystem extends AbstractEmuUnixFileSystem> {
+
+ /**
+ * A file whose contents have a SymValueZ3 piece
+ */
+ public static class SymZ3EmuUnixFile extends AbstractEmuUnixFile> {
+ protected BytesEmuFileContents concrete = new BytesEmuFileContents();
+
+ public SymZ3EmuUnixFile(String pathname, int mode) {
+ super(pathname, mode);
+ }
+
+ @Override
+ protected EmuFileContents> createDefaultContents() {
+ // for now we leave the piece null
+ return new PairedEmuFileContents<>(concrete, null);
+ }
+ }
+
+ @Override
+ public AbstractEmuUnixFile> newFile(String pathname, int mode)
+ throws EmuIOException {
+ return new SymZ3EmuUnixFile(pathname, mode);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/SymZ3LinuxAmd64SyscallLibrary.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/SymZ3LinuxAmd64SyscallLibrary.java
new file mode 100644
index 0000000000..24872639d1
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/SymZ3LinuxAmd64SyscallLibrary.java
@@ -0,0 +1,52 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.lib;
+
+import org.apache.commons.lang3.tuple.Pair;
+
+import ghidra.pcode.emu.PcodeMachine;
+import ghidra.pcode.emu.linux.EmuLinuxAmd64SyscallUseropLibrary;
+import ghidra.pcode.emu.unix.EmuUnixFileSystem;
+import ghidra.pcode.emu.unix.EmuUnixUser;
+import ghidra.program.model.listing.Program;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * A library for the Symbolic Summary Z3 should we wish to customize any functions
+ *
+ *
+ * This library is not currently accessible from the UI. It can be used with scripts by overriding a
+ * emulator's userop library factory method.
+ *
+ *
+ * TODO: A means of adding and configuring userop libraries in the UI.
+ *
+ *
+ * TODO: Example scripts.
+ */
+public class SymZ3LinuxAmd64SyscallLibrary
+ extends EmuLinuxAmd64SyscallUseropLibrary> {
+
+ public SymZ3LinuxAmd64SyscallLibrary(PcodeMachine> machine,
+ EmuUnixFileSystem> fs, Program program, EmuUnixUser user) {
+ super(machine, fs, program, user);
+ }
+
+ public SymZ3LinuxAmd64SyscallLibrary(PcodeMachine> machine,
+ EmuUnixFileSystem> fs, Program program) {
+ super(machine, fs, program);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/Z3InfixPrinter.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/Z3InfixPrinter.java
new file mode 100644
index 0000000000..47c9b74cc0
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/Z3InfixPrinter.java
@@ -0,0 +1,327 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.lib;
+
+import java.math.BigInteger;
+import java.util.List;
+
+import com.microsoft.z3.*;
+import com.microsoft.z3.FuncDecl.Parameter;
+import com.microsoft.z3.enumerations.Z3_decl_kind;
+
+import ghidra.symz3.model.SymValueZ3;
+
+@SuppressWarnings({ "rawtypes", "unchecked" })
+public class Z3InfixPrinter {
+ private static final boolean SHOW_ALL_SIZES = true;
+ private static final boolean FORCE_UNSIGNED = false; //any numeric values will display as unsigned values
+
+ private final Context ctx;
+
+ public Z3InfixPrinter(Context ctx) {
+ this.ctx = ctx;
+ }
+
+ public String symbolForZ3(Z3_decl_kind op) {
+ return switch (op) {
+ case Z3_decl_kind.Z3_OP_EQ -> "==";
+ case Z3_decl_kind.Z3_OP_BMUL -> "*";
+ case Z3_decl_kind.Z3_OP_BADD -> "+";
+ case Z3_decl_kind.Z3_OP_BSUB -> "-";
+ case Z3_decl_kind.Z3_OP_SLEQ -> "<=";
+ case Z3_decl_kind.Z3_OP_NOT -> "not";
+ case Z3_decl_kind.Z3_OP_AND -> "&&";
+ case Z3_decl_kind.Z3_OP_OR -> "||";
+ case Z3_decl_kind.Z3_OP_CONCAT -> "::";
+ case Z3_decl_kind.Z3_OP_ULEQ -> "u<=";
+ case Z3_decl_kind.Z3_OP_BAND -> "&";
+ case Z3_decl_kind.Z3_OP_BOR -> "|";
+ default -> op.toString();
+ };
+ }
+
+ public Expr printSimplificationsConcat(Expr e) {
+ //Msg.debug(this, "Print simplification of " + e);
+ if (e.getNumArgs() == 2) {
+ // check if the first argument is 0, if so we omit as it is implied
+ Expr arg0 = e.getArgs()[0];
+ if (arg0.isNumeral()) {
+ BitVecNum bvn = (BitVecNum) arg0;
+ if (bvn.getInt() == 0) {
+ return e.getArgs()[1];
+ }
+ }
+
+ }
+ else if (e.getNumArgs() > 2) {
+ Expr arg0 = e.getArgs()[0];
+ if (arg0.isNumeral()) {
+ BitVecNum bvn = (BitVecNum) arg0;
+ if (bvn.getInt() == 0) {
+ Expr result = ctx.mkConcat(e.getArgs()[1], e.getArgs()[2]);
+ for (int i = 0; i < e.getNumArgs() - 3; i++) {
+ result = ctx.mkConcat(result, e.getArgs()[i + 3]);
+ }
+ return result;
+ }
+ }
+ }
+ return e;
+ }
+
+ public Expr normalize(Expr e) {
+ // precondition is that the op is commutative
+ if (e.getNumArgs() == 2) {
+ Expr arg0 = e.getArgs()[0];
+ Expr arg1 = e.getArgs()[1];
+ if (arg0.isNumeral() && !arg1.isNumeral()) {
+ Expr[] swap = { arg1, arg0 };
+ return e.update(swap);
+ }
+ }
+ return e;
+ }
+
+ public Expr printSimplifications(Expr e) {
+ Z3_decl_kind op = e.getFuncDecl().getDeclKind();
+ if (op == Z3_decl_kind.Z3_OP_CONCAT) {
+ return printSimplificationsConcat(e);
+ }
+ return e;
+ }
+
+ public String infix(Expr e) {
+ return infixHelper(e, '(', ')', SHOW_ALL_SIZES, FORCE_UNSIGNED);
+ }
+
+ public String infixForceSize(Expr e) {
+ return infixHelper(e, '(', ')', true, FORCE_UNSIGNED);
+ }
+
+ public String infixWithBrackets(Expr e) {
+ return infixHelper(e, '[', ']', SHOW_ALL_SIZES, FORCE_UNSIGNED);
+ }
+
+ public String infixTopLevel(Expr e) {
+ return infixHelper(e, ' ', ' ', SHOW_ALL_SIZES, FORCE_UNSIGNED);
+ }
+
+ public String uninterpretedStringHelper(Expr e) {
+ String name = e.getFuncDecl().getName().toString();
+ if (e.getNumArgs() == 0)
+ return name;
+ if (e.getNumArgs() != 1)
+ return e.toString();
+ if (name.equals("load_64_8") || name.equals("load_64_16") || name.equals("load_64_32") ||
+ name.equals("load_64_64")) {
+ BitVecExpr eb = (BitVecExpr) e;
+ int bitSize = eb.getSortSize();
+ String result =
+ "MEM" + infixWithBrackets(e.getArgs()[0]) + ":" + Integer.toString(bitSize);
+ //println("uninterpreted helper given " + e + " will return " + result);
+ return result;
+
+ }
+ return "(print helper needed)" + e.toString();
+ }
+
+ public class RegisterPlusConstant {
+ public String registerName;
+ public BigInteger constant;
+ public boolean isNegative;
+
+ public RegisterPlusConstant(String name, BigInteger c, boolean isneg) {
+ this.registerName = name;
+ this.constant = c;
+ this.isNegative = isneg;
+ }
+ }
+
+ // if the BitVecExpr eb represents a negative number, return the magnitue of that number else null
+ // e.g., "-6" we return 6.
+ public BigInteger isNegativeConstant(BitVecExpr eb) {
+
+ if (!eb.isNumeral()) {
+ //Msg.info(this, "no, " + eb.getSExpr() + " is not negative its not even a number");
+ return null;
+ }
+
+ BitVecNum ebnum = (BitVecNum) eb;
+ String ebstring = ebnum.toBinaryString();
+
+ // when converted by Z3, leading zeroes are removed! So what we do is check the size of the
+ // string versus the sort size. Previously we used extract but there is some sort of Z3 issue...
+
+ if (ebstring.length() < eb.getSortSize() || ebstring.length() == 1) {
+ //Msg.info(this, "no, " + eb.getSExpr() + " is not negative as the sign bit is not a 1");
+ return null;
+ }
+
+ assert (ebstring.charAt(0) == '1');
+ ebstring = ebstring.replace('1', 'F');
+ ebstring = ebstring.replace('0', '1');
+ ebstring = ebstring.replace('F', '0');
+ BigInteger bi = new BigInteger(ebstring, 2);
+ bi = bi.add(BigInteger.ONE);
+
+ //Msg.info(this, "yes, " + eb.getSExpr() + " is negative " + bi);
+ return bi;
+
+ }
+
+ public BigInteger isConstant(BitVecExpr eb) {
+ if (!eb.isNumeral()) {
+ return null;
+ }
+ BitVecNum num = (BitVecNum) eb;
+ return num.getBigInteger();
+ }
+
+ public boolean isCommutative(Z3_decl_kind op) {
+ return (op == Z3_decl_kind.Z3_OP_BADD ||
+ op == Z3_decl_kind.Z3_OP_BMUL ||
+ op == Z3_decl_kind.Z3_OP_BOR ||
+ op == Z3_decl_kind.Z3_OP_BAND);
+ }
+
+ public boolean isSizeForcing(Z3_decl_kind op) {
+ return (op == Z3_decl_kind.Z3_OP_CONCAT ||
+ op == Z3_decl_kind.Z3_OP_BOR ||
+ op == Z3_decl_kind.Z3_OP_BAND);
+ }
+
+ public String infixHelper(Expr e, boolean forceSize) {
+ return infixHelper(e, '(', ')', forceSize, FORCE_UNSIGNED);
+ }
+
+ public String infixUnsigned(Expr e) {
+ return infixHelper(e, '(', ')', SHOW_ALL_SIZES, true);
+ }
+
+ @SuppressWarnings("unused")
+ public String infixHelper(Expr e, char lchr, char rchr, boolean forceSize,
+ boolean forceUnsigned) {
+ if (e == null) {
+ return "null";
+ }
+ Z3_decl_kind op = e.getFuncDecl().getDeclKind();
+
+ // print_simplifications breaks the invariant that sizes of things on the right and left are equal
+ if (!forceSize) {
+ //e = print_simplifications(e);
+ }
+
+ if (isCommutative(op)) {
+ e = normalize(e);
+ }
+
+ if (op == Z3_decl_kind.Z3_OP_UNINTERPRETED) {
+ String result = uninterpretedStringHelper(e);
+ if (lchr == '[') {
+ return lchr + result + rchr;
+ }
+ return result;
+ }
+
+ if (op == Z3_decl_kind.Z3_OP_EXTRACT) {
+ Parameter[] params = e.getFuncDecl().getParameters();
+ // This is more Sleigh-opinionated....
+ return "%s[%d:%d]".formatted(
+ infixForceSize(e.getArgs()[0]),
+ params[1].getInt(),
+ params[0].getInt() - params[1].getInt() + 1);
+ /*return "extract(" + infixForceSize(e.getArgs()[0]) + "," + params[0].getInt() + "," +
+ params[1].getInt() + ")";*/
+ }
+
+ if (op == Z3_decl_kind.Z3_OP_ITE) {
+ Parameter[] params = e.getFuncDecl().getParameters();
+ return "%s ? %s : %s".formatted(
+ infixForceSize(e.getArgs()[0]),
+ infixForceSize(e.getArgs()[1]),
+ infixForceSize(e.getArgs()[2]));
+ }
+
+ // problem here... the helper might transform our expression.
+ String opString = symbolForZ3(op);
+ if (e.getNumArgs() >= 2) {
+ String result = infixHelper(e.getArgs()[0],
+ SHOW_ALL_SIZES || (isSizeForcing(op) && e.getArgs()[0].isNumeral()));
+
+ for (int i = 1; i < e.getNumArgs(); i++) {
+ result = result + " " + opString + " ";
+ result = result + infixHelper(e.getArgs()[i],
+ SHOW_ALL_SIZES || (isSizeForcing(op) && e.getArgs()[i].isNumeral()));
+ }
+
+ return lchr + result + rchr;
+ }
+ if (e.getNumArgs() == 1) {
+ Expr arg0 = e.getArgs()[0];
+ return opString + lchr + infix(arg0) + rchr;
+ }
+ if (e.getNumArgs() == 0) {
+ if (e.isBV()) {
+ BitVecExpr eb = (BitVecExpr) e;
+ String sizeString = "";
+ if (SHOW_ALL_SIZES || forceSize) {
+ sizeString = ":" + eb.getSortSize();
+ }
+ if (e.isNumeral()) {
+ BitVecNum bvn = (BitVecNum) e;
+ if (forceUnsigned) {
+ return lchr + "0x" + bvn.getBigInteger().toString(16) + sizeString + rchr;
+ }
+ BigInteger b = isNegativeConstant(eb);
+ if (b == null) {
+ BigInteger bi = bvn.getBigInteger();
+ return lchr + "0x" + bi.toString(16) + sizeString + rchr;
+ }
+ return lchr + "-0x" + b.toString(16) + sizeString + rchr;
+ }
+ return eb.toString() + sizeString;
+ }
+ return e.toString();
+ }
+ return "multi-arg" + " for " + op + "yields: " + e.toString();
+ }
+
+ public String fetchListOfStringsHelper(List elements) {
+ StringBuilder result = new StringBuilder();
+ boolean comma = false;
+ for (String r : elements) {
+ if (comma) {
+ result.append(", ");
+ }
+ result.append(r);
+ comma = true;
+ }
+ result.append(System.lineSeparator());
+ return result.toString();
+ }
+
+ public String infix(SymValueZ3 value) {
+ if (value.getBoolExpr(ctx) != null) {
+ return infix(value.getBoolExpr(ctx));
+ }
+ return infix(value.getBitVecExpr(ctx));
+ }
+
+ public String infixWithSexpr(SymValueZ3 value) {
+ Expr e = value.hasBoolExpr() ? value.getBoolExpr(ctx) : value.getBitVecExpr(ctx);
+ return infix(value) + " internal sexpr: " + e.toString();
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/Z3MemoryWitness.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/Z3MemoryWitness.java
new file mode 100644
index 0000000000..3a5be278bc
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/lib/Z3MemoryWitness.java
@@ -0,0 +1,24 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.lib;
+
+import ghidra.symz3.model.SymValueZ3;
+
+public record Z3MemoryWitness(SymValueZ3 address, int bytesMoved, WitnessType t) {
+ public enum WitnessType {
+ LOAD, STORE
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3MemorySpace.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3MemorySpace.java
new file mode 100644
index 0000000000..195152a40b
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3MemorySpace.java
@@ -0,0 +1,67 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.plain;
+
+import java.util.Map.Entry;
+import java.util.stream.Stream;
+
+import com.microsoft.z3.Context;
+
+import ghidra.pcode.emu.symz3.SymZ3MemoryMap;
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.program.model.lang.Language;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * The storage space for memory in a SymZ3Space. See SymZ3MemoryMap for limitations which are
+ * extensive.
+ *
+ *
+ * The SymZ3Space is partitioned into separate storage spaces for registers, memory, etc. As such,
+ * when the space is used for more complex emulators (e.g., based on trace) This class is not
+ * extended. E.g., there exists a TraceSymZ3Space that derives from SymZ3Space, but the individual
+ * pieces use composition instead of inheritance. E.g., most all of the functionality is delegated
+ * to the SymZ3MemoryMap and there is just a bit of plumbing here.
+ */
+public class SymZ3MemorySpace extends SymZ3Space {
+
+ private SymZ3MemoryMap mmap;
+
+ public SymZ3MemorySpace(Language language) {
+ super();
+ mmap = new SymZ3MemoryMap(language);
+ }
+
+ @Override
+ public SymValueZ3 get(SymValueZ3 offset, int size) {
+ return mmap.load(offset, size, true);
+ }
+
+ @Override
+ public void set(SymValueZ3 offset, int size, SymValueZ3 val) {
+ mmap.store(offset, size, val);
+ }
+
+ @Override
+ public String printableSummary() {
+ return mmap.printableSummary();
+ }
+
+ @Override
+ public Stream> streamValuations(Context ctx, Z3InfixPrinter z3p) {
+ return mmap.streamValuations(ctx, z3p);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3PcodeEmulator.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3PcodeEmulator.java
new file mode 100644
index 0000000000..53ae5a0b78
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3PcodeEmulator.java
@@ -0,0 +1,73 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.plain;
+
+import java.util.Collection;
+
+import ghidra.pcode.emu.auxiliary.AuxEmulatorPartsFactory;
+import ghidra.pcode.emu.auxiliary.AuxPcodeEmulator;
+import ghidra.pcode.emu.symz3.*;
+import ghidra.program.model.lang.Language;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * A stand-alone emulator with symbolic Z3 summarization analysis
+ */
+public class SymZ3PcodeEmulator extends AuxPcodeEmulator
+ implements SymZ3PcodeEmulatorTrait {
+ /**
+ * Create an emulator
+ *
+ * @param language the language (processor model)
+ */
+ public SymZ3PcodeEmulator(Language language) {
+ super(language);
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * Here, we just return the singleton parts factory. This appears simple because all the
+ * complexity is encapsulated in the factory. See {@link SymZ3PartsFactory} to see everything
+ * the implementation actually entails.
+ */
+ @Override
+ protected AuxEmulatorPartsFactory getPartsFactory() {
+ return SymZ3PartsFactory.INSTANCE;
+ }
+
+ @Override
+ public SymZ3PcodeThread newThread() {
+ return (SymZ3PcodeThread) super.newThread();
+ }
+
+ @Override
+ public SymZ3PcodeThread newThread(String name) {
+ return (SymZ3PcodeThread) super.newThread(name);
+ }
+
+ @Override
+ @SuppressWarnings("unchecked")
+ public Collection getAllThreads() {
+ return (Collection) super.getAllThreads();
+ }
+
+ @Override
+ public SymZ3PcodeExecutorState getSharedState() {
+ return (SymZ3PcodeExecutorState) super.getSharedState();
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3PcodeExecutorState.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3PcodeExecutorState.java
new file mode 100644
index 0000000000..bba8ae3227
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3PcodeExecutorState.java
@@ -0,0 +1,65 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.plain;
+
+import ghidra.pcode.emu.symz3.*;
+import ghidra.pcode.exec.BytesPcodeExecutorStatePiece;
+import ghidra.pcode.exec.IndependentPairedPcodeExecutorState;
+import ghidra.program.model.lang.Language;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * A paired concrete-plus-symz3 state
+ *
+ *
+ * This contains the emulator's machine state along with symbolic expressions. Technically, one of
+ * these will hold the machine's memory, while another (for each thread) will hold the machine's
+ * registers. It's composed of two pieces. The concrete piece holds the actual concrete bytes, while
+ * the SymValueZ3 piece holds the symbolic values. A request to get a variable's value from this
+ * state will return a pair where the left element comes from the concrete piece and the right
+ * element comes from the symbolic piece.
+ */
+public class SymZ3PcodeExecutorState
+ extends IndependentPairedPcodeExecutorState
+ implements SymZ3PairedPcodeExecutorState {
+
+ /**
+ * Create a state from the two given pieces
+ *
+ * @param concrete the concrete piece
+ * @param symz3 the symbolic z3 piece
+ */
+ protected SymZ3PcodeExecutorState(BytesPcodeExecutorStatePiece concrete,
+ SymZ3PcodeExecutorStatePiece symz3) {
+ super(concrete, symz3);
+ }
+
+ /**
+ * Create a state from the given concrete piece and a symbolic piece
+ *
+ * @param language the language for creating the symz3 piece
+ * @param concrete the concrete piece
+ */
+ public SymZ3PcodeExecutorState(Language language, BytesPcodeExecutorStatePiece concrete) {
+ this(concrete,
+ new SymZ3PcodeExecutorStatePiece(language, SymZ3PcodeArithmetic.forLanguage(language)));
+ }
+
+ @Override
+ public AbstractSymZ3PcodeExecutorStatePiece getRight() {
+ return (SymZ3PcodeExecutorStatePiece) super.getRight();
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3PcodeExecutorStatePiece.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3PcodeExecutorStatePiece.java
new file mode 100644
index 0000000000..38f493fa52
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3PcodeExecutorStatePiece.java
@@ -0,0 +1,101 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.plain;
+
+import java.util.Map;
+
+import ghidra.pcode.emu.symz3.AbstractSymZ3PcodeExecutorStatePiece;
+import ghidra.pcode.emu.symz3.SymZ3PcodeArithmetic;
+import ghidra.pcode.exec.PcodeArithmetic;
+import ghidra.program.model.address.AddressSpace;
+import ghidra.program.model.lang.Language;
+import ghidra.program.model.lang.Register;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * The state piece for holding symbolic values in the emulator's machine state
+ *
+ */
+public class SymZ3PcodeExecutorStatePiece extends AbstractSymZ3PcodeExecutorStatePiece {
+ /**
+ * Create the SymZ3 piece
+ *
+ * @param language the language of the emulator
+ * @param addressArithmetic the address arithmetic, likely taken from the concrete piece
+ */
+ public SymZ3PcodeExecutorStatePiece(Language language,
+ PcodeArithmetic addressArithmetic) {
+ super(language, addressArithmetic, SymZ3PcodeArithmetic.forLanguage(language));
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * Here we use the simplest scheme for creating a map of {@link SymZ3Space}s. This is
+ * essentially a lazy map from address space to some object for managing symbolic values in that
+ * address space. The space could be a memory space, register space, unique space, etc. This
+ * piece will look up the space, creating it if necessary, and then delegate the get and set
+ * methods.
+ */
+ @Override
+ protected AbstractSpaceMap newSpaceMap(Language language) {
+ return new SimpleSpaceMap() {
+ @Override
+ protected SymZ3Space newSpace(AddressSpace space) {
+ if (space.isConstantSpace()) {
+ throw new AssertionError();
+ }
+ else if (space.isRegisterSpace()) {
+ return new SymZ3RegisterSpace(space, language);
+ }
+ else if (space.isUniqueSpace()) {
+ return new SymZ3UniqueSpace();
+ }
+ else if (space.isLoadedMemorySpace()) {
+ return new SymZ3MemorySpace(language);
+ }
+ else {
+ throw new AssertionError("not yet supported space: " + space.toString());
+ }
+ }
+ };
+ }
+
+ @Override
+ public String printableSummary() {
+ StringBuilder result = new StringBuilder();
+ for (SymZ3Space space : spaceMap.values()) {
+ result.append(space.printableSummary());
+ }
+ result.append(this.preconditions.printableSummary());
+ return result.toString();
+ }
+
+ @Override
+ public Map getRegisterValues() {
+ throw new UnsupportedOperationException();
+ }
+
+ @Override
+ public void clear() {
+ /**
+ * In addition to clearing out all the state, you would probably also want to clear the
+ * instruction and op lists.
+ */
+ throw new UnsupportedOperationException();
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3Preconditions.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3Preconditions.java
new file mode 100644
index 0000000000..17af9f7a8f
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3Preconditions.java
@@ -0,0 +1,75 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.plain;
+
+import java.util.*;
+import java.util.stream.Stream;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * Store not related to a specific space for the Symbolic Summary Z3
+ *
+ *
+ * This information is available to any {@link SymZ3Space} and is shared across them
+ */
+public class SymZ3Preconditions {
+ private final List preconditions = new ArrayList<>();
+
+ public void addPrecondition(String r) {
+ preconditions.add(r);
+ }
+
+ public String printableSummary() {
+ StringBuilder result = new StringBuilder();
+ if (preconditions.isEmpty()) {
+ result.append("NO PRECONDITIONS");
+ result.append(System.lineSeparator());
+ return result.toString();
+ }
+ result.append("PRECONDITIONS:");
+ result.append(System.lineSeparator());
+ try (Context ctx = new Context()) {
+ Z3InfixPrinter z3p = new Z3InfixPrinter(ctx);
+ for (String b : preconditions) {
+ BoolExpr be = SymValueZ3.deserializeBoolExpr(ctx, b);
+ be = (BoolExpr) be.simplify();
+ result.append("" + z3p.infix(be));
+ result.append(System.lineSeparator());
+ }
+ }
+ return result.toString();
+ }
+
+ public List getPreconditions() {
+ return Collections.unmodifiableList(preconditions);
+ }
+
+ public Stream streamPreconditions(Context ctx, Z3InfixPrinter z3p) {
+ return preconditions.stream().map(b -> {
+ BoolExpr be = SymValueZ3.deserializeBoolExpr(ctx, b);
+ return z3p.infix(be.simplify());
+ });
+ }
+
+ public void clear() {
+ preconditions.clear();
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3RegisterSpace.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3RegisterSpace.java
new file mode 100644
index 0000000000..111cfbdc70
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3RegisterSpace.java
@@ -0,0 +1,94 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.plain;
+
+import java.util.Map.Entry;
+import java.util.stream.Stream;
+
+import com.microsoft.z3.Context;
+
+import ghidra.pcode.emu.symz3.SymZ3RegisterMap;
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.program.model.address.AddressSpace;
+import ghidra.program.model.lang.Language;
+import ghidra.program.model.lang.Register;
+import ghidra.symz3.model.SymValueZ3;
+import ghidra.util.Msg;
+
+/**
+ * The storage space for registers in a SymZ3Space
+ *
+ *
+ * The SymZ3Space is partitioned into separate storage spaces for registers, memory, etc. As such,
+ * when the space is used for more complex emulators (e.g., based on trace) This class is not
+ * extended. E.g., there exists a TraceSymZ3Space that derives from SymZ3Space, but the individual
+ * pieces use composition instead of inheritance. E.g., most all of the functionality is delegated
+ * to the SymZ3RegisterMap and there is just a bit of plumbing here.
+ */
+public class SymZ3RegisterSpace extends SymZ3Space {
+ private final SymZ3RegisterMap rmap = new SymZ3RegisterMap();
+
+ private final AddressSpace space;
+ private final Language language;
+
+ public SymZ3RegisterSpace(AddressSpace space, Language language) {
+ super();
+ this.space = space;
+ this.language = language;
+ }
+
+ @Override
+ public String printableSummary() {
+ return rmap.printableSummary();
+ }
+
+ @Override
+ public Stream> streamValuations(Context ctx, Z3InfixPrinter z3p) {
+ return rmap.streamValuations(ctx, z3p);
+ }
+
+ private Register getRegister(SymValueZ3 offset, int size) {
+ Long offsetLong = offset.toLong();
+ if (offsetLong == null) {
+ throw new AssertionError(
+ "getRegister was given a symbolic register, should not be possible");
+ }
+ return language.getRegister(space, offset.toLong(), size);
+ }
+
+ @Override
+ public void set(SymValueZ3 offset, int size, SymValueZ3 val) {
+ Register r = getRegister(offset, size);
+ if (r == null) {
+ Msg.warn(this, "set is ignoring set register with offset: " + offset + " and size: " +
+ size + " to: " + val);
+ return;
+ }
+ this.rmap.updateRegister(r, val);
+ }
+
+ @Override
+ public SymValueZ3 get(SymValueZ3 offset, int size) {
+ Register r = getRegister(offset, size);
+ if (r == null) {
+ Msg.warn(this, "unable to get register with space: " + space.getSpaceID() +
+ " offset_long: " + offset + " size: " + size);
+ return null;
+ }
+ SymValueZ3 result = this.rmap.getRegister(r);
+ return result;
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3Space.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3Space.java
new file mode 100644
index 0000000000..3bb728ff77
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3Space.java
@@ -0,0 +1,43 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.plain;
+
+import java.util.Map;
+import java.util.stream.Stream;
+
+import com.microsoft.z3.Context;
+
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * The storage space for symbolic values
+ *
+ * This is the actual implementation of the in-memory storage for symbolic z3 values. For a
+ * stand-alone emulator, this is the full state. For a trace- or Debugger-integrated emulator, this
+ * is a cache of values loaded from a trace backing this emulator. Most likely, that trace is the
+ * user's current trace.
+ */
+public abstract class SymZ3Space {
+ public abstract void set(SymValueZ3 offset, int size, SymValueZ3 val);
+
+ public abstract SymValueZ3 get(SymValueZ3 offset, int size);
+
+ public abstract String printableSummary();
+
+ public abstract Stream> streamValuations(Context ctx,
+ Z3InfixPrinter z3p);
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3UniqueSpace.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3UniqueSpace.java
new file mode 100644
index 0000000000..f8022ad221
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/SymZ3UniqueSpace.java
@@ -0,0 +1,98 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.plain;
+
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.stream.Stream;
+
+import com.microsoft.z3.*;
+
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * The storage space for unique registers
+ *
+ *
+ * This is the actual implementation of the in-memory storage for symbolic z3 values. For a
+ * stand-alone emulator, this is the full state. For a trace- or Debugger-integrated emulator, this
+ * is a cache of values loaded from a trace backing this emulator. Most likely, that trace is the
+ * user's current trace.
+ */
+public class SymZ3UniqueSpace extends SymZ3Space {
+ private final Map uniqvals = new HashMap();;
+
+ private String label(long offset, int size) {
+ return "" + offset + ":" + size;
+ }
+
+ public void set(long offset, int size, SymValueZ3 val) {
+ this.updateUnique(label(offset, size), val);
+ }
+
+ public SymValueZ3 get(long offset, int size) {
+ return this.getUnique(label(offset, size));
+ }
+
+ public void updateUnique(String s, SymValueZ3 value) {
+ uniqvals.put(s, value);
+ }
+
+ public SymValueZ3 getUnique(String s) {
+ return uniqvals.get(s);
+ }
+
+ @Override
+ public String printableSummary() {
+ return "";
+ }
+
+ @Override
+ public Stream> streamValuations(Context ctx, Z3InfixPrinter z3p) {
+ return Stream.of();
+ }
+
+ @Override
+ public void set(SymValueZ3 offset, int size, SymValueZ3 val) {
+ assert val != null;
+ try (Context ctx = new Context()) {
+ BitVecExpr b = offset.getBitVecExpr(ctx);
+ if (b.isNumeral()) {
+ BitVecNum bvn = (BitVecNum) b;
+ this.set(bvn.getLong(), size, val);
+ }
+ else {
+ throw new AssertionError("how can we have a symbolic offset for a unique set:" +
+ offset + "is numeral? " + b.isNumeral() + " is BV numeral: " + b.isBVNumeral());
+ }
+ }
+ }
+
+ @Override
+ public SymValueZ3 get(SymValueZ3 offset, int size) {
+ assert offset != null;
+ try (Context ctx = new Context()) {
+ BitVecExpr b = offset.getBitVecExpr(ctx);
+ if (b.isNumeral()) {
+ BitVecNum bvn = (BitVecNum) b;
+ return this.get(bvn.getLong(), size);
+ }
+ throw new AssertionError("how can we have a symbolic offset for unique get?");
+ }
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/package-info.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/package-info.java
new file mode 100644
index 0000000000..dd487e3398
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/plain/package-info.java
@@ -0,0 +1,34 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+/**
+ * The stand-alone Symbolic Z3 Emulator
+ *
+ *
+ * This and the {@link ghidra.pcode.emu.symz3} packages contain all the parts necessary to construct
+ * a stand-alone emulator. Because this is a working solution, the state components already have
+ * provisions in place for extension to support the fully-integrated solution. Generally, it's a bit
+ * easier to just get the basic state components implemented, put tests in place, and then re-factor
+ * them to permit extension as you address each more integrated emulator.
+ *
+ *
+ * For this package, I recommend a top-down approach, since the top component provides a flat
+ * catalog of the lower components. That top piece is actually in a separate package. See
+ * {@link ghidra.pcode.emu.symz3.SymZ3PartsFactory}. That factory is then used in
+ * {@link ghidra.pcode.emu.symz3.plain.SymZ3PcodeEmulator} to realize the stand-alone emulator. When
+ * you get to the state pieces, you may want to pause and read
+ * {@link ghidra.pcode.emu.symz3.plain.SymZ3Space} first.
+ */
+package ghidra.pcode.emu.symz3.plain;
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/AbstractSymZ3TracePcodeExecutorStatePiece.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/AbstractSymZ3TracePcodeExecutorStatePiece.java
new file mode 100644
index 0000000000..cb3217a606
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/AbstractSymZ3TracePcodeExecutorStatePiece.java
@@ -0,0 +1,125 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.trace;
+
+import ghidra.pcode.emu.symz3.AbstractSymZ3PcodeExecutorStatePiece;
+import ghidra.pcode.emu.symz3.SymZ3PcodeArithmetic;
+import ghidra.pcode.exec.trace.TracePcodeExecutorStatePiece;
+import ghidra.pcode.exec.trace.data.PcodeTraceDataAccess;
+import ghidra.pcode.exec.trace.data.PcodeTracePropertyAccess;
+import ghidra.program.model.address.AddressSpace;
+import ghidra.program.model.lang.Language;
+import ghidra.symz3.model.SymValueZ3;
+import ghidra.trace.model.property.TracePropertyMapSpace;
+
+/**
+ * An abstract trace-integrated state piece
+ *
+ *
+ * See {@link AbstractSymZ3TracePcodeExecutorStatePiece} for framing. This class must remain
+ * abstract since we need to derive the Debugger-integrated state piece from it. Thus it tightens
+ * the bound on {@code } and introduces the parameters necessary to source state from a trace.
+ * We'll store SymValueZ3s in the trace's address property map, which is the recommended scheme for
+ * auxiliary state.
+ */
+public abstract class AbstractSymZ3TracePcodeExecutorStatePiece
+ extends AbstractSymZ3PcodeExecutorStatePiece
+ implements TracePcodeExecutorStatePiece {
+ public static final String NAME = "SymValueZ3";
+
+ protected final PcodeTraceDataAccess data;
+ protected final PcodeTracePropertyAccess property;
+
+ /**
+ * Create a state piece
+ *
+ * @param data the trace-data access shim
+ */
+ public AbstractSymZ3TracePcodeExecutorStatePiece(PcodeTraceDataAccess data) {
+ super(data.getLanguage(),
+ SymZ3PcodeArithmetic.forLanguage(data.getLanguage()),
+ SymZ3PcodeArithmetic.forLanguage(data.getLanguage()));
+ this.data = data;
+ this.property = data.getPropertyAccess(NAME, String.class);
+ }
+
+ @Override
+ public PcodeTraceDataAccess getData() {
+ return data;
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * Here we create a map that uses {@link SymZ3TraceSpace}s. The framework provides the concept
+ * of a space map where storage is actually a cache backed by some other object. The backing
+ * object we'll use here is {@link TracePropertyMapSpace}, which is provided by the
+ * TraceModeling module. We'll need a little bit of extra logic for fetching a register space
+ * vs. a plain memory space, but after that, we need not care which address space the backing
+ * object is for.
+ */
+ @Override
+ protected AbstractSpaceMap newSpaceMap(Language language) {
+ return new CacheingSpaceMap, SymZ3TraceSpace>() {
+ @Override
+ protected PcodeTracePropertyAccess getBacking(AddressSpace space) {
+ return property;
+ }
+
+ @Override
+ protected SymZ3TraceSpace newSpace(AddressSpace space,
+ PcodeTracePropertyAccess backing) {
+
+ if (space.isConstantSpace()) {
+ throw new AssertionError(
+ "request for a trace constant space needs to be implemented");
+ //return new SymZ3TraceConstantSpace(backing, snap);
+ }
+ else if (space.isRegisterSpace()) {
+ return new SymZ3TraceRegisterSpace(space, backing);
+ }
+ else if (space.isUniqueSpace()) {
+ return new SymZ3TraceUniqueSpace(space, backing);
+ }
+ else if (space.isLoadedMemorySpace()) {
+ return new SymZ3TraceMemorySpace(space, backing);
+
+ }
+ else {
+ throw new AssertionError("not yet supported space: " + space.toString());
+ }
+
+ }
+ };
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * This does the inverse of the lazy loading. Serialize the state and store it back into the
+ * trace. Technically, it could be a different trace, but it must have identically-named
+ * threads.
+ */
+ @Override
+ public void writeDown(PcodeTraceDataAccess into) {
+ PcodeTracePropertyAccess intoProp = into.getPropertyAccess(NAME, String.class);
+ for (SymZ3TraceSpace space : spaceMap.values()) {
+ space.writeDown(intoProp);
+ }
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TraceMemorySpace.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TraceMemorySpace.java
new file mode 100644
index 0000000000..8196a25374
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TraceMemorySpace.java
@@ -0,0 +1,105 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.trace;
+
+import java.math.BigInteger;
+import java.util.Map.Entry;
+import java.util.stream.Stream;
+
+import com.microsoft.z3.Context;
+
+import ghidra.pcode.emu.symz3.SymZ3MemoryMap;
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.pcode.exec.trace.data.PcodeTracePropertyAccess;
+import ghidra.program.model.address.*;
+import ghidra.symz3.model.SymValueZ3;
+import ghidra.util.Msg;
+
+public class SymZ3TraceMemorySpace extends SymZ3TraceSpace {
+ private final SymZ3MemoryMap mmap = new SymZ3MemoryMap(property.getLanguage());;
+
+ public SymZ3TraceMemorySpace(AddressSpace space, PcodeTracePropertyAccess property) {
+ super(space, property);
+ }
+
+ public SymValueZ3 extractionHelper(String string, int size) {
+ throw new AssertionError("need to implement extraction from: " + string);
+ }
+
+ public SymValueZ3 whenMissing(SymValueZ3 offset, int size) {
+ if (!this.property.hasSpace(space)) {
+ // our map will create a symbolic value
+ Msg.info(this, "no backing, so our map created a missing symbolic value");
+ return mmap.load(offset, size, true);
+ }
+ // if the address is concrete, we fetch using the address
+ BigInteger bi = offset.toBigInteger();
+ if (bi == null) {
+ String string = this.property.get(Address.NO_ADDRESS);
+ if (string != null) {
+ Msg.info(this, "fetch from memory using the backing but symbolic address");
+ return extractionHelper(string, size);
+ }
+ }
+ else {
+ try {
+ Address addr = space.getAddress(bi.toString(16));
+ String string = this.property.get(addr);
+ if (string != null) {
+ Msg.info(this, "fetch from memory using the backing and concrete address: " +
+ addr + " deserializing: " + string);
+ SymValueZ3 result = SymValueZ3.parse(string);
+ Msg.info(this, "with result: " + result);
+ return result;
+ }
+ }
+ catch (AddressFormatException e) {
+ ;
+ }
+ }
+ Msg.info(this,
+ "we had a backing, but couldn't find the address, using map to create symbolic value");
+ return mmap.load(offset, size, true);
+ }
+
+ @Override
+ public SymValueZ3 get(SymValueZ3 offset, int size) {
+ if (mmap.hasValueFor(offset, size)) {
+ return mmap.load(offset, size, true);
+ }
+ return whenMissing(offset, size);
+ }
+
+ @Override
+ public void set(SymValueZ3 offset, int size, SymValueZ3 val) {
+ mmap.store(offset, size, val);
+ }
+
+ @Override
+ public String printableSummary() {
+ return mmap.printableSummary();
+ }
+
+ @Override
+ public Stream> streamValuations(Context ctx, Z3InfixPrinter z3p) {
+ return mmap.streamValuations(ctx, z3p);
+ }
+
+ @Override
+ public void writeDown(PcodeTracePropertyAccess into) {
+ SymZ3WriteDownHelper.writeDown(mmap, this.space, into);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TracePcodeEmulator.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TracePcodeEmulator.java
new file mode 100644
index 0000000000..2b17044ea6
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TracePcodeEmulator.java
@@ -0,0 +1,81 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.trace;
+
+import java.util.Collection;
+
+import ghidra.pcode.emu.symz3.*;
+import ghidra.pcode.emu.symz3.plain.SymZ3PcodeEmulator;
+import ghidra.pcode.exec.trace.auxiliary.AuxTraceEmulatorPartsFactory;
+import ghidra.pcode.exec.trace.auxiliary.AuxTracePcodeEmulator;
+import ghidra.pcode.exec.trace.data.PcodeTraceAccess;
+import ghidra.symz3.model.SymValueZ3;
+import ghidra.trace.model.guest.TracePlatform;
+
+/**
+ * A trace-integrated emulator with symbolic value analysis
+ */
+public class SymZ3TracePcodeEmulator extends AuxTracePcodeEmulator
+ implements SymZ3PcodeEmulatorTrait {
+ /**
+ * Create an emulator
+ *
+ * @param access the trace access shim
+ */
+ public SymZ3TracePcodeEmulator(PcodeTraceAccess access) {
+ super(access);
+ }
+
+ public SymZ3TracePcodeEmulator(TracePlatform platform, long snap) {
+ super(platform, snap);
+ }
+
+ /**
+ * {@inheritDoc}
+ *
+ *
+ * Here, we just return the singleton parts factory. This appears simple because all the
+ * complexity is encapsulated in the factory. See {@link SymZ3PartsFactory} to see everything
+ * the implementation actually entails. Notice that this is the same parts factory used by
+ * {@link SymZ3PcodeEmulator}. The {@link AuxTracePcodeEmulator} knows to use the more capable
+ * state parts.
+ */
+ @Override
+ protected AuxTraceEmulatorPartsFactory getPartsFactory() {
+ return SymZ3PartsFactory.INSTANCE;
+ }
+
+ @Override
+ public SymZ3PcodeThread newThread() {
+ return (SymZ3PcodeThread) super.newThread();
+ }
+
+ @Override
+ public SymZ3PcodeThread newThread(String name) {
+ return (SymZ3PcodeThread) super.newThread(name);
+ }
+
+ @Override
+ @SuppressWarnings("unchecked")
+ public Collection getAllThreads() {
+ return (Collection) super.getAllThreads();
+ }
+
+ @Override
+ public SymZ3PairedPcodeExecutorState getSharedState() {
+ return (SymZ3PairedPcodeExecutorState) super.getSharedState();
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TracePcodeExecutorState.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TracePcodeExecutorState.java
new file mode 100644
index 0000000000..8525f72a6c
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TracePcodeExecutorState.java
@@ -0,0 +1,63 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.trace;
+
+import ghidra.pcode.emu.symz3.SymZ3PairedPcodeExecutorState;
+import ghidra.pcode.emu.symz3.plain.SymZ3PcodeExecutorState;
+import ghidra.pcode.exec.trace.BytesTracePcodeExecutorStatePiece;
+import ghidra.pcode.exec.trace.IndependentPairedTracePcodeExecutorState;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * A paired concrete-plus-symz3 trace-integrated state
+ *
+ *
+ * This contains the emulator's machine state along with the symbolic values, just like
+ * {@link SymZ3PcodeExecutorState}, except that it can read and write state from a trace. In
+ * reality, this just composes concrete and symz3 state pieces, which actually do all the work.
+ */
+public class SymZ3TracePcodeExecutorState
+ extends IndependentPairedTracePcodeExecutorState
+ implements SymZ3PairedPcodeExecutorState {
+
+ /**
+ * Create a state from the two given pieces
+ *
+ * @param concrete the concrete piece
+ * @param symz3 the symz3 piece
+ */
+ public SymZ3TracePcodeExecutorState(BytesTracePcodeExecutorStatePiece concrete,
+ AbstractSymZ3TracePcodeExecutorStatePiece symz3) {
+ super(concrete, symz3);
+ }
+
+ /**
+ * Create a state from the given concrete piece and an internally constructed symz3 piece
+ *
+ *
+ * We take all the parameters needed by the symz3 piece from the concrete piece.
+ *
+ * @param concrete the concrete piece
+ */
+ public SymZ3TracePcodeExecutorState(BytesTracePcodeExecutorStatePiece concrete) {
+ this(concrete, new SymZ3TracePcodeExecutorStatePiece(concrete.getData()));
+ }
+
+ @Override
+ public SymZ3TracePcodeExecutorStatePiece getRight() {
+ return (SymZ3TracePcodeExecutorStatePiece) super.getRight();
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TracePcodeExecutorStatePiece.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TracePcodeExecutorStatePiece.java
new file mode 100644
index 0000000000..b15a8fbeba
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TracePcodeExecutorStatePiece.java
@@ -0,0 +1,49 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.trace;
+
+import java.util.Map;
+
+import ghidra.pcode.exec.trace.TracePcodeExecutorStatePiece;
+import ghidra.pcode.exec.trace.data.PcodeTraceDataAccess;
+import ghidra.program.model.lang.Register;
+import ghidra.symz3.model.SymValueZ3;
+
+/**
+ * The trace-integrated state piece for holding symbolic values
+ */
+public class SymZ3TracePcodeExecutorStatePiece
+ extends AbstractSymZ3TracePcodeExecutorStatePiece {
+
+ public SymZ3TracePcodeExecutorStatePiece(PcodeTraceDataAccess data) {
+ super(data);
+ }
+
+ @Override
+ public TracePcodeExecutorStatePiece fork() {
+ throw new UnsupportedOperationException();
+ }
+
+ @Override
+ public Map getRegisterValues() {
+ throw new UnsupportedOperationException();
+ }
+
+ @Override
+ public void clear() {
+ throw new UnsupportedOperationException();
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TraceRegisterSpace.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TraceRegisterSpace.java
new file mode 100644
index 0000000000..c8862b05df
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TraceRegisterSpace.java
@@ -0,0 +1,115 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.trace;
+
+import java.util.Map.Entry;
+import java.util.stream.Stream;
+
+import com.microsoft.z3.Context;
+
+import ghidra.pcode.emu.symz3.SymZ3RegisterMap;
+import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
+import ghidra.pcode.exec.trace.data.PcodeTracePropertyAccess;
+import ghidra.program.model.address.AddressSpace;
+import ghidra.program.model.lang.Language;
+import ghidra.program.model.lang.Register;
+import ghidra.symz3.model.SymValueZ3;
+import ghidra.util.Msg;
+
+/**
+ * The storage space for symbolic values in the register space, possibly obtained from a trace
+ *
+ *
+ * This is the actual implementation of the in-memory storage for symbolic z3 values. For a
+ * stand-alone emulator, this is the full state. For a trace- or Debugger-integrated emulator, this
+ * is a cache of values loaded from a trace backing this emulator. Most likely, that trace is the
+ * user's current trace.
+ */
+public class SymZ3TraceRegisterSpace extends SymZ3TraceSpace {
+ private final SymZ3RegisterMap rmap = new SymZ3RegisterMap();
+ private final Language language = property.getLanguage();
+
+ public SymZ3TraceRegisterSpace(AddressSpace space, PcodeTracePropertyAccess property) {
+ super(space, property);
+ }
+
+ @Override
+ public String printableSummary() {
+ return rmap.printableSummary();
+ }
+
+ @Override
+ public Stream> streamValuations(Context ctx, Z3InfixPrinter z3p) {
+ return rmap.streamValuations(ctx, z3p);
+ }
+
+ public SymValueZ3 whenMissing(Register r) {
+ if (!this.property.hasSpace(space)) {
+ // our map will create a symbolic value
+ return rmap.getRegister(r);
+ }
+ String string = this.property.get(r.getAddress());
+ if (string == null) {
+ // our map will create a symbolic value
+ return rmap.getRegister(r);
+ }
+ return SymValueZ3.parse(string);
+ }
+
+ private Register getRegister(SymValueZ3 offset, int size) {
+ Long offsetLong = offset.toLong();
+ if (offsetLong == null) {
+ throw new AssertionError(
+ "getRegister was given a symbolic register, should not be possible");
+ }
+ return language.getRegister(space, offset.toLong(), size);
+ }
+
+ @Override
+ public void set(SymValueZ3 offset, int size, SymValueZ3 val) {
+ assert offset != null;
+ assert val != null;
+ Register r = getRegister(offset, size);
+ if (r == null) {
+ Msg.warn(this, "set is ignoring set register with offset: " + offset + " and size: " +
+ size + " to: " + val);
+ return;
+ }
+ rmap.updateRegister(r, val);
+ }
+
+ @Override
+ public SymValueZ3 get(SymValueZ3 offset, int size) {
+ assert offset != null;
+ Register r = getRegister(offset, size);
+ if (r == null) {
+ Msg.warn(this, "unable to get register with space: " + space.getSpaceID() +
+ " offset_long: " + offset + " size: " + size);
+ return null;
+ }
+ if (rmap.hasValueForRegister(r)) {
+ SymValueZ3 result = rmap.getRegister(r);
+ return result;
+ }
+ // attempt to get it from the backing
+ return whenMissing(r);
+ }
+
+ @Override
+ public void writeDown(PcodeTracePropertyAccess into) {
+ SymZ3WriteDownHelper.writeDown(rmap, into);
+ }
+}
diff --git a/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TraceSpace.java b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TraceSpace.java
new file mode 100644
index 0000000000..ade3a9d4c4
--- /dev/null
+++ b/Ghidra/Debug/SymbolicSummaryZ3/src/main/java/ghidra/pcode/emu/symz3/trace/SymZ3TraceSpace.java
@@ -0,0 +1,55 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.pcode.emu.symz3.trace;
+
+import ghidra.pcode.emu.symz3.plain.SymZ3Space;
+import ghidra.pcode.exec.trace.data.PcodeTracePropertyAccess;
+import ghidra.program.model.address.AddressSpace;
+
+/**
+ * The storage space for symbolic values in a trace's address space
+ *
+ *
+ * This adds to {@link SymZ3Space} the ability to load symbolic values from a trace and the ability
+ * to save them back into a trace.
+ */
+public abstract class SymZ3TraceSpace extends SymZ3Space {
+ protected final AddressSpace space;
+ protected final PcodeTracePropertyAccess