Merge remote-tracking branch

'origin/GP-5727_Dan_z3emu--SQUASHED'
This commit is contained in:
ghidra1 2025-06-30 09:51:02 -04:00
commit a483a4e28c
81 changed files with 7707 additions and 69 deletions

View file

@ -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 {
* <p>
* 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
*
* <p>
* To guarantee the emulator is present, call {@link #backgroundEmulate(Trace, TraceSchedule)}
* first.
* To guarantee the emulator is present, call
* {@link #backgroundEmulate(TracePlatform, TraceSchedule)} first.
* <p>
* <b>WARNING:</b> 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<CachedEmulator> getBusyEmulators();
/**
* Invalidate the trace's cache of emulated states.
*/
void invalidateCache();
/**
* Add a listener for emulator state changes
*

View file

@ -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<DebuggerPcodeEmulatorFactory> getEmulatorFactories() {
return ClassSearcher.getInstances(DebuggerPcodeEmulatorFactory.class);

View file

@ -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 <L> the type of values for the left state
* @param <R> the type of values for the right piece
* @see PairedPcodeExecutorState
*/
public class IndependentPairedTracePcodeExecutorState<L, R>
extends IndependentPairedPcodeExecutorState<L, R>
implements TracePcodeExecutorState<Pair<L, R>> {
private final TracePcodeExecutorStatePiece<L, L> left;
private final TracePcodeExecutorStatePiece<R, R> right;
public IndependentPairedTracePcodeExecutorState(TracePcodeExecutorStatePiece<L, L> left,
TracePcodeExecutorStatePiece<R, R> 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<L, R> fork() {
return new IndependentPairedTracePcodeExecutorState<>(left.fork(), right.fork());
}
}

View file

@ -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<T>
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<T>
ops.clear(span, toOverlay(ops, hostRange));
}
@Override
public boolean hasSpace(AddressSpace space) {
TracePropertyMapOperations<T> ops = getPropertyOperations(false);
if (ops == null) {
return false;
}
if (ops instanceof TracePropertyMapSpace<T> propSpace) {
return propSpace.getAddressSpace() == space;
}
if (ops instanceof TracePropertyMap<T> propMap) {
return propMap.getPropertyMapSpace(space, false) != null;
}
throw new AssertionError();
}
/**
* If this provides access to an overlay space, translate the physical address to it
*

View file

@ -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 <T> the type of the property's values
*/
public interface PcodeTracePropertyAccess<T> {
/**
* @see PcodeTraceDataAccess#getLanguage()
*/
Language getLanguage();
/**
* Get the property's value at the given address
*
@ -57,4 +62,18 @@ public interface PcodeTracePropertyAccess<T> {
* @param range the range
*/
void clear(AddressRange range);
/**
* Check if the trace has allocated property space for the given address space
*
* <p>
* 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);
}

View file

@ -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.

View file

@ -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)

View file

@ -0,0 +1,4 @@
##VERSION: 2.0
##MODULE IP: JSch License
Module.manifest||GHIDRA||||END|
README.md||GHIDRA||||END|

View file

@ -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
*
* <p>
* 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 <S> the type of an execute state space, internally associated with an address space
*/
public abstract class AbstractSymZ3OffsetPcodeExecutorStatePiece<S>
implements PcodeExecutorStatePiece<SymValueZ3, SymValueZ3> {
/**
* A map of address spaces to objects which store or cache state for that space
*
* @param <S> the type of object for each address space
*/
public abstract static class AbstractSpaceMap<S> {
protected final Map<AddressSpace, S> spaces = new HashMap<>();
public abstract S getForSpace(AddressSpace space, boolean toWrite);
public Collection<S> values() {
return spaces.values();
}
}
/**
* Use this when each S contains the complete state for the address space
*
* @param <S> the type of object for each address space
*/
public abstract static class SimpleSpaceMap<S> extends AbstractSpaceMap<S> {
/**
* Construct a new space internally associated with the given address space
*
* <p>
* 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 <B> the type of the object backing the cache for each address space
* @param <S> the type of cache for each address space
*/
public abstract static class CacheingSpaceMap<B, S> extends AbstractSpaceMap<S> {
/**
* 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
*
* <p>
* 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<SymValueZ3> addressArithmetic;
protected final PcodeArithmetic<SymValueZ3> 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<SymValueZ3> addressArithmetic, PcodeArithmetic<SymValueZ3> arithmetic) {
this.language = language;
this.addressArithmetic = addressArithmetic;
this.arithmetic = arithmetic;
uniqueSpace = language.getAddressFactory().getUniqueSpace();
}
@Override
public Language getLanguage() {
return language;
}
@Override
public PcodeArithmetic<SymValueZ3> getAddressArithmetic() {
return addressArithmetic;
}
@Override
public PcodeArithmetic<SymValueZ3> getArithmetic() {
return arithmetic;
}
/**
* Set a value in the unique space
*
* <p>
* 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.
*
* <p>
* 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);
}
}

View file

@ -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
*
* <p>
* 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 <S>}. 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 <S>}
* bounded, but unspecified.
*
* @param <S> the type of spaces
*/
public abstract class AbstractSymZ3PcodeExecutorStatePiece<S extends SymZ3Space>
extends AbstractSymZ3OffsetPcodeExecutorStatePiece<S>
implements InternalSymZ3RecordsPreconditions, InternalSymZ3RecordsExecution {
/**
* The map from address space to storage space
*
* <p>
* 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<S> 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<RecOp> ops = new ArrayList<RecOp>();
protected final List<RecInstruction> instructions = new ArrayList<RecInstruction>();
/**
* 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<SymValueZ3> addressArithmetic, PcodeArithmetic<SymValueZ3> arithmetic) {
super(language, addressArithmetic, arithmetic);
}
/**
* Extension point: Create the actual space map
*
* <p>
* This will need to be implemented by each state piece, i.e., non-abstract derivating class.
* The space map will provide instances of {@code <S>}, which will provide the actual (extended)
* storage logic.
*
* @return the space map
*/
protected abstract AbstractSpaceMap<S> newSpaceMap(Language language);
@Override
public MemBuffer getConcreteBuffer(Address address, Purpose purpose) {
throw new ConcretionError("Cannot make Symbolic concrete", purpose);
}
/**
* {@inheritDoc}
*
* <p>
* 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}
*
* <p>
* Because the super class places no bound on {@code <S>}, 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}
*
* <p>
* Because the super class places no bound on {@code <S>}, 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<Map.Entry<String, String>> 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<RecInstruction> getInstructions() {
return Collections.unmodifiableList(instructions);
}
@Override
public void addOp(SymZ3PcodeThread thread, PcodeOp op) {
ops.add(new RecOp(ops.size(), thread, op));
}
@Override
public List<RecOp> getOps() {
return Collections.unmodifiableList(ops);
}
@Override
public List<String> getPreconditions() {
return preconditions.getPreconditions();
}
@Override
public void clear() {
spaceMap.spaces.clear();
preconditions.clear();
ops.clear();
instructions.clear();
}
protected Stream<String> streamPreconditions(Context ctx, Z3InfixPrinter z3p) {
return preconditions.streamPreconditions(ctx, z3p);
}
}

View file

@ -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);
}

View file

@ -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);
}

View file

@ -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));
}
}

View file

@ -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
*
* <p>
* <b>NOTE: DELIBERATELY NO KNOWLEDGE OF SPACES, Languages, or "get" and "set"
* <p>
* 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.
* <p>
* In terms of storage, we have two options:
* <p>
* 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.
* <p>
* 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].
* <p>
* 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:
*
* <pre>
* MEM[RAX]:8 = extract(RBX,?,?)
* MEM[RAX+1]:8 = extract(RBX,?,?)
* </pre>
* <p>
* 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<String, SymValueZ3> memvals;
private List<Z3MemoryWitness> witnesses;
private Language language;
private static final boolean USE_BYTE_MODEL = true;
public static FuncDecl<BitVecSort> 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<String, SymValueZ3>();
this.language = language;
witnesses = new ArrayList<Z3MemoryWitness>();
}
protected Entry<String, String> valuationForMemval(Context ctx, Z3InfixPrinter z3p,
Entry<String, SymValueZ3> 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<String, String> valuationForWitness(Context ctx, Z3InfixPrinter z3p,
Set<BitVecExpr> 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<String, SymValueZ3> 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<BitVecExpr> reported = new ArrayList<BitVecExpr>();
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<Entry<String, String>> streamValuations(Context ctx, Z3InfixPrinter z3p) {
Stream<Entry<String, String>> forMemVals = memvals.entrySet().stream().map(entry -> {
return valuationForMemval(ctx, z3p, entry);
});
Set<BitVecExpr> reported = new HashSet<>();
Stream<Entry<String, String>> forWitnesses = witnesses.stream().mapMulti((w, mapper) -> {
Entry<String, String> 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<BitVecSort> 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<BitVecExpr> result_pieces = new ArrayList<BitVecExpr>();
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<BitVecSort> 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;
}
}

View file

@ -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<Pair<byte[], SymValueZ3>> {
PcodeExecutorStatePiece<byte[], byte[]> getLeft();
AbstractSymZ3PcodeExecutorStatePiece<? extends SymZ3Space> getRight();
}

View file

@ -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
*
* <p>
* 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}.
*
* <p>
* 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:
* <ul>
* <li>P-code Arithmetic: {@link SymZ3PcodeArithmetic}</li>
* <li>Userop Library: {@link SymZ3PcodeUseropLibrary}</li>
* <li>P-code Executor: {@link SymZ3PcodeThreadExecutor}</li>
* <li>Machine State</li>
* <ul>
* <li>Stand alone: {@link SymZ3PcodeExecutorState}</li>
* <li>Trace integrated: {@link SymZ3TracePcodeExecutorState}</li>
* <li>Debugger integrated: Not applicable. Uses trace integration only.</li>
* </ul>
* </ul>
*
* <p>
* 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<SymValueZ3> {
/** This singleton factory instance */
INSTANCE;
/**
* {@inheritDoc}
*
* <p>
* Here we simply return the arithmetic for symbolic values for the emulator's language.
*/
@Override
public PcodeArithmetic<SymValueZ3> getArithmetic(Language language) {
return SymZ3PcodeArithmetic.forLanguage(language);
}
/**
* {@inheritDoc}
*
* <p>
* 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<Pair<byte[], SymValueZ3>> createSharedUseropLibrary(
AuxPcodeEmulator<SymValueZ3> emulator) {
return new SymZ3PcodeUseropLibrary();
}
/**
* {@inheritDoc}
*
* <p>
* 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<Pair<byte[], SymValueZ3>> createLocalUseropStub(
AuxPcodeEmulator<SymValueZ3> emulator) {
return PcodeUseropLibrary.nil();
}
/**
* {@inheritDoc}
*
* <p>
* We have no thread-specific userops to add, so here we just return the empty library.
*/
@Override
public PcodeUseropLibrary<Pair<byte[], SymValueZ3>> createLocalUseropLibrary(
AuxPcodeEmulator<SymValueZ3> emulator, PcodeThread<Pair<byte[], SymValueZ3>> thread) {
return PcodeUseropLibrary.nil();
}
@Override
public PcodeThread<Pair<byte[], SymValueZ3>> createThread(AuxPcodeEmulator<SymValueZ3> emulator,
String name) {
return new SymZ3PcodeThread(name, emulator);
}
/**
* {@inheritDoc}
*
* <p>
* We'd like to instrument conditional branches to record preconditions, so we'll need a custom
* executor. We construct it here.
*/
@Override
public PcodeThreadExecutor<Pair<byte[], SymValueZ3>> createExecutor(
AuxPcodeEmulator<SymValueZ3> emulator,
DefaultPcodeThread<Pair<byte[], SymValueZ3>> thread) {
return new SymZ3PcodeThreadExecutor((SymZ3PcodeThread) thread);
}
@Override
public PcodeExecutorState<Pair<byte[], SymValueZ3>> createSharedState(
AuxPcodeEmulator<SymValueZ3> emulator, BytesPcodeExecutorStatePiece concrete) {
return new SymZ3PcodeExecutorState(emulator.getLanguage(), concrete);
}
@Override
public PcodeExecutorState<Pair<byte[], SymValueZ3>> createLocalState(
AuxPcodeEmulator<SymValueZ3> emulator, PcodeThread<Pair<byte[], SymValueZ3>> thread,
BytesPcodeExecutorStatePiece concrete) {
return new SymZ3PcodeExecutorState(emulator.getLanguage(), concrete);
}
@Override
public TracePcodeExecutorState<Pair<byte[], SymValueZ3>> createTraceSharedState(
AuxTracePcodeEmulator<SymValueZ3> emulator,
BytesTracePcodeExecutorStatePiece concrete) {
return new SymZ3TracePcodeExecutorState(concrete);
}
@Override
public TracePcodeExecutorState<Pair<byte[], SymValueZ3>> createTraceLocalState(
AuxTracePcodeEmulator<SymValueZ3> emulator,
PcodeThread<Pair<byte[], SymValueZ3>> emuThread,
BytesTracePcodeExecutorStatePiece concrete) {
return new SymZ3TracePcodeExecutorState(concrete);
}
@Override
public TracePcodeExecutorState<Pair<byte[], SymValueZ3>> createDebuggerSharedState(
AuxDebuggerPcodeEmulator<SymValueZ3> emulator,
RWTargetMemoryPcodeExecutorStatePiece concrete) {
return new SymZ3TracePcodeExecutorState(concrete);
}
@Override
public TracePcodeExecutorState<Pair<byte[], SymValueZ3>> createDebuggerLocalState(
AuxDebuggerPcodeEmulator<SymValueZ3> emulator,
PcodeThread<Pair<byte[], SymValueZ3>> emuThread,
RWTargetRegistersPcodeExecutorStatePiece concrete) {
return new SymZ3TracePcodeExecutorState(concrete);
}
}

View file

@ -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<SymValueZ3> {
/** 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
*
* <p>
* 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
*
* <p>
* 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;
}
}

View file

@ -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<Pair<byte[], SymValueZ3>>, SymZ3RecordsExecution {
@Override
SymZ3PcodeThread newThread();
@Override
SymZ3PcodeThread newThread(String name);
@Override
Collection<? extends SymZ3PcodeThread> getAllThreads();
@Override
SymZ3PairedPcodeExecutorState getSharedState();
default AbstractSymZ3PcodeExecutorStatePiece<? extends SymZ3Space> getSharedSymbolicState() {
return getSharedState().getRight();
}
@Override
default List<RecInstruction> getInstructions() {
return getSharedSymbolicState().getInstructions();
}
@Override
default List<RecOp> 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<RecOp> 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<String> streamPreconditions(Context ctx, Z3InfixPrinter z3p) {
Stream<String> shared = getSharedState().getRight().streamPreconditions(ctx, z3p);
Stream<String> locals = getAllThreads().stream()
.flatMap(t -> t.getLocalSymbolicState().streamPreconditions(ctx, z3p));
return Stream.concat(shared, locals);
}
default Stream<Entry<String, String>> streamValuations(Context ctx, Z3InfixPrinter z3p) {
Stream<Entry<String, String>> shared =
getSharedState().getRight().streamValuations(ctx, z3p);
Stream<Entry<String, String>> locals = getAllThreads().stream()
.flatMap(t -> t.getLocalSymbolicState().streamValuations(ctx, z3p));
return Stream.concat(shared, locals);
}
}

View file

@ -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<SymValueZ3>
implements InternalSymZ3RecordsPreconditions {
public SymZ3PcodeThread(String name, AuxPcodeEmulator<SymValueZ3> emulator) {
super(name, emulator);
}
@Override
protected SleighInstructionDecoder createInstructionDecoder(
PcodeExecutorState<Pair<byte[], SymValueZ3>> 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<Pair<byte[], SymValueZ3>> createThreadState(
PcodeExecutorState<Pair<byte[], SymValueZ3>> sharedState,
PcodeExecutorState<Pair<byte[], SymValueZ3>> localState) {
return new SymZ3ThreadPcodeExecutorState(sharedState, localState);
}
@Override
public SymZ3ThreadPcodeExecutorState getState() {
return (SymZ3ThreadPcodeExecutorState) super.getState();
}
public PcodeExecutorStatePiece<byte[], byte[]> getSharedConcreteState() {
return getState().getSharedState().getLeft();
}
public AbstractSymZ3PcodeExecutorStatePiece<? extends SymZ3Space> getSharedSymbolicState() {
return getState().getSharedState().getRight();
}
public PcodeExecutorStatePiece<byte[], byte[]> getLocalConcreteState() {
return getState().getLocalState().getLeft();
}
public AbstractSymZ3PcodeExecutorStatePiece<? extends SymZ3Space> getLocalSymbolicState() {
return getState().getLocalState().getRight();
}
@Override
public void addPrecondition(String precondition) {
getLocalSymbolicState().addPrecondition(precondition);
}
@Override
public List<String> 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<String, String> p = registerComparison(reg);
out.println(reg + " concrete: " + p.getLeft() + " whereas symbolic: " + p.getRight());
}
public ImmutablePair<String, String> registerComparison(String reg) {
Register register = getLanguage().getRegister(reg);
PcodeArithmetic<byte[]> 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<String, String> p = memoryComparisonRegPlusOffset(reg, offset);
out.println("MEM[" + reg + "+" + offset + "]" + " concrete: " + p.getLeft() +
" whereas symbolic: " + p.getRight());
}
public ImmutablePair<String, String> memoryComparisonRegPlusOffset(String reg, int offset) {
Language language = this.getLanguage();
Register register = language.getRegister(reg);
PcodeArithmetic<byte[]> 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));
}
}
}

View file

@ -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
*
* <p>
* 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<Pair<byte[], SymValueZ3>> {
/**
* 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<Pair<byte[], SymValueZ3>> library) {
getThread().addOp(op);
super.stepOp(op, frame, library);
}
/**
* {@inheritDoc}
*
* <p>
* 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<byte[], SymValueZ3> 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);
}
}

View file

@ -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<Pair<byte[], SymValueZ3>> {
}

View file

@ -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<RecInstruction> getInstructions();
public List<RecOp> getOps();
}

View file

@ -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<String> getPreconditions();
}

View file

@ -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 /*
* <p>
* <b>NOTE:</b> 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<Register, SymValueZ3> regvals = new HashMap<Register, SymValueZ3>();
//private List<String> createdSymbolics = new ArrayList<String>();
private final Set<String> registerNamesRead = new HashSet<String>();
private final Set<String> registerNamesUpdated = new HashSet<String>();
private final Map<String, Register> knownRegisters = new HashMap<String, Register>();
public List<String> getRegisterNamesRead() {
ArrayList<String> result = new ArrayList<String>(registerNamesRead);
Collections.sort(result);
return result;
}
public List<String> getRegisterNamesUpdated() {
ArrayList<String> result = new ArrayList<String>(registerNamesUpdated);
Collections.sort(result);
return result;
}
public List<String> getRegisterNamesReadOrUpdated() {
HashSet<String> both = new HashSet<String>(registerNamesRead);
both.addAll(registerNamesUpdated);
ArrayList<String> result = new ArrayList<String>(both);
Collections.sort(result);
return result;
}
public List<String> getRegisterNames() {
// make this recursive later and get children???
List<String> result = new ArrayList<String>();
for (Map.Entry<Register, SymValueZ3> 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<String, String> valuation = valuationFor(ctx, z3p, r);
return valuation.getKey() + " = " + valuation.getValue();
}
public Entry<String, String> 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<String> registersRead = this.getRegisterNamesRead();
result.append(z3p.fetchListOfStringsHelper(registersRead));
result.append("Registers that were updated: ");
result.append(System.lineSeparator());
List<String> registersUpdated = this.getRegisterNamesUpdated();
result.append(z3p.fetchListOfStringsHelper(registersUpdated));
result.append("Registers that were read or updated: ");
result.append(System.lineSeparator());
List<String> 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<Entry<String, String>> streamValuations(Context ctx, Z3InfixPrinter z3p) {
return getRegisterNamesReadOrUpdated().stream().map(n -> {
Register r = knownRegisters.get(n);
return valuationFor(ctx, z3p, r);
});
}
}

View file

@ -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<Pair<byte[], SymValueZ3>> {
public SymZ3ThreadPcodeExecutorState(PcodeExecutorState<Pair<byte[], SymValueZ3>> sharedState,
PcodeExecutorState<Pair<byte[], SymValueZ3>> localState) {
super(sharedState, localState);
}
@Override
public SymZ3PairedPcodeExecutorState getSharedState() {
return (SymZ3PairedPcodeExecutorState) super.getSharedState();
}
@Override
public SymZ3PairedPcodeExecutorState getLocalState() {
return (SymZ3PairedPcodeExecutorState) super.getLocalState();
}
}

View file

@ -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<SymValueZ3>
implements SymZ3PcodeEmulatorTrait {
/**
* Create an emulator
*
* @param access the trace-and-debugger access shim
*/
public SymZ3DebuggerPcodeEmulator(PcodeDebuggerAccess access) {
super(access);
}
/**
* {@inheritDoc}
*
* <p>
* 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<SymValueZ3> 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<? extends SymZ3PcodeThread> getAllThreads() {
return (Collection<? extends SymZ3PcodeThread>) super.getAllThreads();
}
@Override
public SymZ3PairedPcodeExecutorState getSharedState() {
return (SymZ3PairedPcodeExecutorState) super.getSharedState();
}
}

View file

@ -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
*
* <p>
* 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);
}
}

View file

@ -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<Pair<byte[], SymValueZ3>> {
/**
* A file whose contents have a SymValueZ3 piece
*/
public static class SymZ3EmuUnixFile extends AbstractEmuUnixFile<Pair<byte[], SymValueZ3>> {
protected BytesEmuFileContents concrete = new BytesEmuFileContents();
public SymZ3EmuUnixFile(String pathname, int mode) {
super(pathname, mode);
}
@Override
protected EmuFileContents<Pair<byte[], SymValueZ3>> createDefaultContents() {
// for now we leave the piece null
return new PairedEmuFileContents<>(concrete, null);
}
}
@Override
public AbstractEmuUnixFile<Pair<byte[], SymValueZ3>> newFile(String pathname, int mode)
throws EmuIOException {
return new SymZ3EmuUnixFile(pathname, mode);
}
}

View file

@ -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
*
* <p>
* This library is not currently accessible from the UI. It can be used with scripts by overriding a
* emulator's userop library factory method.
*
* <p>
* TODO: A means of adding and configuring userop libraries in the UI.
*
* <p>
* TODO: Example scripts.
*/
public class SymZ3LinuxAmd64SyscallLibrary
extends EmuLinuxAmd64SyscallUseropLibrary<Pair<byte[], SymValueZ3>> {
public SymZ3LinuxAmd64SyscallLibrary(PcodeMachine<Pair<byte[], SymValueZ3>> machine,
EmuUnixFileSystem<Pair<byte[], SymValueZ3>> fs, Program program, EmuUnixUser user) {
super(machine, fs, program, user);
}
public SymZ3LinuxAmd64SyscallLibrary(PcodeMachine<Pair<byte[], SymValueZ3>> machine,
EmuUnixFileSystem<Pair<byte[], SymValueZ3>> fs, Program program) {
super(machine, fs, program);
}
}

View file

@ -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<String> 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();
}
}

View file

@ -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
}
}

View file

@ -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.
*
* <p>
* 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<Entry<String, String>> streamValuations(Context ctx, Z3InfixPrinter z3p) {
return mmap.streamValuations(ctx, z3p);
}
}

View file

@ -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<SymValueZ3>
implements SymZ3PcodeEmulatorTrait {
/**
* Create an emulator
*
* @param language the language (processor model)
*/
public SymZ3PcodeEmulator(Language language) {
super(language);
}
/**
* {@inheritDoc}
*
* <p>
* 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<SymValueZ3> 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<? extends SymZ3PcodeThread> getAllThreads() {
return (Collection<? extends SymZ3PcodeThread>) super.getAllThreads();
}
@Override
public SymZ3PcodeExecutorState getSharedState() {
return (SymZ3PcodeExecutorState) super.getSharedState();
}
}

View file

@ -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
*
* <p>
* 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<byte[], SymValueZ3>
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<? extends SymZ3Space> getRight() {
return (SymZ3PcodeExecutorStatePiece) super.getRight();
}
}

View file

@ -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<SymZ3Space> {
/**
* 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<SymValueZ3> addressArithmetic) {
super(language, addressArithmetic, SymZ3PcodeArithmetic.forLanguage(language));
}
/**
* {@inheritDoc}
*
* <p>
* 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<SymZ3Space> newSpaceMap(Language language) {
return new SimpleSpaceMap<SymZ3Space>() {
@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<Register, SymValueZ3> 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();
}
}

View file

@ -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
*
* <p>
* This information is available to any {@link SymZ3Space} and is shared across them
*/
public class SymZ3Preconditions {
private final List<String> 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<String> getPreconditions() {
return Collections.unmodifiableList(preconditions);
}
public Stream<String> 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();
}
}

View file

@ -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
*
* <p>
* 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<Entry<String, String>> 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;
}
}

View file

@ -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
* <p>
* 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<Map.Entry<String, String>> streamValuations(Context ctx,
Z3InfixPrinter z3p);
}

View file

@ -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
*
* <p>
* 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<String, SymValueZ3> uniqvals = new HashMap<String, SymValueZ3>();;
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<Entry<String, String>> 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?");
}
}
}

View file

@ -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
*
* <p>
* 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.
*
* <p>
* 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;

View file

@ -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
*
* <p>
* 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 <S>} 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<SymZ3TraceSpace>
implements TracePcodeExecutorStatePiece<SymValueZ3, SymValueZ3> {
public static final String NAME = "SymValueZ3";
protected final PcodeTraceDataAccess data;
protected final PcodeTracePropertyAccess<String> 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}
*
* <p>
* 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<SymZ3TraceSpace> newSpaceMap(Language language) {
return new CacheingSpaceMap<PcodeTracePropertyAccess<String>, SymZ3TraceSpace>() {
@Override
protected PcodeTracePropertyAccess<String> getBacking(AddressSpace space) {
return property;
}
@Override
protected SymZ3TraceSpace newSpace(AddressSpace space,
PcodeTracePropertyAccess<String> 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}
*
* <p>
* 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<String> intoProp = into.getPropertyAccess(NAME, String.class);
for (SymZ3TraceSpace space : spaceMap.values()) {
space.writeDown(intoProp);
}
}
}

View file

@ -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<String> 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<Entry<String, String>> streamValuations(Context ctx, Z3InfixPrinter z3p) {
return mmap.streamValuations(ctx, z3p);
}
@Override
public void writeDown(PcodeTracePropertyAccess<String> into) {
SymZ3WriteDownHelper.writeDown(mmap, this.space, into);
}
}

View file

@ -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<SymValueZ3>
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}
*
* <p>
* 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<SymValueZ3> 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<? extends SymZ3PcodeThread> getAllThreads() {
return (Collection<? extends SymZ3PcodeThread>) super.getAllThreads();
}
@Override
public SymZ3PairedPcodeExecutorState getSharedState() {
return (SymZ3PairedPcodeExecutorState) super.getSharedState();
}
}

View file

@ -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
*
* <p>
* 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<byte[], SymValueZ3>
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
*
* <p>
* 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();
}
}

View file

@ -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<SymValueZ3, SymValueZ3> fork() {
throw new UnsupportedOperationException();
}
@Override
public Map<Register, SymValueZ3> getRegisterValues() {
throw new UnsupportedOperationException();
}
@Override
public void clear() {
throw new UnsupportedOperationException();
}
}

View file

@ -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
*
* <p>
* 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<String> property) {
super(space, property);
}
@Override
public String printableSummary() {
return rmap.printableSummary();
}
@Override
public Stream<Entry<String, String>> 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<String> into) {
SymZ3WriteDownHelper.writeDown(rmap, into);
}
}

View file

@ -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
*
* <p>
* 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<String> property;
/**
* Create the space
*
* @param space the address space
* @param property the property for storing and retrieving values in the trace
*/
public SymZ3TraceSpace(AddressSpace space, PcodeTracePropertyAccess<String> property) {
this.space = space;
this.property = property;
}
/**
* Write this cache back down into a trace
*
* <p>
* Here we simply iterate over every entry in this space, serialize the value, and store it into
* the property map at the entry's offset. Because a backing object may not have existed when
* creating this space, we must re-fetch the backing object, creating it if it does not exist.
*
* @param into the destination trace property accessor
*/
public abstract void writeDown(PcodeTracePropertyAccess<String> into);
}

View file

@ -0,0 +1,108 @@
/* ###
* 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.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.pcode.exec.trace.data.PcodeTracePropertyAccess;
import ghidra.program.model.address.AddressSpace;
import ghidra.symz3.model.SymValueZ3;
/**
* The storage space for unique registers
*
* <p>
* 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 SymZ3TraceUniqueSpace extends SymZ3TraceSpace {
private final Map<String, SymValueZ3> uniqvals = new HashMap<String, SymValueZ3>();
public SymZ3TraceUniqueSpace(AddressSpace space, PcodeTracePropertyAccess<String> property) {
super(space, property);
}
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<Entry<String, String>> 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) {
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?");
}
}
@Override
public void writeDown(PcodeTracePropertyAccess<String> into) {
return;
}
}

View file

@ -0,0 +1,90 @@
/* ###
* 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 com.microsoft.z3.Context;
import ghidra.pcode.emu.symz3.SymZ3MemoryMap;
import ghidra.pcode.emu.symz3.SymZ3RegisterMap;
import ghidra.pcode.exec.trace.data.PcodeTracePropertyAccess;
import ghidra.program.model.address.*;
import ghidra.program.model.lang.Register;
import ghidra.symz3.model.SymValueZ3;
public class SymZ3WriteDownHelper {
public static void writeDown(SymZ3RegisterMap rmap, PcodeTracePropertyAccess<String> property) {
for (Entry<Register, SymValueZ3> entry : rmap.regvals.entrySet()) {
SymValueZ3 symval = entry.getValue();
if (symval == null) {
throw new AssertionError(
"Register " + entry.getKey() + " has a null value in the map!");
}
Register key = entry.getKey();
Address address = key.getAddress();
String serialized_value = symval.serialize();
property.put(address, serialized_value);
}
}
public static void writeDown(SymZ3MemoryMap mmap, AddressSpace space,
PcodeTracePropertyAccess<String> into) {
/**
* Symbolic addresses all get stored as a single string in NO_ADDRESS, but concrete
* addresses we can store using the map.
*/
for (Entry<String, SymValueZ3> entry : mmap.memvals.entrySet()) {
/**
* some improvement could be made here, we have a serialized string as an address, but
* it might be just a number.
*
* This is really HACKY HACKY
*
* TODO: some refactoring needed
*/
try (Context ctx = new Context()) {
SymValueZ3 symAddr =
new SymValueZ3(ctx, SymValueZ3.deserializeBitVecExpr(ctx, entry.getKey()));
String serializedValue = entry.getValue().serialize();
BigInteger bi = symAddr.toBigInteger();
Boolean handled = false;
if (bi != null) {
try {
Address address = space.getAddress(bi.toString(16));
handled = true;
into.put(address, serializedValue);
}
catch (AddressFormatException e) {
// NOTE: Falls through to unhandled case
}
}
if (!handled) {
/**
* need to explore this.. for now we will grab and append, and not check for
* replacement so yes, this needs fixed...
*/
Address fakeAddress = Address.NO_ADDRESS;
String existing = into.get(fakeAddress);
existing = existing + "::" + symAddr + "<==>" + serializedValue;
into.put(fakeAddress, existing);
}
}
}
}
}

View file

@ -0,0 +1,35 @@
/* ###
* 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 trace-integrated Symbolic Z3 Emulator
*
* <p>
* This package builds on {@link ghidra.pcode.emu.plain} to construct a trace-integrated emulator.
* See that package for remarks about this "working solution." Those state components were factored
* to accommodate the state components introduced by this package.
*
* <p>
* For this package, I recommend a bottom-up approach, since you should already be familiar with the
* parts factory and the structure of the stand-alone state part.
* {@link ghidra.pcode.emu.symz3.trace.SymZ3TraceSpace} adds the ability to read and write symbolic
* values sets from a trace. {@link ghidra.pcode.emu.symz3.trace.SymZ3TracePcodeExecutorStatePiece}
* works that into a state piece derived from
* {@link ghidra.pcode.emu.symz3.plain.SymZ3PcodeExecutorStatePiece}. Then,
* {@link ghidra.pcode.emu.symz3.trace.SymZ3TracePcodeExecutorState} composes that with a given
* concrete state piece. The factory creates that state for use by the
* {@link ghidra.pcode.emu.symz3.trace.SymZ3TracePcodeEmulator}.
*/
package ghidra.pcode.emu.symz3.trace;

View file

@ -0,0 +1,38 @@
/* ###
* 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.symz3.gui;
import java.awt.Font;
import ghidra.docking.settings.Settings;
import ghidra.util.HTMLUtilities;
import ghidra.util.table.column.AbstractGColumnRenderer;
class HtmlCellRenderer extends AbstractGColumnRenderer<String> {
{
setHTMLRenderingEnabled(true);
}
@Override
protected Font getDefaultFont() {
return fixedWidthFont;
}
@Override
public String getFilterString(String t, Settings settings) {
return HTMLUtilities.fromHTML(t);
}
}

View file

@ -0,0 +1,37 @@
/* ###
* 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.symz3.gui;
import java.awt.Font;
import ghidra.docking.settings.Settings;
import ghidra.util.table.column.AbstractGColumnRenderer;
class MonospaceCellRenderer extends AbstractGColumnRenderer<Object> {
{
setHTMLRenderingEnabled(false);
}
@Override
protected Font getDefaultFont() {
return fixedWidthFont;
}
@Override
public String getFilterString(Object t, Settings settings) {
return t.toString();
}
}

View file

@ -0,0 +1,150 @@
/* ###
* 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.symz3.gui;
import java.awt.BorderLayout;
import java.util.List;
import java.util.Map.Entry;
import java.util.function.Function;
import java.util.stream.Stream;
import javax.swing.JPanel;
import javax.swing.JScrollPane;
import javax.swing.table.TableColumn;
import javax.swing.table.TableColumnModel;
import docking.widgets.table.DefaultEnumeratedColumnTableModel;
import docking.widgets.table.DefaultEnumeratedColumnTableModel.EnumeratedTableColumn;
import docking.widgets.table.GTable;
import ghidra.framework.plugintool.PluginTool;
import ghidra.pcode.emu.symz3.SymZ3RecordsExecution.RecInstruction;
import ghidra.symz3.gui.Z3SummaryInstructionLogPanel.InstructionHtmlFormatter;
import ghidra.util.table.GhidraTableFilterPanel;
public class Z3SummaryInformationPanel extends JPanel {
enum InfoKind {
VALUATION("val"), PRECONDITION("pre");
final String display;
private InfoKind(String display) {
this.display = display;
}
@Override
public String toString() {
return display;
}
}
record InformationRow(InfoKind kind, String variable, String value) {
}
protected enum InformationTableColumns
implements EnumeratedTableColumn<InformationTableColumns, InformationRow> {
KIND("Kind", InfoKind.class, InformationRow::kind, true),
VARIABLE("Variable", String.class, InformationRow::variable, true),
VALUE("Value", String.class, InformationRow::value, true);
private final String header;
private final Class<?> cls;
private final Function<InformationRow, ?> getter;
private final boolean visible;
<T> InformationTableColumns(String header, Class<T> cls,
Function<InformationRow, T> getter, boolean visible) {
this.header = header;
this.cls = cls;
this.getter = getter;
this.visible = visible;
}
static String getInstructionHtml(RecInstruction op) {
InstructionHtmlFormatter formatter = new InstructionHtmlFormatter();
return formatter.formatInstruction(op.instruction());
}
@Override
public Class<?> getValueClass() {
return cls;
}
@Override
public Object getValueOf(InformationRow row) {
return getter.apply(row);
}
@Override
public String getHeader() {
return header;
}
@Override
public boolean isVisible() {
return visible;
}
}
protected static class InformationTableModel extends
DefaultEnumeratedColumnTableModel<InformationTableColumns, InformationRow> {
public InformationTableModel(PluginTool tool) {
super(tool, "Summary-Information", InformationTableColumns.class);
}
@Override
public List<InformationTableColumns> defaultSortOrder() {
return List.of(InformationTableColumns.KIND, InformationTableColumns.VARIABLE);
}
}
protected final InformationTableModel model;
protected final GTable table;
protected final GhidraTableFilterPanel<InformationRow> filterPanel;
public Z3SummaryInformationPanel(Z3SummaryProvider provider) {
super(new BorderLayout());
model = new InformationTableModel(provider.getTool());
table = new GTable(model);
add(new JScrollPane(table));
filterPanel = new GhidraTableFilterPanel<>(table, model);
add(filterPanel, BorderLayout.SOUTH);
TableColumnModel columnModel = table.getColumnModel();
TableColumn kindCol = columnModel.getColumn(InformationTableColumns.KIND.ordinal());
kindCol.setMaxWidth(40);
kindCol.setMinWidth(40);
TableColumn varCol = columnModel.getColumn(InformationTableColumns.VARIABLE.ordinal());
varCol.setCellRenderer(new MonospaceCellRenderer());
varCol.setPreferredWidth(20);
TableColumn valCol = columnModel.getColumn(InformationTableColumns.VALUE.ordinal());
valCol.setCellRenderer(new MonospaceCellRenderer());
valCol.setPreferredWidth(60);
}
public void setInformation(Stream<Entry<String, String>> valuations,
Stream<String> preconditions) {
model.clear();
Stream<InformationRow> fromValuations =
valuations.map(v -> new InformationRow(InfoKind.VALUATION, v.getKey(), v.getValue()));
Stream<InformationRow> fromPreconditions =
preconditions.map(v -> new InformationRow(InfoKind.PRECONDITION, "", v));
model.addAll(Stream.concat(fromValuations, fromPreconditions).toList());
}
}

View file

@ -0,0 +1,332 @@
/* ###
* 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.symz3.gui;
import java.awt.BorderLayout;
import java.awt.Color;
import java.awt.event.*;
import java.util.List;
import java.util.function.Function;
import javax.swing.*;
import javax.swing.table.TableColumn;
import javax.swing.table.TableColumnModel;
import docking.widgets.table.DefaultEnumeratedColumnProgramTableModel;
import docking.widgets.table.DefaultEnumeratedColumnTableModel.EnumeratedTableColumn;
import docking.widgets.table.GTable;
import generic.theme.GColor;
import ghidra.framework.plugintool.PluginTool;
import ghidra.pcode.emu.symz3.SymZ3RecordsExecution.RecInstruction;
import ghidra.program.model.address.Address;
import ghidra.program.model.lang.Register;
import ghidra.program.model.listing.*;
import ghidra.program.model.scalar.Scalar;
import ghidra.program.model.symbol.Equate;
import ghidra.util.HTMLUtilities;
import ghidra.util.WebColors;
import ghidra.util.table.GhidraTableFilterPanel;
public class Z3SummaryInstructionLogPanel extends JPanel {
private static final Color COLOR_FOREGROUND_ADDRESS = new GColor("color.fg.listing.address");
private static final Color COLOR_FOREGROUND_REGISTER = new GColor("color.fg.listing.register");
private static final Color COLOR_FOREGROUND_SCALAR = new GColor("color.fg.listing.constant");
private static final Color COLOR_FOREGROUND_MNEMONIC = new GColor("color.fg.listing.mnemonic");
private static final Color COLOR_FOREGROUND_SEPARATOR =
new GColor("color.fg.listing.separator");
private static final Color COLOR_FOREGROUND_BADREF = new GColor("color.fg.listing.ref.bad");
private static final Color COLOR_FOREGROUND_VARIABLE =
new GColor("color.fg.listing.function.variable");
protected static String htmlColor(Color color, String display) {
return String.format("<font color=\"%s\">%s</font>", WebColors.toString(color, false),
HTMLUtilities.escapeHTML(display));
}
protected enum InstructionLogTableColumns
implements EnumeratedTableColumn<InstructionLogTableColumns, RecInstruction> {
INDEX("Index", Integer.class, RecInstruction::index, true),
THREAD("Thread", String.class, RecInstruction::getThreadName, true),
ADDRESS("Address", Address.class, RecInstruction::getAddress, true),
CODE("Instruction", String.class, InstructionLogTableColumns::getInstructionHtml, true),;
private final String header;
private final Class<?> cls;
private final Function<RecInstruction, ?> getter;
private final boolean visible;
<T> InstructionLogTableColumns(String header, Class<T> cls,
Function<RecInstruction, T> getter, boolean visible) {
this.header = header;
this.cls = cls;
this.getter = getter;
this.visible = visible;
}
static String getInstructionHtml(RecInstruction op) {
InstructionHtmlFormatter formatter = new InstructionHtmlFormatter();
return formatter.formatInstruction(op.instruction());
}
@Override
public Class<?> getValueClass() {
return cls;
}
@Override
public Object getValueOf(RecInstruction row) {
return getter.apply(row);
}
@Override
public String getHeader() {
return header;
}
@Override
public boolean isVisible() {
return visible;
}
}
protected static class InstructionLogTableModel extends
DefaultEnumeratedColumnProgramTableModel<InstructionLogTableColumns, RecInstruction> {
public InstructionLogTableModel(PluginTool tool) {
super(tool, "Summary-InstructionLog", InstructionLogTableColumns.class,
InstructionLogTableColumns.ADDRESS);
}
@Override
public List<InstructionLogTableColumns> defaultSortOrder() {
return List.of(InstructionLogTableColumns.INDEX);
}
}
static class InstructionHtmlAppender {
private final StringBuffer html = new StringBuffer("<html>");
public void appendMnemonic(String mnemonic) {
html.append(htmlColor(COLOR_FOREGROUND_MNEMONIC, mnemonic));
}
public void appendSeparator(String separator) {
html.append(htmlColor(COLOR_FOREGROUND_SEPARATOR, separator));
}
public void appendSeparator(Character separator) {
html.append(htmlColor(COLOR_FOREGROUND_SEPARATOR, Character.toString(separator)));
}
public void appendBadRef(String error) {
html.append(htmlColor(COLOR_FOREGROUND_BADREF, error));
}
public void appendRegister(String regname) {
html.append(htmlColor(COLOR_FOREGROUND_REGISTER, regname));
}
public void appendScalar(String scalar) {
html.append(htmlColor(COLOR_FOREGROUND_SCALAR, scalar));
}
public void appendAddress(String address) {
html.append(htmlColor(COLOR_FOREGROUND_ADDRESS, address));
}
public void appendVariableRef(String variable) {
html.append(htmlColor(COLOR_FOREGROUND_VARIABLE, variable));
}
public String finish() {
html.append("</html>");
return html.toString();
}
}
static class InstructionHtmlFormatter {
private final static boolean SPACE_AFTER_SEP = true;
String formatInstruction(Instruction instruction) {
InstructionHtmlAppender appender = new InstructionHtmlAppender();
appender.appendMnemonic(instruction.getMnemonicString());
appender.appendSeparator(" ");
int numOperands = instruction.getNumOperands();
if (numOperands == 0) {
return appender.finish();
}
formatSeparator(instruction, 0, appender);
for (int opIndex = 0; opIndex < numOperands; opIndex++) {
List<Object> operandRepresentationList =
instruction.getDefaultOperandRepresentationList(opIndex);
formatOperand(instruction, operandRepresentationList, opIndex, appender);
}
return appender.finish();
}
void formatSeparator(Instruction instruction, int separatorIndex,
InstructionHtmlAppender appender) {
String separator = instruction.getSeparator(separatorIndex);
if (separator == null) {
return;
}
if (SPACE_AFTER_SEP) {
separator += " ";
}
appender.appendSeparator(separator);
}
void formatOperand(Instruction instruction, List<Object> opRepList, int opIndex,
InstructionHtmlAppender appender) {
if (opRepList == null) {
appender.appendBadRef(opRepList == null ? "<UNSUPPORTED>" : opRepList.toString());
return;
}
for (int subOpIndex = 0; subOpIndex < opRepList.size(); subOpIndex++) {
formatSubOperand(instruction, opRepList.get(subOpIndex), opIndex, subOpIndex,
appender);
}
formatSeparator(instruction, opIndex + 1, appender);
}
void formatSubOperand(Instruction instruction, Object opRep, int opIndex, int subOpIndex,
InstructionHtmlAppender appender) {
switch (opRep) {
case VariableOffset vo -> formatSubOperand(instruction, vo.getObjects(), opIndex,
subOpIndex, appender);
case List<?> l -> formatSubOperand(instruction, l, opIndex, subOpIndex, appender);
case String s -> formatSeparator(instruction, s, opIndex, subOpIndex, appender);
case Register r -> formatRegister(instruction, r, opIndex, subOpIndex, appender);
case Scalar s -> formatScalar(instruction, s, opIndex, subOpIndex, appender);
case Address a -> formatAddress(instruction, a, opIndex, subOpIndex, appender);
case Character c -> formatSeparator(instruction, c, opIndex, subOpIndex, appender);
case Equate e -> formatEquate(instruction, e, opIndex, subOpIndex, appender);
case LabelString l -> formatLabelString(instruction, l, opIndex, subOpIndex,
appender);
default -> formatSeparator(instruction, opRep.toString(), opIndex, subOpIndex,
appender);
}
}
void formatSeparator(Instruction instruction, String opRep, int opIndex, int subOpIndex,
InstructionHtmlAppender appender) {
appender.appendSeparator(opRep);
}
void formatSeparator(Instruction instruction, Character opRep, int opIndex, int subOpIndex,
InstructionHtmlAppender appender) {
appender.appendSeparator(opRep);
}
void formatRegister(Instruction instruction, Register opRep, int opIndex, int subOpIndex,
InstructionHtmlAppender appender) {
appender.appendRegister(opRep.toString());
}
void formatScalar(Instruction instruction, Scalar opRep, int opIndex, int subOpIndex,
InstructionHtmlAppender appender) {
appender.appendScalar(opRep.toString());
}
void formatAddress(Instruction instruction, Address opRep, int opIndex, int subOpIndex,
InstructionHtmlAppender appender) {
appender.appendAddress(opRep.toString());
}
void formatEquate(Instruction instruction, Equate opRep, int opIndex, int subOpIndex,
InstructionHtmlAppender appender) {
appender.appendScalar(opRep.toString());
}
void formatLabelString(Instruction instruction, LabelString l, int opIndex, int subOpIndex,
InstructionHtmlAppender appender) {
switch (l.getLabelType()) {
case VARIABLE -> appender.appendVariableRef(l.toString());
default -> appender.appendSeparator(l.toString());
}
}
}
private final Z3SummaryProvider provider;
protected final InstructionLogTableModel model;
protected final GTable table;
protected final GhidraTableFilterPanel<RecInstruction> filterPanel;
public Z3SummaryInstructionLogPanel(Z3SummaryProvider provider) {
super(new BorderLayout());
this.provider = provider;
model = new InstructionLogTableModel(provider.getTool());
table = new GTable(model);
add(new JScrollPane(table));
filterPanel = new GhidraTableFilterPanel<>(table, model);
add(filterPanel, BorderLayout.SOUTH);
TableColumnModel columnModel = table.getColumnModel();
TableColumn indexCol = columnModel.getColumn(InstructionLogTableColumns.INDEX.ordinal());
indexCol.setMaxWidth(30);
indexCol.setMinWidth(30);
TableColumn threadCol = columnModel.getColumn(InstructionLogTableColumns.THREAD.ordinal());
threadCol.setMaxWidth(30);
threadCol.setMinWidth(30);
TableColumn addrCol = columnModel.getColumn(InstructionLogTableColumns.ADDRESS.ordinal());
addrCol.setCellRenderer(new MonospaceCellRenderer());
addrCol.setPreferredWidth(20);
TableColumn codeCol = columnModel.getColumn(InstructionLogTableColumns.CODE.ordinal());
codeCol.setCellRenderer(new HtmlCellRenderer());
codeCol.setPreferredWidth(40);
table.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION);
table.addMouseListener(new MouseAdapter() {
@Override
public void mouseClicked(MouseEvent e) {
if (e.getClickCount() != 2) {
return;
}
e.consume();
fireSelectedAddress();
}
});
table.addKeyListener(new KeyAdapter() {
@Override
public void keyPressed(KeyEvent e) {
if (e.getKeyCode() != KeyEvent.VK_ENTER) {
return;
}
e.consume();
fireSelectedAddress();
}
});
}
private void fireSelectedAddress() {
RecInstruction sel = filterPanel.getSelectedItem();
if (sel == null) {
return;
}
provider.fireAddress(sel.getAddress());
}
public void setLog(List<RecInstruction> log) {
model.clear();
model.addAll(log);
}
}

View file

@ -0,0 +1,328 @@
/* ###
* 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.symz3.gui;
import java.awt.BorderLayout;
import java.awt.Color;
import java.awt.event.*;
import java.util.List;
import java.util.function.Function;
import javax.swing.*;
import javax.swing.table.TableColumn;
import javax.swing.table.TableColumnModel;
import docking.widgets.table.DefaultEnumeratedColumnProgramTableModel;
import docking.widgets.table.DefaultEnumeratedColumnTableModel.EnumeratedTableColumn;
import docking.widgets.table.GTable;
import generic.theme.GColor;
import ghidra.app.plugin.processors.sleigh.template.OpTpl;
import ghidra.app.util.pcode.*;
import ghidra.framework.plugintool.PluginTool;
import ghidra.pcode.emu.PcodeThread;
import ghidra.pcode.emu.symz3.SymZ3RecordsExecution.RecOp;
import ghidra.pcode.exec.PcodeFrame;
import ghidra.pcode.exec.PcodeProgram;
import ghidra.program.model.address.Address;
import ghidra.program.model.address.AddressSpace;
import ghidra.program.model.lang.Language;
import ghidra.program.model.lang.Register;
import ghidra.program.model.pcode.PcodeOp;
import ghidra.util.HTMLUtilities;
import ghidra.util.WebColors;
import ghidra.util.table.GhidraTableFilterPanel;
public class Z3SummaryPcodeLogPanel extends JPanel {
private static final Color COLOR_FOREGROUND_ADDRESS = new GColor("color.fg.listing.address");
private static final Color COLOR_FOREGROUND_REGISTER = new GColor("color.fg.listing.register");
private static final Color COLOR_FOREGROUND_SCALAR = new GColor("color.fg.listing.constant");
private static final Color COLOR_FOREGROUND_LOCAL = new GColor("color.fg.listing.label.local");
private static final Color COLOR_FOREGROUND_MNEMONIC = new GColor("color.fg.listing.mnemonic");
private static final Color COLOR_FOREGROUND_UNIMPL =
new GColor("color.fg.listing.mnemonic.unimplemented");
private static final Color COLOR_FOREGROUND_SEPARATOR =
new GColor("color.fg.listing.separator");
private static final Color COLOR_FOREGROUND_LINE_LABEL =
new GColor("color.fg.listing.pcode.label");
private static final Color COLOR_FOREGROUND_SPACE =
new GColor("color.fg.listing.pcode.address.space");
private static final Color COLOR_FOREGROUND_RAW = new GColor("color.fg.listing.pcode.varnode");
private static final Color COLOR_FOREGROUND_USEROP =
new GColor("color.fg.listing.pcode.userop");
protected static String htmlColor(Color color, String display) {
return String.format("<font color=\"%s\">%s</font>", WebColors.toString(color, false),
HTMLUtilities.escapeHTML(display));
}
protected enum PcodeLogTableColumns
implements EnumeratedTableColumn<PcodeLogTableColumns, RecOp> {
INDEX("Index", Integer.class, RecOp::index, true),
THREAD("Thread", String.class, RecOp::getThreadName, true),
ADDRESS("Address", Address.class, RecOp::getAddress, false),
CODE("P-code", String.class, PcodeLogTableColumns::getPcodeHtml, true),
;
private final String header;
private final Class<?> cls;
private final Function<RecOp, ?> getter;
private final boolean visible;
<T> PcodeLogTableColumns(String header, Class<T> cls, Function<RecOp, T> getter,
boolean visible) {
this.header = header;
this.cls = cls;
this.getter = getter;
this.visible = visible;
}
static String getPcodeHtml(RecOp op) {
PcodeHtmlFormatter formatter = new PcodeHtmlFormatter(op.thread());
return formatter.formatOp(op.op());
}
@Override
public Class<?> getValueClass() {
return cls;
}
@Override
public Object getValueOf(RecOp row) {
return getter.apply(row);
}
@Override
public String getHeader() {
return header;
}
@Override
public boolean isVisible() {
return visible;
}
}
protected static class PcodeLogTableModel
extends DefaultEnumeratedColumnProgramTableModel<PcodeLogTableColumns, RecOp> {
public PcodeLogTableModel(PluginTool tool) {
super(tool, "Summary-PcodeLog", PcodeLogTableColumns.class,
PcodeLogTableColumns.ADDRESS);
}
@Override
public List<PcodeLogTableColumns> defaultSortOrder() {
return List.of(PcodeLogTableColumns.INDEX);
}
}
static class PcodeHtmlAppender extends AbstractAppender<String> {
private final PcodeFrame frame;
private final StringBuffer html = new StringBuffer("<html>");
public PcodeHtmlAppender(Language language, PcodeFrame frame) {
super(language, false);
this.frame = frame;
}
@Override
public void appendAddressWordOffcut(long wordOffset, long offcut) {
html.append(
htmlColor(COLOR_FOREGROUND_ADDRESS, stringifyWordOffcut(wordOffset, offcut)));
}
@Override
public void appendCharacter(char c) {
if (c == '=') {
html.append("&nbsp;");
html.append(htmlColor(COLOR_FOREGROUND_SEPARATOR, "="));
html.append("&nbsp;");
}
else if (c == ' ') {
html.append("&nbsp;");
}
else {
html.append(htmlColor(COLOR_FOREGROUND_SEPARATOR, Character.toString(c)));
}
}
@Override
public void appendIndent() {
// stub
}
@Override
public void appendLabel(String label) {
html.append(htmlColor(COLOR_FOREGROUND_LOCAL, label));
}
@Override
public void appendLineLabel(long label) {
throw new AssertionError();
}
@Override
public void appendLineLabelRef(long label) {
html.append(htmlColor(COLOR_FOREGROUND_LINE_LABEL, stringifyLineLabel(label)));
}
@Override
public void appendMnemonic(int opcode) {
Color style = opcode == PcodeOp.UNIMPLEMENTED ? COLOR_FOREGROUND_UNIMPL
: COLOR_FOREGROUND_MNEMONIC;
html.append(htmlColor(style, stringifyOpMnemonic(opcode)));
}
@Override
public void appendRawVarnode(AddressSpace space, long offset, long size) {
html.append(
htmlColor(COLOR_FOREGROUND_RAW, stringifyRawVarnode(space, offset, size)));
}
@Override
public void appendRegister(Register register) {
html.append(htmlColor(COLOR_FOREGROUND_REGISTER, stringifyRegister(register)));
}
@Override
public void appendScalar(long value) {
html.append(htmlColor(COLOR_FOREGROUND_SCALAR, stringifyScalarValue(value)));
}
@Override
public void appendSpace(AddressSpace space) {
html.append(htmlColor(COLOR_FOREGROUND_SPACE, stringifySpace(space)));
}
@Override
public void appendUnique(long offset) {
html.append(htmlColor(COLOR_FOREGROUND_LOCAL, stringifyUnique(offset)));
}
@Override
public void appendUserop(int id) {
html.append(htmlColor(COLOR_FOREGROUND_USEROP, stringifyUserop(language, id)));
}
@Override
protected String stringifyUseropUnchecked(Language lang, int id) {
String name = super.stringifyUseropUnchecked(lang, id);
if (name != null) {
return name;
}
return frame.getUseropName(id);
}
@Override
public String finish() {
html.append("</html>");
return html.toString();
}
}
static class PcodeHtmlFormatter extends AbstractPcodeFormatter<String, PcodeHtmlAppender> {
private final Language language;
private final PcodeFrame frame;
public PcodeHtmlFormatter(PcodeThread<?> thread) {
this.language = thread.getLanguage();
PcodeProgram nop = thread.getMachine().compileSleigh("nothing", "");
this.frame = thread.getExecutor().begin(nop);
}
String getHtml() {
return formatOps(language, frame.getCode());
}
@Override
protected PcodeHtmlAppender createAppender(Language lang, boolean indent) {
return new PcodeHtmlAppender(lang, frame);
}
String formatOp(PcodeOp op) {
OpTpl tpl = PcodeFormatter.getPcodeOpTemplateLog(language.getAddressFactory(), op);
PcodeHtmlAppender appender = createAppender(language, false);
formatOpTemplate(appender, tpl);
return appender.finish();
}
}
private final Z3SummaryProvider provider;
protected final PcodeLogTableModel model;
protected final GTable table;
protected final GhidraTableFilterPanel<RecOp> filterPanel;
public Z3SummaryPcodeLogPanel(Z3SummaryProvider provider) {
super(new BorderLayout());
this.provider = provider;
model = new PcodeLogTableModel(provider.getTool());
table = new GTable(model);
add(new JScrollPane(table));
filterPanel = new GhidraTableFilterPanel<>(table, model);
add(filterPanel, BorderLayout.SOUTH);
TableColumnModel columnModel = table.getColumnModel();
TableColumn indexCol = columnModel.getColumn(PcodeLogTableColumns.INDEX.ordinal());
indexCol.setMaxWidth(30);
indexCol.setMinWidth(30);
TableColumn threadCol = columnModel.getColumn(PcodeLogTableColumns.THREAD.ordinal());
threadCol.setMaxWidth(30);
threadCol.setMinWidth(30);
TableColumn addrCol = columnModel.getColumn(PcodeLogTableColumns.ADDRESS.ordinal());
addrCol.setCellRenderer(new MonospaceCellRenderer());
addrCol.setPreferredWidth(20);
TableColumn codeCol = columnModel.getColumn(PcodeLogTableColumns.CODE.ordinal());
codeCol.setCellRenderer(new HtmlCellRenderer());
codeCol.setPreferredWidth(40);
table.setSelectionMode(ListSelectionModel.MULTIPLE_INTERVAL_SELECTION);
table.addMouseListener(new MouseAdapter() {
@Override
public void mouseClicked(MouseEvent e) {
if (e.getClickCount() != 2) {
return;
}
e.consume();
fireSelectedAddress();
}
});
table.addKeyListener(new KeyAdapter() {
@Override
public void keyPressed(KeyEvent e) {
if (e.getKeyCode() != KeyEvent.VK_ENTER) {
return;
}
e.consume();
fireSelectedAddress();
}
});
}
private void fireSelectedAddress() {
RecOp sel = filterPanel.getSelectedItem();
if (sel == null) {
return;
}
provider.fireAddress(sel.getAddress());
}
public void setLog(List<RecOp> log) {
model.clear();
model.addAll(log);
}
}

View file

@ -0,0 +1,61 @@
/* ###
* 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.symz3.gui;
import ghidra.app.plugin.PluginCategoryNames;
import ghidra.app.plugin.core.debug.AbstractDebuggerPlugin;
import ghidra.app.plugin.core.debug.DebuggerPluginPackage;
import ghidra.app.plugin.core.debug.event.TraceActivatedPluginEvent;
import ghidra.app.services.DebuggerEmulationService;
import ghidra.app.services.DebuggerTraceManagerService;
import ghidra.framework.plugintool.*;
import ghidra.framework.plugintool.util.PluginStatus;
@PluginInfo(
shortDescription = "xyzzy",
description = "GUI to single-step emulation of p-code",
category = PluginCategoryNames.DEBUGGER,
packageName = DebuggerPluginPackage.NAME,
status = PluginStatus.UNSTABLE,
eventsConsumed = {
TraceActivatedPluginEvent.class,
},
servicesRequired = {
DebuggerTraceManagerService.class,
DebuggerEmulationService.class,
})
public class Z3SummaryPlugin extends AbstractDebuggerPlugin {
protected Z3SummaryProvider provider;
public Z3SummaryPlugin(PluginTool tool) {
super(tool);
}
@Override
protected void init() {
provider = new Z3SummaryProvider(this);
super.init();
}
@Override
public void processEvent(PluginEvent event) {
super.processEvent(event);
if (event instanceof TraceActivatedPluginEvent) {
TraceActivatedPluginEvent ev = (TraceActivatedPluginEvent) event;
provider.coordinatesActivated(ev.getActiveCoordinates());
}
}
}

View file

@ -0,0 +1,204 @@
/* ###
* 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.symz3.gui;
import java.awt.BorderLayout;
import java.util.Objects;
import javax.swing.*;
import com.microsoft.z3.Context;
import ghidra.app.plugin.core.debug.DebuggerPluginPackage;
import ghidra.app.plugin.core.debug.event.TraceLocationPluginEvent;
import ghidra.app.plugin.core.debug.gui.DebuggerResources;
import ghidra.app.services.DebuggerEmulationService;
import ghidra.app.services.DebuggerEmulationService.CachedEmulator;
import ghidra.app.services.DebuggerEmulationService.EmulatorStateListener;
import ghidra.app.services.DebuggerTraceManagerService;
import ghidra.app.util.pcode.StringPcodeFormatter;
import ghidra.debug.api.emulation.DebuggerPcodeEmulatorFactory;
import ghidra.debug.api.emulation.DebuggerPcodeMachine;
import ghidra.debug.api.tracemgr.DebuggerCoordinates;
import ghidra.framework.options.AutoOptions;
import ghidra.framework.plugintool.AutoService;
import ghidra.framework.plugintool.ComponentProviderAdapter;
import ghidra.framework.plugintool.annotation.AutoServiceConsumed;
import ghidra.pcode.emu.symz3.full.SymZ3DebuggerPcodeEmulator;
import ghidra.pcode.emu.symz3.full.SymZ3DebuggerPcodeEmulatorFactory;
import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
import ghidra.program.model.address.Address;
import ghidra.program.util.ProgramLocation;
import ghidra.trace.model.Trace;
import ghidra.trace.model.time.schedule.TraceSchedule;
public class Z3SummaryProvider extends ComponentProviderAdapter {
protected static boolean sameCoordinates(DebuggerCoordinates a, DebuggerCoordinates b) {
if (!Objects.equals(a.getTrace(), b.getTrace())) {
return false;
}
if (!Objects.equals(a.getTime(), b.getTime())) {
return false;
}
if (!Objects.equals(a.getThread(), b.getThread())) {
return false;
}
return true;
}
private final EmulatorStateListener emuListener = new EmulatorStateListener() {
@Override
public void stopped(CachedEmulator emu) {
if (!(emu.emulator() instanceof SymZ3DebuggerPcodeEmulator z3emu)) {
setFactoryToZ3();
return;
}
populateSummaryFromEmulator(z3emu);
}
};
@SuppressWarnings("unused")
private final Z3SummaryPlugin plugin;
DebuggerCoordinates current = DebuggerCoordinates.NOWHERE;
@AutoServiceConsumed
private DebuggerTraceManagerService traceManager;
//@AutoServiceConsumed via method
private DebuggerEmulationService emulationService;
@SuppressWarnings("unused")
private AutoService.Wiring autoServiceWiring;
@SuppressWarnings("unused")
private AutoOptions.Wiring autoOptionsWiring;
String style = "<html>";
JPanel mainPanel = new JPanel(new BorderLayout());
JSplitPane submainPanel = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT);
JSplitPane codePanel = new JSplitPane(JSplitPane.VERTICAL_SPLIT);
Z3SummaryInformationPanel information;
Z3SummaryPcodeLogPanel ops;
Z3SummaryInstructionLogPanel instructions;
StringPcodeFormatter formatter = new StringPcodeFormatter();
public Z3SummaryProvider(Z3SummaryPlugin plugin) {
super(plugin.getTool(), "Z3 Summary", plugin.getName(), null);
this.plugin = plugin;
this.autoServiceWiring = AutoService.wireServicesConsumed(plugin, this);
this.autoOptionsWiring = AutoOptions.wireOptions(plugin, this);
setIcon(DebuggerResources.ICON_PROVIDER_PCODE);
setHelpLocation(DebuggerResources.HELP_PROVIDER_PCODE);
setWindowMenuGroup(DebuggerPluginPackage.NAME);
buildMainPanel();
setVisible(true);
contextChanged();
}
@Override
public JComponent getComponent() {
return mainPanel;
}
private void buildMainPanel() {
information = new Z3SummaryInformationPanel(this);
ops = new Z3SummaryPcodeLogPanel(this);
instructions = new Z3SummaryInstructionLogPanel(this);
JPanel summaryPanel = new JPanel(new BorderLayout());
summaryPanel.add(new JScrollPane(information));
codePanel.setTopComponent(instructions);
codePanel.setBottomComponent(ops);
codePanel.setDividerLocation(0.4);
submainPanel.setRightComponent(summaryPanel);
submainPanel.setLeftComponent(codePanel);
mainPanel.add(submainPanel);
}
public void updateSummary() {
ops.setLog(java.util.List.of());
instructions.setLog(java.util.List.of());
if (emulationService == null) {
return;
}
Trace trace = current.getTrace();
if (trace == null) {
return;
}
TraceSchedule time = current.getTime();
DebuggerPcodeMachine<?> emu = emulationService.getCachedEmulator(trace, time);
if (!(emu instanceof SymZ3DebuggerPcodeEmulator z3Emu)) {
/** LATER: It'd be nice if the summary were written down somewhere */
setFactoryToZ3();
return;
}
populateSummaryFromEmulator(z3Emu);
}
private void setFactoryToZ3() {
for (DebuggerPcodeEmulatorFactory factory : emulationService.getEmulatorFactories()) {
if (factory instanceof SymZ3DebuggerPcodeEmulatorFactory z3factory) {
emulationService.setEmulatorFactory(z3factory);
emulationService.invalidateCache();
return;
}
}
}
public void populateSummaryFromEmulator(SymZ3DebuggerPcodeEmulator emu) {
try (Context ctx = new Context()) {
Z3InfixPrinter z3p = new Z3InfixPrinter(ctx);
information.setInformation(emu.streamValuations(ctx, z3p),
emu.streamPreconditions(ctx, z3p));
}
ops.setLog(emu.getOps());
instructions.setLog(emu.getInstructions());
}
public void coordinatesActivated(DebuggerCoordinates coordinates) {
if (sameCoordinates(current, coordinates)) {
current = coordinates;
return;
}
current = coordinates;
updateSummary();
setSubTitle(current.getTime().toString());
contextChanged();
}
public void fireAddress(Address address) {
plugin.firePluginEvent(new TraceLocationPluginEvent(plugin.getName(),
new ProgramLocation(current.getView(), address)));
}
@AutoServiceConsumed
private void setEmulationService(DebuggerEmulationService emulationService) {
if (this.emulationService != null) {
this.emulationService.removeStateListener(emuListener);
}
this.emulationService = emulationService;
if (this.emulationService != null) {
this.emulationService.addStateListener(emuListener);
}
}
}

View file

@ -0,0 +1,88 @@
/* ###
* 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.symz3.gui.field;
import docking.widgets.table.AbstractDynamicTableColumn;
import docking.widgets.table.DynamicTableColumn;
import ghidra.app.plugin.core.debug.gui.register.DebuggerRegisterColumnFactory;
import ghidra.app.plugin.core.debug.gui.register.RegisterRow;
import ghidra.debug.api.tracemgr.DebuggerCoordinates;
import ghidra.docking.settings.Settings;
import ghidra.framework.plugintool.ServiceProvider;
import ghidra.pcode.emu.symz3.trace.SymZ3TracePcodeExecutorStatePiece;
import ghidra.program.model.address.AddressSpace;
import ghidra.program.model.lang.Register;
import ghidra.trace.model.Trace;
import ghidra.trace.model.property.TracePropertyMap;
import ghidra.trace.model.property.TracePropertyMapSpace;
/**
* A factory for the "Symbolic Expression" column in the "Registers" panel
*
* <p>
* For the most part, this is just a matter of accessing the property map and rendering the value on
* screen.
*/
public class SymZ3DebuggerRegisterColumnFactory implements DebuggerRegisterColumnFactory {
protected static final String PROP_NAME = SymZ3TracePcodeExecutorStatePiece.NAME;
public static final String COL_NAME = "Symbolic Expression";
@Override
public DynamicTableColumn<RegisterRow, ?, ?> create() {
return new AbstractDynamicTableColumn<RegisterRow, String, Void>() {
@Override
public String getColumnName() {
return COL_NAME;
}
@Override
public String getValue(RegisterRow rowObject, Settings settings, Void data,
ServiceProvider serviceProvider) throws IllegalArgumentException {
DebuggerCoordinates current = rowObject.getCurrent();
Trace trace = current.getTrace();
if (trace == null) {
return "";
}
TracePropertyMap<String> symMap = current.getTrace()
.getAddressPropertyManager()
.getPropertyMap(PROP_NAME, String.class);
if (symMap == null) {
return "";
}
Register register = rowObject.getRegister();
TracePropertyMapSpace<String> symSpace;
AddressSpace addressSpace = register.getAddressSpace();
if (addressSpace.isRegisterSpace()) {
symSpace = symMap.getPropertyMapRegisterSpace(current.getThread(),
current.getFrame(), false);
}
else {
symSpace = symMap.getPropertyMapSpace(addressSpace, false);
}
if (symSpace == null) {
return "";
}
// Cheat the deserialization/reserialization here
String display = symSpace.get(current.getViewSnap(), register.getAddress());
return display == null ? "" : display;
}
};
}
}

View file

@ -0,0 +1,140 @@
/* ###
* 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.symz3.gui.field;
import java.math.BigInteger;
import docking.widgets.fieldpanel.field.AttributedString;
import docking.widgets.fieldpanel.field.TextFieldElement;
import docking.widgets.fieldpanel.support.FieldLocation;
import generic.theme.GColor;
import ghidra.app.util.ListingHighlightProvider;
import ghidra.app.util.viewer.field.*;
import ghidra.app.util.viewer.format.FieldFormatModel;
import ghidra.app.util.viewer.proxy.ProxyObj;
import ghidra.framework.options.Options;
import ghidra.framework.options.ToolOptions;
import ghidra.pcode.emu.symz3.trace.SymZ3TracePcodeExecutorStatePiece;
import ghidra.program.model.listing.CodeUnit;
import ghidra.program.model.util.StringPropertyMap;
import ghidra.program.util.ProgramLocation;
import ghidra.symz3.model.SymValueZ3;
/**
* A field factory for "SymZ3" in the Listing panels
*
* <p>
* This implements an interface that is part of the core framework, even lower than the Debugger
* framework. I used the "sample" module's {@code EntropyFieldFactory} for reference.
*/
public class SymZ3FieldFactory extends FieldFactory {
public static final String PROPERTY_NAME = SymZ3TracePcodeExecutorStatePiece.NAME;
public static final GColor COLOR = new GColor("color.fg.listing.z3symbolic");
public static final String FIELD_NAME = "Z3 Symbolic Value";
public SymZ3FieldFactory() {
super(FIELD_NAME);
}
protected SymZ3FieldFactory(FieldFormatModel formatModel,
ListingHighlightProvider highlightProvider, Options displayOptions,
Options fieldOptions) {
super(FIELD_NAME, formatModel, highlightProvider, displayOptions, fieldOptions);
}
@Override
public FieldFactory newInstance(FieldFormatModel formatModel,
ListingHighlightProvider highlightProvider, ToolOptions displayOptions,
ToolOptions fieldOptions) {
return new SymZ3FieldFactory(formatModel, highlightProvider, displayOptions, fieldOptions);
}
/**
* {@inheritDoc}
*
* <p>
* This is where the most of the rendering logic is. Here, we access the property map and
* deserialize into a {@link SymValueZ3} manually (as compared to using a state piece as we did
* in {@link SymZ3DebuggerRegisterColumnFactory}). Once we have the complete vector, we render
* it for display.
*/
@Override
public ListingField getField(ProxyObj<?> proxy, int varWidth) {
Object obj = proxy.getObject();
if (!enabled || !(obj instanceof CodeUnit)) {
return null;
}
CodeUnit cu = (CodeUnit) obj;
StringPropertyMap symMap =
cu.getProgram().getUsrPropertyManager().getStringPropertyMap(PROPERTY_NAME);
if (symMap == null) {
return null;
}
String display = symMap.get(cu.getAddress());
if (display == null) {
return null;
}
return ListingTextField.createSingleLineTextField(this, proxy,
new TextFieldElement(new AttributedString(display, COLOR, getMetrics()), 0, 0),
startX + varWidth, width, hlProvider);
}
/**
* {@inheritDoc}
*
* <p>
* Because the core framework provides an API for accessing and manipulating the user's cursor,
* we have to provide a means to distinguish locations in our field from others. This method
* provides on direction of the conversion between field and program locations.
*/
@Override
public FieldLocation getFieldLocation(ListingField bf, BigInteger index, int fieldNum,
ProgramLocation loc) {
if (!(loc instanceof SymZ3FieldLocation)) {
return null;
}
SymZ3FieldLocation tfLoc = (SymZ3FieldLocation) loc;
return new FieldLocation(index, fieldNum, 0, tfLoc.getCharOffset());
}
/**
* {@inheritDoc}
*
* <p>
* Because the core framework provides an API for accessing and manipulating the user's cursor,
* we have to provide a means to distinguish locations in our field from others. This method
* provides on direction of the conversion between field and program locations.
*/
@Override
public ProgramLocation getProgramLocation(int row, int col, ListingField bf) {
ProxyObj<?> proxy = bf.getProxy();
Object obj = proxy.getObject();
if (!(obj instanceof CodeUnit)) {
return null;
}
CodeUnit cu = (CodeUnit) obj;
return new SymZ3FieldLocation(proxy.getListingLayoutModel().getProgram(), cu.getAddress(),
col);
}
@Override
public boolean acceptsType(int category, Class<?> proxyObjectClass) {
return (category == FieldFormatModel.INSTRUCTION_OR_DATA);
}
}

View file

@ -0,0 +1,37 @@
/* ###
* 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.symz3.gui.field;
import ghidra.program.model.address.Address;
import ghidra.program.model.listing.Program;
import ghidra.program.util.CodeUnitLocation;
import ghidra.program.util.ProgramLocation;
/**
* This is a {@link ProgramLocation} for when the user's cursor is in our "SymZ3" field
*
* <p>
* I used the "sample" module's {@code EntropyFieldLocation} for reference.
*/
public class SymZ3FieldLocation extends CodeUnitLocation {
public SymZ3FieldLocation(Program program, Address address, int charOffset) {
super(program, address, 0, 0, charOffset);
}
// Need default for XML restore
public SymZ3FieldLocation() {
}
}

View file

@ -0,0 +1,20 @@
/* ###
* 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.
*/
/**
* UI components for the Symbolic Summarizer
*/
package ghidra.symz3.gui.field;

View file

@ -0,0 +1,430 @@
/* ###
* 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.
*/
/* 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.symz3.model;
import static ghidra.pcode.emu.symz3.SymZ3PcodeArithmetic.*;
import java.math.BigInteger;
import java.util.Objects;
import com.microsoft.z3.*;
import ghidra.pcode.emu.symz3.lib.Z3InfixPrinter;
import ghidra.pcode.exec.PcodeArithmetic.Purpose;
import ghidra.util.Msg;
/**
* A symbolic value consisting of a either a Z3 bit-vector expression, and an optional Z3 boolean
* expression. We could simply always use a bit-vector, but we are hoping to avoid simplification of
* complex ITE expressions. We explored having the value be either a bit-vector or a boolean, but
* problems arise when we need to create a new symbolic value for a register like "ZF" that from
* PCode perspective is a base register with 8 bits. Everything worked pretty much if we just made
* it a Boolean, but that seems very fragile. Thus, we won't need code to convert from Boolean back
* to bit-vector, because we will always have a bit-vector.
*/
public class SymValueZ3 {
@SuppressWarnings("unchecked")
public static String serialize(Context ctx, BitVecExpr b) {
// serialization is a bit goofy, because we must create a boolean expression
// see https://github.com/Z3Prover/z3/issues/2674.
Solver solver = ctx.mkSolver();
solver.add(ctx.mkEq(b, b));
return "V:" + solver.toString();
}
@SuppressWarnings("unchecked")
public static String serialize(Context ctx, BoolExpr b) {
Solver solver = ctx.mkSolver();
solver.add(b);
return "B:" + solver.toString();
}
// this is deserialization of a value from a string
public static SymValueZ3 parse(String serialized) {
int index = serialized.indexOf(":::::");
String left = serialized.substring(0, index);
String right = serialized.substring(index + 5);
return new SymValueZ3(left, right);
}
public static BitVecExpr deserializeBitVecExpr(Context ctx, String s) {
assert s != null;
String smt = s.substring(2);
BoolExpr f = ctx.parseSMTLIB2String(smt, null, null, null, null)[0];
assert f != null;
assert s.charAt(0) == 'V';
return (BitVecExpr) f.getArgs()[0];
}
public static BoolExpr deserializeBoolExpr(Context ctx, String s) {
assert s != null;
String smt = s.substring(2);
BoolExpr f = ctx.parseSMTLIB2String(smt, null, null, null, null)[0];
assert f != null;
assert s.charAt(0) == 'B';
return f;
}
public final String bitVecExprString;
public final String boolExprString;
public SymValueZ3(Context ctx, BitVecExpr bve) {
this.bitVecExprString = serialize(ctx, bve);
this.boolExprString = null;
}
public SymValueZ3(Context ctx, BitVecExpr bve, BoolExpr be) {
this.bitVecExprString = serialize(ctx, bve);
this.boolExprString = serialize(ctx, be);
}
private SymValueZ3(String be, String bve) {
if (be.isEmpty()) {
this.boolExprString = null;
}
else {
this.boolExprString = be;
}
if (bve.isEmpty()) {
this.bitVecExprString = null;
}
else {
this.bitVecExprString = bve;
}
}
public BitVecExpr getBitVecExpr(Context ctx) {
return deserializeBitVecExpr(ctx, this.bitVecExprString);
}
public BoolExpr getBoolExpr(Context ctx) {
if (this.boolExprString == null) {
BitVecExpr b = this.getBitVecExpr(ctx);
BitVecExpr zero = ctx.mkBV(0, b.getSortSize());
BoolExpr predicate = ctx.mkEq(b, zero);
return (BoolExpr) ctx.mkITE(predicate, ctx.mkFalse(), ctx.mkTrue());
}
return deserializeBoolExpr(ctx, this.boolExprString);
}
public boolean hasBoolExpr() {
return this.boolExprString != null;
}
public boolean hasBitVecExpr() {
return this.bitVecExprString != null;
}
@Override
public String toString() {
return String.format("<SymValueZ3: %s>", toDisplay());
}
public String toDisplay() {
try (Context ctx = new Context()) {
Z3InfixPrinter z3p = new Z3InfixPrinter(ctx);
if (this.hasBoolExpr()) {
return z3p.infix(deserializeBoolExpr(ctx, boolExprString));
}
return z3p.infix(deserializeBitVecExpr(ctx, bitVecExprString));
}
}
@Override
public boolean equals(Object obj) {
if (this == obj) {
return true;
}
if (!(obj instanceof SymValueZ3 that)) {
return false;
}
return Objects.equals(this.bitVecExprString, that.bitVecExprString);
}
@Override
public int hashCode() {
return Objects.hash(this.bitVecExprString);
}
public String serialize() {
String delimiter = ":::::";
if (this.hasBoolExpr()) {
return this.boolExprString + delimiter;
}
if (this.hasBitVecExpr()) {
return delimiter + this.bitVecExprString;
}
throw new AssertionError("attempted to serialize a null SymValueZ3");
}
/** {@return BigInteger value or null if not a BigInteger} */
public BigInteger toBigInteger() {
try (Context ctx = new Context()) {
BitVecExpr b = this.getBitVecExpr(ctx);
if (b == null || !b.isNumeral()) {
return null;
}
BitVecNum bvn = (BitVecNum) b;
try {
return bvn.getBigInteger();
}
catch (Exception e) {
return null;
}
}
}
/** {@return Long value or null if not a long} */
public Long toLong() {
try (Context ctx = new Context()) {
BitVecExpr b = this.getBitVecExpr(ctx);
if (b == null || !b.isNumeral()) {
return null;
}
BitVecNum bvn = (BitVecNum) b;
try {
return bvn.getLong();
}
catch (Exception e) {
Msg.info(this, "tolong invoked bit not a long returning null " + this);
return null;
}
}
}
private interface Z3CmpOp {
BoolExpr apply(Context ctx, BitVecExpr l, BitVecExpr r);
}
private static SymValueZ3 ite(Context ctx, BoolExpr predicate) {
return new SymValueZ3(ctx, (BitVecExpr) ctx.mkITE(predicate, one(ctx), zero(ctx)));
}
private static SymValueZ3 ite(Context ctx, SymValueZ3 l, Z3CmpOp op, SymValueZ3 r) {
return ite(ctx, op.apply(ctx, l.getBitVecExpr(ctx), r.getBitVecExpr(ctx)));
}
private static SymValueZ3 iteInv(Context ctx, BoolExpr predicate) {
return new SymValueZ3(ctx, (BitVecExpr) ctx.mkITE(predicate, zero(ctx), one(ctx)));
}
private static SymValueZ3 iteInv(Context ctx, SymValueZ3 l, Z3CmpOp op, SymValueZ3 r) {
return iteInv(ctx, op.apply(ctx, l.getBitVecExpr(ctx), r.getBitVecExpr(ctx)));
}
public SymValueZ3 intEqual(Context ctx, SymValueZ3 that) {
return ite(ctx, this, Context::mkEq, that);
}
public SymValueZ3 intNotEqual(Context ctx, SymValueZ3 that) {
return iteInv(ctx, this, Context::mkEq, that);
}
public SymValueZ3 intSLess(Context ctx, SymValueZ3 that) {
return ite(ctx, this, Context::mkBVSLT, that);
}
public SymValueZ3 intSLessEqual(Context ctx, SymValueZ3 that) {
return ite(ctx, this, Context::mkBVSLE, that);
}
public SymValueZ3 intLess(Context ctx, SymValueZ3 that) {
return ite(ctx, this, Context::mkBVULT, that);
}
public SymValueZ3 intLessEqual(Context ctx, SymValueZ3 that) {
return ite(ctx, this, Context::mkBVULE, that);
}
public SymValueZ3 intZExt(Context ctx, int outSizeBytes) {
BitVecExpr bv = this.getBitVecExpr(ctx);
return new SymValueZ3(ctx, ctx.mkZeroExt(outSizeBytes * 8 - bv.getSortSize(), bv));
}
public SymValueZ3 intSExt(Context ctx, int outSizeBytes) {
BitVecExpr bv = this.getBitVecExpr(ctx);
return new SymValueZ3(ctx, ctx.mkSignExt(outSizeBytes * 8 - bv.getSortSize(), bv));
}
private interface Z3BinBitVecOp {
BitVecExpr apply(Context ctx, BitVecExpr l, BitVecExpr r);
}
private static SymValueZ3 binBitVec(Context ctx, SymValueZ3 l, Z3BinBitVecOp op, SymValueZ3 r) {
return new SymValueZ3(ctx, op.apply(ctx, l.getBitVecExpr(ctx), r.getBitVecExpr(ctx)));
}
public SymValueZ3 intAdd(Context ctx, SymValueZ3 that) {
return binBitVec(ctx, this, Context::mkBVAdd, that);
}
public SymValueZ3 intSub(Context ctx, SymValueZ3 that) {
return binBitVec(ctx, this, Context::mkBVSub, that);
}
private static BoolExpr carry(Context ctx, BitVecExpr l, BitVecExpr r) {
return ctx.mkBVAddNoOverflow(l, r, false);
}
public SymValueZ3 intCarry(Context ctx, SymValueZ3 that) {
return iteInv(ctx, this, SymValueZ3::carry, that);
}
private static BoolExpr scarry(Context ctx, BitVecExpr l, BitVecExpr r) {
return ctx.mkBVAddNoOverflow(l, r, true);
}
public SymValueZ3 intSCarry(Context ctx, SymValueZ3 that) {
return iteInv(ctx, this, SymValueZ3::scarry, that);
}
public SymValueZ3 intSBorrow(Context ctx, SymValueZ3 that) {
return iteInv(ctx, this, Context::mkBVSubNoOverflow, that);
}
public SymValueZ3 intXor(Context ctx, SymValueZ3 that) {
return binBitVec(ctx, this, Context::mkBVXOR, that);
}
public SymValueZ3 intAnd(Context ctx, SymValueZ3 that) {
return binBitVec(ctx, this, Context::mkBVAND, that);
}
public SymValueZ3 intOr(Context ctx, SymValueZ3 that) {
return binBitVec(ctx, this, Context::mkBVOR, that);
}
private static BitVecExpr matchSortSize(Context ctx, int sizeBits, BitVecExpr bv) {
if (bv.getSortSize() == sizeBits) {
return bv;
}
if (bv.getSortSize() > sizeBits) {
return ctx.mkExtract(sizeBits - 1, 0, bv);
}
return ctx.mkZeroExt(sizeBits - bv.getSortSize(), bv);
}
private static SymValueZ3 shift(Context ctx, SymValueZ3 value, Z3BinBitVecOp op,
SymValueZ3 amt) {
BitVecExpr valBv = value.getBitVecExpr(ctx);
BitVecExpr normAmt = matchSortSize(ctx, valBv.getSortSize(), amt.getBitVecExpr(ctx));
return new SymValueZ3(ctx, op.apply(ctx, valBv, normAmt));
}
public SymValueZ3 intLeft(Context ctx, SymValueZ3 that) {
return shift(ctx, this, Context::mkBVSHL, that);
}
public SymValueZ3 intRight(Context ctx, SymValueZ3 that) {
return shift(ctx, this, Context::mkBVLSHR, that);
}
public SymValueZ3 intSRight(Context ctx, SymValueZ3 that) {
return shift(ctx, this, Context::mkBVASHR, that);
}
public SymValueZ3 intMult(Context ctx, SymValueZ3 that) {
return binBitVec(ctx, this, Context::mkBVMul, that);
}
public SymValueZ3 intDiv(Context ctx, SymValueZ3 that) {
return binBitVec(ctx, this, Context::mkBVUDiv, that);
}
public SymValueZ3 intSDiv(Context ctx, SymValueZ3 that) {
return binBitVec(ctx, this, Context::mkBVSDiv, that);
}
private interface Z3UnBoolOp {
BoolExpr apply(Context ctx, BoolExpr u);
}
private interface Z3BinBoolOp {
BoolExpr apply(Context ctx, BoolExpr l, BoolExpr r);
}
private interface Z3ArrBoolOp {
BoolExpr apply(Context ctx, BoolExpr... e);
}
private static SymValueZ3 unBool(Context ctx, Z3UnBoolOp op, SymValueZ3 u) {
return ite(ctx, op.apply(ctx, u.getBoolExpr(ctx)));
}
private static SymValueZ3 binBool(Context ctx, SymValueZ3 l, Z3BinBoolOp op, SymValueZ3 r) {
return ite(ctx, op.apply(ctx, l.getBoolExpr(ctx), r.getBoolExpr(ctx)));
}
private static SymValueZ3 binABool(Context ctx, SymValueZ3 l, Z3ArrBoolOp op, SymValueZ3 r) {
return ite(ctx, op.apply(ctx, l.getBoolExpr(ctx), r.getBoolExpr(ctx)));
}
public SymValueZ3 boolNegate(Context ctx) {
return unBool(ctx, Context::mkNot, this);
}
public SymValueZ3 boolXor(Context ctx, SymValueZ3 that) {
return binBool(ctx, this, Context::mkXor, that);
}
public SymValueZ3 boolAnd(Context ctx, SymValueZ3 that) {
return binABool(ctx, this, Context::mkAnd, that);
}
public SymValueZ3 boolOr(Context ctx, SymValueZ3 that) {
return binABool(ctx, this, Context::mkOr, that);
}
public SymValueZ3 piece(Context ctx, SymValueZ3 that) {
return binBitVec(ctx, this, Context::mkConcat, that);
}
public SymValueZ3 subpiece(Context ctx, int outSizeBytes, SymValueZ3 that) {
int outSizeBits = outSizeBytes * 8;
BitVecExpr thisBv = this.getBitVecExpr(ctx);
int thisSizeBits = thisBv.getSortSize();
int shiftBits = isInt(that.getBitVecExpr(ctx), Purpose.BY_DEF) * 8;
BitVecExpr out = thisSizeBits - shiftBits > outSizeBits
? ctx.mkExtract(outSizeBits + shiftBits - 1, shiftBits, thisBv)
: ctx.mkExtract(thisSizeBits - 1, shiftBits, thisBv);
return new SymValueZ3(ctx, out);
}
public SymValueZ3 popcount(Context ctx, int outSizeBytes) {
BitVecExpr outBv = ctx.mkBV(0, outSizeBytes * 8);
BitVecExpr thisBv = this.getBitVecExpr(ctx);
for (int i = 0; i < thisBv.getSortSize(); i++) {
BitVecExpr theBit = ctx.mkZeroExt(outBv.getSortSize() - 1, ctx.mkExtract(i, i, thisBv));
outBv = ctx.mkBVAdd(outBv, theBit);
}
return new SymValueZ3(ctx, outBv);
}
}

View file

@ -0,0 +1,19 @@
/* ###
* 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 Symbolic Value Z3 domain package
*/
package ghidra.symz3.model;

View file

@ -0,0 +1,23 @@
/* ###
* 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 Symbolic Z3 Analysis module
*
* <p>
* This emulator was based on the TaintAnalaysis module, but was modified to support the intended
* purpose (creating symbolic Z3 expressions).
*/
package ghidra.symz3;

View file

@ -0,0 +1,366 @@
/* ###
* 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.bugTest;
import static org.junit.Assert.assertEquals;
import org.apache.commons.lang3.tuple.ImmutablePair;
import org.apache.commons.lang3.tuple.Pair;
import org.junit.*;
import db.Transaction;
import ghidra.app.plugin.assembler.Assembler;
import ghidra.app.plugin.assembler.Assemblers;
import ghidra.pcode.emu.linux.EmuLinuxAmd64SyscallUseropLibraryTest;
import ghidra.pcode.emu.symz3.SymZ3PcodeThread;
import ghidra.pcode.emu.symz3.lib.SymZ3EmuUnixFileSystem;
import ghidra.pcode.emu.symz3.lib.SymZ3LinuxAmd64SyscallLibrary;
import ghidra.pcode.emu.symz3.plain.SymZ3PcodeEmulator;
import ghidra.pcode.exec.PcodeUseropLibrary;
import ghidra.program.model.address.Address;
import ghidra.program.model.address.AddressSpace;
import ghidra.program.model.lang.Language;
import ghidra.program.model.lang.Register;
import ghidra.program.model.listing.Program;
import ghidra.program.model.mem.MemoryBlock;
import ghidra.symz3.model.SymValueZ3;
import ghidra.test.AbstractGhidraHeadlessIntegrationTest;
import ghidra.util.Msg;
import ghidra.util.task.TaskMonitor;
public class SymZ3PcodeEmulatorBugTest extends AbstractGhidraHeadlessIntegrationTest {
protected final class LinuxAmd64SymZ3PcodeEmulator extends SymZ3PcodeEmulator {
public LinuxAmd64SymZ3PcodeEmulator() {
super(program.getLanguage());
}
@Override
protected PcodeUseropLibrary<Pair<byte[], SymValueZ3>> createUseropLibrary() {
return super.createUseropLibrary()
.compose(new SymZ3LinuxAmd64SyscallLibrary(this, fs, program));
}
}
protected static final byte[] BYTES_HW = "Hello, World!\n".getBytes();
private Program program;
private AddressSpace space;
private Address start;
private int size;
private MemoryBlock block;
private Assembler asm;
private SymZ3EmuUnixFileSystem fs;
private SymZ3PcodeEmulator emulator;
@Before
public void setUpSymZ3Test() throws Exception {
program = createDefaultProgram("HelloSymZ3", "x86:LE:64:default", "gcc", this);
space = program.getAddressFactory().getDefaultAddressSpace();
start = space.getAddress(0x00400000);
size = 0x1000;
try (Transaction tid = program.openTransaction("Initialize")) {
block = program.getMemory()
.createInitializedBlock(".text", start, size, (byte) 0, TaskMonitor.DUMMY,
false);
EmuLinuxAmd64SyscallUseropLibraryTest.SYSCALL_HELPER.bootstrapProgram(program);
}
asm = Assemblers.getAssembler(program);
}
@After
public void tearDownSymZ3Test() throws Exception {
if (program != null) {
program.release(this);
}
}
public void prepareEmulator() throws Exception {
// The emulator is not itself bound to the program or a trace, so copy bytes in
byte[] buf = new byte[size];
assertEquals(size, block.getBytes(start, buf));
emulator.getSharedState().getLeft().setVar(space, start.getOffset(), size, true, buf);
}
public SymZ3PcodeThread launchThread(Address pc) {
SymZ3PcodeThread thread = emulator.newThread();
thread.overrideCounter(start);
thread.overrideContextWithDefault();
thread.reInitialize();
return thread;
}
@Test
// Quick function check, add registers together and verify the output
public void testAdditionSummary() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"ADD RAX, RCX",
"ADD RAX, RBX" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
Msg.info(this, "ready for emulation");
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
//Execute instructions
for (int i = 0; i < instructions.length; i++) {
thread.stepInstruction();
}
emulator.printCompleteSummary(System.out);
thread.printRegisterComparison(System.out, "RAX");
//Test concrete and symbolic values of RAX
ImmutablePair<String, String> raxcompare = thread.registerComparison("RAX");
assertEquals(raxcompare.getLeft(), "0");
assertEquals(raxcompare.getRight(), "(RAX + RCX + RBX)");
}
@Test
// Simple test to see if memory store/loads of different sizes work
// Load into [RBP-0x18] as a qword, then make sure we can read it as a dword
public void testVarSize() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"MOV RAX, 1",
"MOV qword ptr [RBP + -0x18], RAX",
"MOV ECX, dword ptr [RBP + -0x18]" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
Msg.info(this, "ready for emulation");
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
//Execute instructions
for (int i = 0; i < instructions.length; i++) {
thread.stepInstruction();
}
emulator.printCompleteSummary(System.out);
thread.printRegisterComparison(System.out, "ECX");
thread.printRegisterComparison(System.out, "RAX");
ImmutablePair<String, String> raxcompare = thread.registerComparison("RAX");
assertEquals(raxcompare.getRight(), "(0x1:64)");
ImmutablePair<String, String> eaxcompare = thread.registerComparison("EAX");
assertEquals(eaxcompare.getRight(), "(0x1:32)");
assertEquals(eaxcompare.getLeft(), "1");
}
@Test
// Test to see if zero extend works with differently sized store/loads in the same memory location
// Load into [RBP-18] as a qword, then make sure we can read the same location with zero extend on a byte
public void testZeroExtend() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"MOV RAX, 0xdeadbeef",
"MOV qword ptr [RBP + -0x18], RAX",
"MOVZX ECX, byte ptr [RBP + -0x18]" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
Msg.info(this, "ready for emulation");
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
//Execute instructions
for (int i = 0; i < instructions.length; i++) {
thread.stepInstruction();
}
emulator.printCompleteSummary(System.out);
thread.printRegisterComparison(System.out, "RAX");
thread.printRegisterComparison(System.out, "ECX");
//Test that ECX recieves the bottom byte of RAX with zero extend
ImmutablePair<String, String> raxcompare = thread.registerComparison("RAX");
ImmutablePair<String, String> ecxcompare = thread.registerComparison("ECX");
//Test concrete values
String bottomByte = raxcompare.getLeft().substring(6, 8);
assertEquals(ecxcompare.getLeft(), bottomByte);
}
@Test
// Test CMOV instruction
// Using CMOVA (CMOV Above) on RSI and RDI, RDI = 0xdeadbeef and RSI = 0xdeadbeef + 1
public void testCMOVPass() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"MOV RDI, 0xdeadbeef",
"CMP RSI, RDI",
"CMOVA RSI, RDI" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
Msg.info(this, "ready for emulation");
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
Language language = thread.getLanguage();
Register regRSI = language.getRegister("RSI");
//Set RSI to 0xdeadbeef + 1 before executing instructions
byte[] initRSI = new byte[] { 0xd, 0xe, 0xa, 0xd, 0xb, 0xe, 0xf, 0x0 };
thread.getLocalConcreteState().setVar(regRSI, initRSI);
//Execute instructions
for (int i = 0; i < instructions.length; i++) {
thread.stepInstruction();
}
emulator.printCompleteSummary(System.out);
thread.printRegisterComparison(System.out, "RSI");
thread.printRegisterComparison(System.out, "RDI");
//Test concrete value of RSI to see if the move executed
ImmutablePair<String, String> rsicompare = thread.registerComparison("RSI");
assertEquals(rsicompare.getLeft(), "deadbeef");
}
@Test
// Test CMOV instruction
// Using CMOVA (CMOV Above) on RSI and RDI, RDI = 0xdeadbeef and RSI = 0 (implied)
public void testCMOVFail() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"MOV RDI, 0xdeadbeef",
"CMP RSI, RDI",
"CMOVA RSI, RDI" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
Msg.info(this, "ready for emulation");
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
//Execute instructions
for (int i = 0; i < instructions.length; i++) {
thread.stepInstruction();
}
emulator.printCompleteSummary(System.out);
thread.printRegisterComparison(System.out, "RSI");
thread.printRegisterComparison(System.out, "RDI");
//Test concrete value of RSI to see if the move executed
ImmutablePair<String, String> rsicompare = thread.registerComparison("RSI");
assertEquals(rsicompare.getLeft(), "0");
}
@Test
// Test size conversions
// REP takes the memory at RSI and puts it in the memory location RDI, an RCX number of times
// Not sure what the output looks like, current Z3 emulator can't handle REP instructions
public void testConversion() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"MOV EAX, dword ptr [RBP]",
"CDQE"
};
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
Msg.info(this, "ready for emulation");
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
for (int i = 0; i < instructions.length; i++) {
thread.stepInstruction();
}
emulator.printCompleteSummary(System.out);
thread.printRegisterComparison(System.out, "RAX");
//Test concrete value of RAX, should just be 0
ImmutablePair<String, String> raxcompare = thread.registerComparison("RAX");
assertEquals(raxcompare.getLeft(), "0");
}
@Test
// Test IMUL
// Code from 'arrayp' binary
public void testIMUL() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"MOV EAX, 0x3",
"MOV EDX, 0x5",
"IMUL ECX, EDX, 0x5" //EDX * EAX = 0xf
// "SAR EDX, 0x3", //EDX = 1
// "MOV EAX, ECX",
// "SAR EAX, 0x1f", //extend sign bit, EAX = 0
// "MOV EAX, EDX",
// "IMUL EAX, EAX, 0x1a", //EAX = EAX * 26 = 26
// "SUB ECX, EAX", //ECX = ECX - 0x1a
// "MOV EAX, ECX",
// "CDQE"
};
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
Msg.info(this, "ready for emulation");
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
for (int i = 0; i < instructions.length; i++) {
thread.stepInstruction();
}
emulator.printCompleteSummary(System.out);
thread.printRegisterComparison(System.out, "RCX");
//Test concrete value of RCX, should be 0x19
ImmutablePair<String, String> rcxcompare = thread.registerComparison("RCX");
assertEquals(rcxcompare.getLeft(), "19");
}
}

View file

@ -0,0 +1,151 @@
/* ###
* 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 static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertTrue;
import org.junit.Before;
import org.junit.Test;
import db.Transaction;
import ghidra.app.plugin.assembler.Assembler;
import ghidra.app.plugin.assembler.Assemblers;
import ghidra.app.plugin.core.debug.gui.AbstractGhidraHeadedDebuggerTest;
import ghidra.app.plugin.core.debug.service.emulation.DebuggerEmulationServicePlugin;
import ghidra.app.plugin.core.debug.service.modules.DebuggerStaticMappingServicePlugin;
import ghidra.app.services.DebuggerEmulationService;
import ghidra.app.services.DebuggerEmulationService.EmulationResult;
import ghidra.app.services.DebuggerStaticMappingService;
import ghidra.debug.api.emulation.DebuggerPcodeMachine;
import ghidra.pcode.emu.symz3.trace.SymZ3TracePcodeExecutorState;
import ghidra.pcode.emu.symz3.trace.SymZ3TracePcodeExecutorStatePiece;
import ghidra.program.model.util.StringPropertyMap;
import ghidra.program.util.ProgramLocation;
import ghidra.trace.model.*;
import ghidra.trace.model.property.TracePropertyMap;
import ghidra.trace.model.property.TracePropertyMapSpace;
import ghidra.trace.model.thread.TraceThread;
import ghidra.trace.model.time.schedule.*;
import ghidra.util.Msg;
import ghidra.util.task.TaskMonitor;
public class SymZ3DebuggerPcodeEmulatorTest extends AbstractGhidraHeadedDebuggerTest {
private DebuggerStaticMappingService mappingService;
private DebuggerEmulationService emuService;
@Before
public void setUpSymTest() throws Throwable {
mappingService = addPlugin(tool, DebuggerStaticMappingServicePlugin.class);
emuService = addPlugin(tool, DebuggerEmulationServicePlugin.class);
}
@Test
public void testFactoryDiscovered() {
assertEquals(1, emuService.getEmulatorFactories()
.stream()
.filter(f -> f instanceof SymZ3DebuggerPcodeEmulatorFactory)
.count());
}
@Test
public void testFactoryCreate() throws Exception {
emuService.setEmulatorFactory(new SymZ3DebuggerPcodeEmulatorFactory());
createAndOpenTrace();
try (Transaction tid = tb.startTransaction()) {
tb.getOrAddThread("Threads[0]", 0);
}
traceManager.activateTrace(tb.trace);
EmulationResult result =
emuService.run(tb.host, TraceSchedule.snap(0), monitor, new Scheduler() {
int calls = 0;
@Override
public TickStep nextSlice(Trace trace) {
// Expect decode of uninitialized memory immediately
assertEquals(0, calls++);
return new TickStep(0, 1);
}
});
DebuggerPcodeMachine<?> emu = emuService.getCachedEmulator(tb.trace, result.schedule());
assertTrue(emu instanceof SymZ3DebuggerPcodeEmulator);
SymZ3TracePcodeExecutorState state = (SymZ3TracePcodeExecutorState) emu.getSharedState();
Msg.debug(this, "here is your state: " + state);
}
@Test
public void testReadsProgramUsrProperties() throws Exception {
emuService.setEmulatorFactory(new SymZ3DebuggerPcodeEmulatorFactory());
createAndOpenTrace("x86:LE:64:default");
createProgramFromTrace();
intoProject(program);
intoProject(tb.trace);
programManager.openProgram(program);
TraceThread thread;
try (Transaction tid = tb.startTransaction()) {
mappingService.addMapping(
new DefaultTraceLocation(tb.trace, null, Lifespan.nowOn(0), tb.addr(0x55550000)),
new ProgramLocation(program, tb.addr(0x00400000)), 0x1000, false);
thread = tb.getOrAddThread("Threads[0]", 0);
tb.exec(0, thread, 0, """
RIP = 0x55550000;
""");
}
waitForDomainObject(tb.trace);
waitForPass(() -> assertEquals(new ProgramLocation(program, tb.addr(0x00400000)),
mappingService.getOpenMappedLocation(
new DefaultTraceLocation(tb.trace, null, Lifespan.at(0), tb.addr(0x55550000)))));
try (Transaction tid = program.openTransaction("Assemble")) {
program.getMemory()
.createInitializedBlock(".text", tb.addr(0x00400000), 0x1000, (byte) 0,
TaskMonitor.DUMMY, false);
StringPropertyMap progSymMap = program.getUsrPropertyManager()
.createStringPropertyMap(SymZ3TracePcodeExecutorStatePiece.NAME);
progSymMap.add(tb.addr(0x00400800), "test_0");
Assembler asm = Assemblers.getAssembler(program);
// TODO: I should be able to make this use a RIP-relative address
asm.assemble(tb.addr(0x00400000),
"MOV RAX, [0x55550800]"); // was [0x00400800], but fixed address is a problem.
}
TraceSchedule time = TraceSchedule.parse("0:t0-1");
long scratch = emuService.emulate(tb.trace, time, TaskMonitor.DUMMY);
TracePropertyMap<String> traceSymMap = tb.trace.getAddressPropertyManager()
.getPropertyMap(SymZ3TracePcodeExecutorStatePiece.NAME, String.class);
TracePropertyMapSpace<String> symRegSpace =
traceSymMap.getPropertyMapRegisterSpace(thread, 0, false);
Msg.info(this, symRegSpace.getEntries(Lifespan.at(scratch), tb.reg("RAX")));
//SymZ3DebuggerPcodeEmulator emu =
// (SymZ3DebuggerPcodeEmulator) emuService.getCachedEmulator(tb.trace, time);
//emu.printSymbolicSummary();
}
}

View file

@ -0,0 +1,273 @@
/* ###
* 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 static org.junit.Assert.assertEquals;
import java.math.BigInteger;
import org.apache.commons.lang3.tuple.ImmutablePair;
import org.apache.commons.lang3.tuple.Pair;
import org.junit.*;
import com.microsoft.z3.BitVecExpr;
import com.microsoft.z3.Context;
import db.Transaction;
import ghidra.app.plugin.assembler.Assembler;
import ghidra.app.plugin.assembler.Assemblers;
import ghidra.pcode.emu.PcodeThread;
import ghidra.pcode.emu.linux.EmuLinuxAmd64SyscallUseropLibraryTest;
import ghidra.pcode.emu.linux.EmuLinuxAmd64SyscallUseropLibraryTest.Syscall;
import ghidra.pcode.emu.symz3.SymZ3PcodeThread;
import ghidra.pcode.emu.symz3.lib.*;
import ghidra.pcode.emu.sys.EmuProcessExitedException;
import ghidra.pcode.exec.PcodeUseropLibrary;
import ghidra.program.model.address.Address;
import ghidra.program.model.address.AddressSpace;
import ghidra.program.model.listing.Program;
import ghidra.program.model.mem.MemoryBlock;
import ghidra.symz3.model.SymValueZ3;
import ghidra.test.AbstractGhidraHeadlessIntegrationTest;
import ghidra.util.Msg;
import ghidra.util.task.TaskMonitor;
public class SymZ3PcodeEmulatorTest extends AbstractGhidraHeadlessIntegrationTest {
protected final class LinuxAmd64SymZ3PcodeEmulator extends SymZ3PcodeEmulator {
public LinuxAmd64SymZ3PcodeEmulator() {
super(program.getLanguage());
}
@Override
protected PcodeUseropLibrary<Pair<byte[], SymValueZ3>> createUseropLibrary() {
return super.createUseropLibrary()
.compose(new SymZ3LinuxAmd64SyscallLibrary(this, fs, program));
}
}
protected static final byte[] BYTES_HW = "Hello, World!\n".getBytes();
private Program program;
private AddressSpace space;
private Address start;
private int size;
private MemoryBlock block;
private Assembler asm;
private SymZ3EmuUnixFileSystem fs;
private SymZ3PcodeEmulator emulator;
@Before
public void setUpSymZ3Test() throws Exception {
program = createDefaultProgram("HelloSymZ3", "x86:LE:64:default", "gcc", this);
space = program.getAddressFactory().getDefaultAddressSpace();
start = space.getAddress(0x00400000);
size = 0x1000;
try (Transaction tid = program.openTransaction("Initialize")) {
block = program.getMemory()
.createInitializedBlock(".text", start, size, (byte) 0, TaskMonitor.DUMMY,
false);
EmuLinuxAmd64SyscallUseropLibraryTest.SYSCALL_HELPER.bootstrapProgram(program);
}
asm = Assemblers.getAssembler(program);
}
@After
public void tearDownSymZ3Test() throws Exception {
if (program != null) {
program.release(this);
}
}
public void prepareEmulator() throws Exception {
// The emulator is not itself bound to the program or a trace, so copy bytes in
byte[] buf = new byte[size];
assertEquals(size, block.getBytes(start, buf));
emulator.getSharedState().getLeft().setVar(space, start.getOffset(), size, true, buf);
}
public SymZ3PcodeThread launchThread(Address pc) {
SymZ3PcodeThread thread = emulator.newThread();
thread.overrideCounter(start);
thread.overrideContextWithDefault();
thread.reInitialize();
return thread;
}
@Test
public void testAHregister() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"ADD AH, AH",
"MOV RCX, RAX" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
thread.stepInstruction(instructions.length);
emulator.printCompleteSummary(System.out);
String rcxContents = thread.registerComparison("RCX").getRight();
assertEquals("(RAX[16:48] :: (RAX[8:8] * (0x2:8)) :: RAX[0:8])", rcxContents);
}
@Test
public void testLAHF() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"LAHF" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
prepareEmulator();
PcodeThread<?> thread = launchThread(start);
thread.stepInstruction(instructions.length);
emulator.printCompleteSummary(System.out);
}
@Test
public void testSAHFandPUSHF() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] { "SAHF", "PUSHF" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
prepareEmulator();
PcodeThread<?> thread = launchThread(start);
thread.stepInstruction(instructions.length);
emulator.printCompleteSummary(System.out);
}
@Test
public void testFetchofBoolean() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"CLC",
"JA 0x00400632" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
prepareEmulator();
PcodeThread<?> thread = launchThread(start);
thread.stepInstruction(instructions.length);
emulator.printCompleteSummary(System.out);
}
@Test
public void testAdditionSummary() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"ADD RAX, RCX",
"ADD RAX, RBX" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
thread.stepInstruction(instructions.length);
emulator.printCompleteSummary(System.out);
thread.printRegisterComparison(System.out, "RAX");
ImmutablePair<String, String> comparison = thread.registerComparison("RAX");
assertEquals(comparison.getRight(), "(RAX + RCX + RBX)");
Msg.info(this, "Z3 Version: " + com.microsoft.z3.Version.getFullVersion());
}
@Test
public void testSymZ3Twobytes() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start,
"MOV dword ptr [RBP + -0x18],EAX",
"MOVZX EAX,byte ptr [RBP + -0x10]",
"MOVZX EAX,AL",
"SHL EAX,0x8",
"MOV EDX,EAX",
"MOVZX EAX,byte ptr [RBP + -0xf]",
"MOVZX EAX,AL",
"OR EAX,EDX",
"MOV word ptr [RBP + -0x1a],AX",
"CMP word ptr [RBP + -0x1a],0x6162",
"JZ 0x00400632",
"MOV byte ptr [RBP + -0x11],0x30",
"MOV RAX," + Syscall.GROUP_EXIT.number,
"MOV RDI,0",
"SYSCALL");
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
try {
thread.run();
}
catch (EmuProcessExitedException e) {
Msg.info(this, "exit");
}
emulator.printCompleteSummary(System.out);
thread.printRegisterComparison(System.out, "RAX");
ImmutablePair<String, String> comparison = thread.registerComparison("RAX");
assertEquals("(0x" + comparison.getLeft() + ":64)", comparison.getRight()); // same syscall
// TODO: need an assert about the precondition
}
@Test
public void testIsNegativeConstant() throws Exception {
try (Context ctx = new Context()) {
Z3InfixPrinter z3p = new Z3InfixPrinter(ctx);
BitVecExpr negone = ctx.mkBV(-1, 32);
Msg.info(this, "as an expr: " + negone.getSExpr());
Msg.info(this, z3p.isNegativeConstant(negone));
assertEquals(BigInteger.ONE, z3p.isNegativeConstant(negone));
}
}
@Test
public void testSerialization() throws Exception {
try (Context ctx = new Context()) {
SymValueZ3 one = new SymValueZ3(ctx, ctx.mkBV(123, 8));
Msg.info(this, one.getBitVecExpr(ctx).getSExpr());
//SymValueZ3 b = new SymValueZ3(ctx,ctx.mkTrue());
//Msg.info(this, b.getBoolExpr(ctx).getSExpr());
}
}
@Test
public void testSimpleMemory() throws Exception {
emulator = new LinuxAmd64SymZ3PcodeEmulator();
String[] instructions = new String[] {
"MOV EAX, 0xdeadbeef",
"MOV dword ptr [RBP + -0x18],EAX",
"MOV ECX, dword ptr[RBP + -0x18]" };
try (Transaction tid = program.openTransaction("Initialize")) {
asm.assemble(start, instructions);
block.putBytes(space.getAddress(0x00400880), "myfile\0".getBytes());
}
prepareEmulator();
SymZ3PcodeThread thread = launchThread(start);
thread.stepInstruction(instructions.length);
emulator.printCompleteSummary(System.out);
thread.printRegisterComparison(System.out, "RAX");
thread.printRegisterComparison(System.out, "RCX");
thread.printMemoryComparisonRegPlusOffset(System.out, "RBP", -0x18);
}
}

View file

@ -0,0 +1,295 @@
/* ###
* 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.List;
import org.apache.commons.lang3.tuple.Pair;
import org.junit.Test;
import com.microsoft.z3.BitVecExpr;
import com.microsoft.z3.Context;
import db.Transaction;
import ghidra.pcode.emu.PcodeThread;
import ghidra.pcode.exec.PcodeExecutorStatePiece.Reason;
import ghidra.pcode.exec.trace.AbstractTracePcodeEmulatorTest;
import ghidra.program.model.address.Address;
import ghidra.program.model.address.AddressSpace;
import ghidra.program.model.lang.Register;
import ghidra.symz3.model.SymValueZ3;
import ghidra.trace.database.ToyDBTraceBuilder;
import ghidra.trace.model.Lifespan;
import ghidra.trace.model.property.TracePropertyMap;
import ghidra.trace.model.property.TracePropertyMapSpace;
import ghidra.trace.model.thread.TraceThread;
import ghidra.util.Msg;
public class SymZ3TracePcodeEmulatorTest extends AbstractTracePcodeEmulatorTest {
/**
* Test that state is properly read from trace memory
*
* <p>
* We isolate exactly a read by executing sleigh.
*
* @throws Throwable because
*/
@Test
public void testReadStateMemory() throws Throwable {
try (ToyDBTraceBuilder tb = new ToyDBTraceBuilder("Test", "x86:LE:64:default")) {
TraceThread thread = initTrace(tb, "", List.of());
try (Transaction tid = tb.startTransaction()) {
TracePropertyMap<String> symMap = tb.trace.getAddressPropertyManager()
.getOrCreatePropertyMap(SymZ3TracePcodeExecutorStatePiece.NAME,
String.class);
try (Context ctx = new Context()) {
SymValueZ3 test = new SymValueZ3(ctx, ctx.mkBV(0, 8));
symMap.set(Lifespan.nowOn(0), tb.range(0x00400000, 0x00400003),
test.serialize());
}
}
SymZ3TracePcodeEmulator emu = new SymZ3TracePcodeEmulator(tb.host, 0);
PcodeThread<Pair<byte[], SymValueZ3>> emuThread = emu.newThread(thread.getPath());
emuThread.getExecutor().executeSleigh("RAX = *0x00400000:8;");
Pair<byte[], SymValueZ3> valRAX =
emuThread.getState().getVar(tb.language.getRegister("RAX"), Reason.INSPECT);
Msg.info(this, valRAX);
// TODO: assertion needed
}
}
@Test
public void testReadStateRegister() throws Throwable {
Msg.info(this, "");
Msg.info(this, "BEGIN testReadStateRegister");
try (ToyDBTraceBuilder tb = new ToyDBTraceBuilder("Test", "x86:LE:64:default")) {
TraceThread thread = initTrace(tb, "", List.of());
Register regRAX = tb.language.getRegister("RAX");
Register regEAX = tb.language.getRegister("EAX");
Register regRBX = tb.language.getRegister("RBX");
// TODO... test on EBX
try (Transaction tid = tb.startTransaction()) {
TracePropertyMap<String> symZ3Map = tb.trace.getAddressPropertyManager()
.getOrCreatePropertyMap(SymZ3TracePcodeExecutorStatePiece.NAME,
String.class);
TracePropertyMapSpace<String> mapSpace =
symZ3Map.getPropertyMapRegisterSpace(thread, 0, true);
mapSpace.set(Lifespan.nowOn(0), regRBX, "test_0");
}
SymZ3TracePcodeEmulator emu = new SymZ3TracePcodeEmulator(tb.host, 0);
PcodeThread<Pair<byte[], SymValueZ3>> emuThread = emu.newThread(thread.getPath());
try (Context ctx = new Context()) {
BitVecExpr e = ctx.mkBVConst("symbolic_RBX", 64);
SymValueZ3 symVal = new SymValueZ3(ctx, e);
emuThread.getState().setVar(tb.reg("RBX"), Pair.of(tb.arr(0, 0, 0, 0), symVal));
}
emuThread.getExecutor().executeSleigh("RAX = RBX;");
Msg.debug(this, "executed the line 'RAX = RBX'");
Pair<byte[], SymValueZ3> valRAX = emuThread.getState().getVar(regRAX, Reason.INSPECT);
Msg.info(this, "read the value of RAX:" + valRAX);
Pair<byte[], SymValueZ3> valEAX = emuThread.getState().getVar(regEAX, Reason.INSPECT);
Msg.info(this, "read the value of EAX:" + valEAX);
Msg.info(this, "END testReadStateRegister");
Msg.info(this, "");
}
}
@Test
public void testWriteStateMemory() throws Throwable {
try (ToyDBTraceBuilder tb = new ToyDBTraceBuilder("Test", "x86:LE:64:default")) {
initTrace(tb, "", List.of());
SymZ3TracePcodeEmulator emu = new SymZ3TracePcodeEmulator(tb.host, 0);
Address addr = tb.addr(0x00400000);
try (Context ctx = new Context()) {
BitVecExpr e = ctx.mkBVConst("symbolic_buffer", 64);
SymValueZ3 symVal = new SymValueZ3(ctx, e);
emu.getSharedState()
.setVar(tb.addr(0x00400000), 8, true,
Pair.of(tb.arr(0, 0, 0, 0, 0, 0, 0, 0), symVal));
}
try (Transaction tid = tb.startTransaction()) {
emu.writeDown(tb.host, 1, 0);
}
TracePropertyMap<String> map =
tb.trace.getAddressPropertyManager()
.getPropertyMap(SymZ3TracePcodeExecutorStatePiece.NAME, String.class);
TracePropertyMapSpace<String> backing =
map.getPropertyMapSpace(addr.getAddressSpace(), false);
Msg.info(this, "to pass this test, we fetch from backing:" + backing +
" with address: " + addr + " with offset: " + addr.getOffset());
Msg.info(this, backing.get(1, addr));
}
}
@Test
public void testWriteStateRegister() throws Throwable {
Msg.info(this, "");
Msg.info(this, "BEGIN testWriteStateRegister");
try (ToyDBTraceBuilder tb = new ToyDBTraceBuilder("Test", "x86:LE:64:default")) {
TraceThread thread = initTrace(tb, "", List.of());
SymZ3TracePcodeEmulator emu = new SymZ3TracePcodeEmulator(tb.host, 0);
PcodeThread<Pair<byte[], SymValueZ3>> emuThread = emu.newThread(thread.getPath());
try (Context ctx = new Context()) {
BitVecExpr e = ctx.mkBVConst("symbolic_EAX", 32);
SymValueZ3 symVal = new SymValueZ3(ctx, e);
emuThread.getState().setVar(tb.reg("EAX"), Pair.of(tb.arr(0, 0, 0, 0), symVal));
}
try (Transaction tid = tb.startTransaction()) {
emu.writeDown(tb.host, 1, 0);
// grab the name property from the abstract class....
TracePropertyMap<String> symMap =
tb.trace.getAddressPropertyManager()
.getPropertyMap(SymZ3TracePcodeExecutorStatePiece.NAME, String.class);
Msg.info(this, "we have a symMap: " + symMap);
TracePropertyMapSpace<String> mapSpace = symMap
.getPropertyMapRegisterSpace(thread, 0, true);
Msg.info(this, "we have a mapSpace: " + mapSpace);
Msg.info(this, "entries from the map space: " +
mapSpace.getEntries(Lifespan.at(1), tb.reg("EAX")));
}
Msg.info(this, "END testWriteStateRegister");
Msg.info(this, "");
}
}
@Test
public void testSymbolicMemory() throws Throwable {
try (ToyDBTraceBuilder tb = new ToyDBTraceBuilder("Test", "x86:LE:64:default")) {
AddressSpace ram = tb.language.getAddressFactory().getDefaultAddressSpace();
TraceThread thread = initTrace(tb, """
RIP = 0x00400000;
""",
List.of(
"MOV RBX, qword ptr [0x00600000]",
"MOV qword ptr [0x00600020], RBX",
"MOV dword ptr [RBP + -0x18],EAX",
"MOV qword ptr [RBP + -0x28],RAX",
"MOV RBP, qword ptr [RBP + -0x28]"));
SymZ3TracePcodeEmulator emu = new SymZ3TracePcodeEmulator(tb.host, 0);
PcodeThread<Pair<byte[], SymValueZ3>> emuThread = emu.newThread(thread.getPath());
emuThread.stepInstruction();
try (Transaction tid = tb.startTransaction()) {
emu.writeDown(tb.host, 1, 0);
}
emuThread.stepInstruction();
try (Transaction tid = tb.startTransaction()) {
emu.writeDown(tb.host, 2, 0);
}
emuThread.stepInstruction();
emuThread.stepInstruction();
emuThread.stepInstruction();
System.out.println("Instructions emulated:");
emu.printInstructions(System.out);
System.out.println("Pcode emulated:");
emu.printOps(System.out);
System.out.println("Summary:");
emu.printSymbolicSummary(System.out);
try (Transaction tid = tb.startTransaction()) {
emu.writeDown(tb.host, 5, 0);
}
TracePropertyMap<String> symMap =
tb.trace.getAddressPropertyManager()
.getPropertyMap(SymZ3TracePcodeExecutorStatePiece.NAME, String.class);
TracePropertyMapSpace<String> backing = symMap.getPropertyMapSpace(ram, false);
Msg.debug(this, "read: " +
backing.getEntries(Lifespan.at(5), tb.range(0x00600020, 0x00600027)));
}
}
@Test
public void testPrecondition() throws Throwable {
try (ToyDBTraceBuilder tb = new ToyDBTraceBuilder("Test", "x86:LE:64:default")) {
TraceThread thread = initTrace(tb, """
RIP = 0x00400000;
""",
List.of(
"MOV dword ptr [RBP + -0x18],EAX",
"MOVZX EAX, byte ptr [RBP + -0x28]"));
SymZ3TracePcodeEmulator emu = new SymZ3TracePcodeEmulator(tb.host, 0);
PcodeThread<Pair<byte[], SymValueZ3>> emuThread = emu.newThread(thread.getPath());
emuThread.stepInstruction();
try (Transaction tid = tb.startTransaction()) {
emu.writeDown(tb.host, 1, 0);
}
emuThread.stepInstruction();
try (Transaction tid = tb.startTransaction()) {
emu.writeDown(tb.host, 2, 0);
}
emu.printSymbolicSummary(System.out);
try (Transaction tid = tb.startTransaction()) {
emu.writeDown(tb.host, 5, 0);
}
TracePropertyMap<String> symMap =
tb.trace.getAddressPropertyManager()
.getPropertyMap(SymZ3TracePcodeExecutorStatePiece.NAME, String.class);
AddressSpace noSpace = Address.NO_ADDRESS.getAddressSpace();
TracePropertyMapSpace<String> backing = symMap.getPropertyMapSpace(noSpace, false);
Msg.debug(this, "read: " +
backing.getEntries(Lifespan.at(5), tb.range(0x00600020, 0x00600027)));
}
}
}

View file

@ -1,6 +1,6 @@
# Taint Analysis Module
This module is both a useful feature and a good reference for implementing a custom emulator
This module is both a useful feature and a good reference for implementing a custom emulator.
Users: see the help pages in Ghidra.

View file

@ -62,9 +62,9 @@ public class TaintSpace {
* Retrieve the taint sets for the variable at the given offset
*
* <p>
* This retrieves as many taint sets as there are elements in the given buffer vector. This
* first element becomes the taint set at the given offset, then each subsequent element becomes
* the taint set at each subsequent offset until the vector is filled. This is analogous to the
* This retrieves as many taint sets as there are elements in the given buffer vector. The first
* element becomes the taint set at the given offset, then each subsequent element becomes the
* taint set at each subsequent offset until the vector is filled. This is analogous to the
* manner in which bytes would be "read" from concrete state, starting at a given offset, into a
* destination array.
*

View file

@ -71,10 +71,7 @@ public class TaintTraceSpace extends TaintSpace {
* the property at the entry's offset. If the taint set is empty, we clear the property rather
* than putting the empty taint set into the property.
*
* @param map the backing object, which must now exist
* @param snap the destination snap
* @param thread if a register space, the destination thread
* @param frame if a register space, the destination frame
* @param into the trace-property access to write into
*/
public void writeDown(PcodeTracePropertyAccess<String> into) {
if (space.isUniqueSpace()) {

View file

@ -172,6 +172,7 @@ public class TaintPcodeEmulatorTest extends AbstractGhidraHeadlessIntegrationTes
"MOV RAX," + Syscall.CLOSE.number,
"MOV RDI,RBP",
"SYSCALL",
"MOV RAX," + Syscall.GROUP_EXIT.number,
"MOV RDI,0",

View file

@ -45,7 +45,7 @@ public class StringPcodeFormatter
return result;
}
static class ToStringAppender extends AbstractAppender<String> {
protected static class ToStringAppender extends AbstractAppender<String> {
private final StringBuffer buf = new StringBuffer();
private int lineCount = 0;

View file

@ -444,7 +444,7 @@ public abstract class AnnotatedPcodeUseropLibrary<T> implements PcodeUseropLibra
public <T> Object convert(Varnode vn, PcodeExecutor<T> executor) {
PcodeExecutorStatePiece<T, T> state = executor.getState();
PcodeArithmetic<T> arithmetic = executor.getArithmetic();
return arithmetic.toBoolean(state.getVar(vn, executor.getReason()), Purpose.OTHER);
return arithmetic.isTrue(state.getVar(vn, executor.getReason()), Purpose.OTHER);
}
}

View file

@ -0,0 +1,143 @@
/* ###
* 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;
import java.util.*;
import org.apache.commons.lang3.tuple.Pair;
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.lang.Register;
import ghidra.program.model.mem.MemBuffer;
/**
* A paired executor state
*
* <p>
* This composes a delegate state and piece "left" and "write" creating a single state which instead
* stores pairs of values, where the left component has the value type of the left state, and the
* right component has the value type of the right state. Note that each states is addressed using
* its own value type. Every operation on this state is decomposed into operations upon the delegate
* states, and the final result composed from the results of those operations.
*
* <p>
* Where a response cannot be composed of both states, the paired state defers to the left. In this
* way, the left state controls the machine, while the right is computed in tandem. The right never
* directly controls the machine
*
* @param <L> the type of values for the "left" state
* @param <R> the type of values for the "right" state
*/
public class IndependentPairedPcodeExecutorState<L, R>
implements PcodeExecutorState<Pair<L, R>> {
private final PcodeExecutorStatePiece<L, L> left;
private final PcodeExecutorStatePiece<R, R> right;
private final PcodeArithmetic<Pair<L, R>> arithmetic;
public IndependentPairedPcodeExecutorState(PcodeExecutorStatePiece<L, L> left,
PcodeExecutorStatePiece<R, R> right, PcodeArithmetic<Pair<L, R>> arithmetic) {
this.left = left;
this.right = right;
this.arithmetic = arithmetic;
}
/**
* Compose a paired state from the given left and right states
*
* @param left the state backing the left side of paired values ("control")
* @param right the state backing the right side of paired values ("auxiliary")
*/
public IndependentPairedPcodeExecutorState(PcodeExecutorStatePiece<L, L> left,
PcodeExecutorStatePiece<R, R> right) {
this(left, right, new PairedPcodeArithmetic<>(left.getArithmetic(), right.getArithmetic()));
}
@Override
public Language getLanguage() {
return left.getLanguage();
}
@Override
public PcodeArithmetic<Pair<L, R>> getArithmetic() {
return arithmetic;
}
@Override
public IndependentPairedPcodeExecutorState<L, R> fork() {
return new IndependentPairedPcodeExecutorState<>(left.fork(), right.fork(), arithmetic);
}
@Override
public Map<Register, Pair<L, R>> getRegisterValues() {
Map<Register, L> leftRVs = left.getRegisterValues();
Map<Register, R> rightRVs = right.getRegisterValues();
Set<Register> union = new HashSet<>();
union.addAll(leftRVs.keySet());
union.addAll(rightRVs.keySet());
Map<Register, Pair<L, R>> result = new HashMap<>();
for (Register k : union) {
result.put(k, Pair.of(leftRVs.get(k), rightRVs.get(k)));
}
return result;
}
@Override
public void setVar(AddressSpace space, Pair<L, R> offset, int size, boolean quantize,
Pair<L, R> val) {
left.setVar(space, offset.getLeft(), size, quantize, val.getLeft());
right.setVar(space, offset.getRight(), size, quantize, val.getRight());
}
@Override
public Pair<L, R> getVar(AddressSpace space, Pair<L, R> offset, int size, boolean quantize,
Reason reason) {
return Pair.of(
left.getVar(space, offset.getLeft(), size, quantize, reason),
right.getVar(space, offset.getRight(), size, quantize, reason));
}
@Override
public MemBuffer getConcreteBuffer(Address address, Purpose purpose) {
return left.getConcreteBuffer(address, purpose);
}
/**
* Get the delegate backing the left side of paired values
*
* @return the left state
*/
public PcodeExecutorStatePiece<L, L> getLeft() {
return left;
}
/**
* Get the delegate backing the right side of paired values
*
* @return the right state
*/
public PcodeExecutorStatePiece<R, R> getRight() {
return right;
}
@Override
public void clear() {
left.clear();
right.clear();
}
}

View file

@ -15,6 +15,7 @@
*/
package ghidra.pcode.exec;
import java.math.BigInteger;
import java.util.Objects;
import org.apache.commons.lang3.tuple.Pair;
@ -156,6 +157,22 @@ public class PairedPcodeArithmetic<L, R> implements PcodeArithmetic<Pair<L, R>>
return Pair.of(leftArith.fromConst(value), rightArith.fromConst(value));
}
@Override
public Pair<L, R> fromConst(long value, int size) {
return Pair.of(leftArith.fromConst(value, size), rightArith.fromConst(value, size));
}
@Override
public Pair<L, R> fromConst(BigInteger value, int size, boolean isContextreg) {
return Pair.of(leftArith.fromConst(value, size, isContextreg),
rightArith.fromConst(value, size, isContextreg));
}
@Override
public Pair<L, R> fromConst(BigInteger value, int size) {
return Pair.of(leftArith.fromConst(value, size), rightArith.fromConst(value, size));
}
@Override
public byte[] toConcrete(Pair<L, R> value, Purpose purpose) {
return leftArith.toConcrete(value.getLeft(), purpose);

View file

@ -62,6 +62,7 @@ public class PairedPcodeExecutorState<L, R> implements PcodeExecutorState<Pair<L
*
* @param left the state backing the left side of paired values ("control")
* @param right the state backing the right side of paired values ("auxiliary")
* @param arithmetic the arithmetic for the paired values of the state
*/
public PairedPcodeExecutorState(PcodeExecutorState<L> left,
PcodeExecutorStatePiece<L, R> right, PcodeArithmetic<Pair<L, R>> arithmetic) {

View file

@ -62,6 +62,8 @@ public interface PcodeArithmetic<T> {
LOAD(Reason.EXECUTE_READ),
/** The value will be used as the address of a value to store */
STORE(Reason.EXECUTE_READ),
/** The p-code specification defines the operand as a constant */
BY_DEF(Reason.EXECUTE_READ),
/** Some other reason, perhaps for userop library use */
OTHER(Reason.EXECUTE_READ),
/** The user or a tool is inspecting the value */
@ -561,26 +563,6 @@ public interface PcodeArithmetic<T> {
return Double.longBitsToDouble(toLong(value, purpose));
}
/**
* Convert, if possible, the given abstract value to a concrete boolean
*
* <p>
* Any non-zero value is considered true
*
* @param value the abstract value
* @param purpose the reason why the emulator needs a concrete value
* @return the concrete value
* @throws ConcretionError if the value cannot be made concrete
*/
default boolean toBoolean(T value, Purpose purpose) {
for (byte b : toConcrete(value, purpose)) {
if (b != 0) {
return true;
}
}
return false;
}
/**
* Get the size in bytes, if possible, of the given abstract value
*

View file

@ -16,6 +16,7 @@
package ghidra.app.util.pcode;
import java.util.*;
import java.util.stream.Stream;
import ghidra.app.plugin.processors.sleigh.template.*;
import ghidra.program.model.address.AddressFactory;
@ -58,6 +59,35 @@ public interface PcodeFormatter<T> {
*/
T formatTemplates(Language language, List<OpTpl> pcodeOpTemplates);
/**
* Convert one p-code op into a template, without re-writing relative branches.
*
* @param addrFactory the language's address factory
* @param pcodeOp the p-code op to convert
* @return p-code op template
*/
public static OpTpl getPcodeOpTemplateLog(AddressFactory addrFactory, PcodeOp pcodeOp) {
int opcode = pcodeOp.getOpcode();
Varnode v = pcodeOp.getOutput();
VarnodeTpl outputTpl = v == null ? null : getVarnodeTpl(addrFactory, v);
VarnodeTpl[] inputTpls = Stream.of(pcodeOp.getInputs())
.map(i -> getVarnodeTpl(addrFactory, i))
.toArray(VarnodeTpl[]::new);
return new OpTpl(opcode, outputTpl, inputTpls);
}
/**
* Convert flattened p-code ops into templates, without re-writing relative branches.
*
* @param addrFactory the language's address factory
* @param pcodeOps the p-code ops to convert
* @return p-code op templates
*/
public static List<OpTpl> getPcodeOpTemplatesLog(AddressFactory addrFactory,
List<PcodeOp> pcodeOps) {
return pcodeOps.stream().map(op -> getPcodeOpTemplateLog(addrFactory, op)).toList();
}
/**
* Convert flattened p-code ops into templates.
*
@ -68,17 +98,15 @@ public interface PcodeFormatter<T> {
public static List<OpTpl> getPcodeOpTemplates(AddressFactory addrFactory,
List<PcodeOp> pcodeOps) {
ArrayList<OpTpl> list = new ArrayList<OpTpl>();
HashMap<Integer, Integer> labelMap = new HashMap<Integer, Integer>(); // label offset to index map
// label offset to index map
HashMap<Integer, Integer> labelMap = new HashMap<Integer, Integer>();
for (int seq = 0; seq < pcodeOps.size(); seq++) {
PcodeOp pcodeOp = pcodeOps.get(seq);
int opcode = pcodeOp.getOpcode();
VarnodeTpl outputTpl = null;
Varnode v = pcodeOp.getOutput();
if (v != null) {
outputTpl = getVarnodeTpl(addrFactory, v);
}
VarnodeTpl outputTpl = v == null ? null : getVarnodeTpl(addrFactory, v);
Varnode[] inputs = pcodeOp.getInputs();
VarnodeTpl[] inputTpls = new VarnodeTpl[inputs.length];
@ -143,7 +171,7 @@ public interface PcodeFormatter<T> {
return new OpTpl(PcodeOp.PTRADD, null, new VarnodeTpl[] { input });
}
private static VarnodeTpl getVarnodeTpl(AddressFactory addrFactory, Varnode v) {
public static VarnodeTpl getVarnodeTpl(AddressFactory addrFactory, Varnode v) {
ConstTpl offsetTpl = new ConstTpl(ConstTpl.REAL, v.getOffset());
ConstTpl spaceTpl = new ConstTpl(v.getAddress().getAddressSpace());
ConstTpl sizeTpl = new ConstTpl(ConstTpl.REAL, v.getSize());

View file

@ -60,6 +60,16 @@ file("${REPO_DIR}/Ghidra/application.properties").withReader { reader ->
ext.RELEASE_VERSION = ghidraProps.getProperty('application.version')
}
// Z3 download versions (https://github.com/Z3Prover/z3/releases)
// NOTE: Changing these versions also requires appropriate changes to the sha256 values for each of
// the Z3 files specified in the dependency list below. These versions may also be specified
// elsewhere within the Ghidra source/build code.
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
ext.deps = [
[
name: "java-sarif-2.1-modified.jar",
@ -163,6 +173,39 @@ ext.deps = [
sha256: "98605c6b6b9214a945d844e41c85860d54649a45bca7873ef6991c0e93720787",
destination: FID_DIR
],
[
name: "z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}.zip", // Use this one for the Java jar
url: "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VER}/z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}.zip",
sha256: "93f91f9c6f4a00a041c19fc7a74adc1f441c8244ce70d486e19abcd89c6a014b",
destination: {
unzip(DOWNLOADS_DIR, DOWNLOADS_DIR, "z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}.zip")
copyDirectory(new File(DOWNLOADS_DIR, "z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}/bin/"), FLAT_REPO_DIR, new WildcardFileFilter("*.jar"))
}
],
[
name: "z3-${Z3_VER}-arm64-osx-${Z3_ARM64_OSX_VER}.zip", // macOS on Apple silicon
url: "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VER}/z3-${Z3_VER}-arm64-osx-${Z3_ARM64_OSX_VER}.zip",
sha256: "e23d03005558c1b5d3c1b8bd503e65b84edfe3f1ae4298bd8c4710b5b0a645eb",
destination: file("${DEPS_DIR}/SymbolicSummaryZ3")
],
[
name: "z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}.zip", // Linux on 64-bit Intel
url: "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VER}/z3-${Z3_VER}-x64-glibc-${Z3_X64_GLIBC_VER}.zip",
sha256: "93f91f9c6f4a00a041c19fc7a74adc1f441c8244ce70d486e19abcd89c6a014b",
destination: file("${DEPS_DIR}/SymbolicSummaryZ3")
],
[
name: "z3-${Z3_VER}-x64-osx-${Z3_X64_OSX_VER}.zip", // macOS on 64-bit Intel
url: "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VER}/z3-${Z3_VER}-x64-osx-${Z3_X64_OSX_VER}.zip",
sha256: "7598c2be3129429e83fb5082b92ae973f41a6a289873b4ea33180d9072067e80",
destination: file("${DEPS_DIR}/SymbolicSummaryZ3")
],
[
name: "z3-${Z3_VER}-x64-win.zip", // Windows on 64-bit Intel
url: "https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VER}/z3-${Z3_VER}-x64-win.zip",
sha256: "0a36dd5654fe423d23a727c4570c9db9a315926a4301189b868b6eb9bfd5979d",
destination: file("${DEPS_DIR}/SymbolicSummaryZ3")
],
[
name: "protobuf-6.31.0-py3-none-any.whl",
url: "https://files.pythonhosted.org/packages/ee/01/1ed1d482960a5718fd99c82f6d79120181947cfd4667ec3944d448ed44a3/protobuf-6.31.0-py3-none-any.whl",