Merge remote-tracking branch 'origin/GP-7138_ryanmkurtz_Z3-tests'

(Closes #9464)
This commit is contained in:
Ryan Kurtz
2026-08-12 12:44:27 -04:00
5 changed files with 63 additions and 4 deletions
@@ -0,0 +1,44 @@
/* ###
* 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 static org.junit.Assume.*;
import ghidra.framework.Platform;
/**
* Utilities for SymZ3 testing
*/
public class SymZ3TestUtils {
/**
* Checks to make sure the current {@link Platform} is supported by our default native binary
* set. If it's not supported, the test this is called from is skipped with an appropriate
* message.
*/
public static void skipTestIfUnsupportedPlatform() {
boolean supportedPlatform = switch (Platform.CURRENT_PLATFORM) {
case WIN_X86_64:
case LINUX_X86_64:
case MAC_ARM_64:
case MAC_X86_64:
yield true;
default:
yield false;
};
assumeTrue("Skipping test: Running on an unsupported platform", supportedPlatform);
}
}
@@ -15,7 +15,7 @@
*/
package ghidra.pcode.emu.symz3.bugTest;
import static org.junit.Assert.assertEquals;
import static org.junit.Assert.*;
import org.apache.commons.lang3.tuple.ImmutablePair;
import org.apache.commons.lang3.tuple.Pair;
@@ -26,6 +26,7 @@ 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.SymZ3TestUtils;
import ghidra.pcode.emu.symz3.lib.SymZ3EmuUnixFileSystem;
import ghidra.pcode.emu.symz3.lib.SymZ3LinuxAmd64SyscallLibrary;
import ghidra.pcode.emu.symz3.state.SymZ3PcodeEmulator;
@@ -68,6 +69,8 @@ public class SymZ3PcodeEmulatorBugTest extends AbstractGhidraHeadlessIntegration
@Before
public void setUpSymZ3Test() throws Exception {
SymZ3TestUtils.skipTestIfUnsupportedPlatform();
program = createDefaultProgram("HelloSymZ3", "x86:LE:64:default", "gcc", this);
space = program.getAddressFactory().getDefaultAddressSpace();
start = space.getAddress(0x00400000);
@@ -15,8 +15,7 @@
*/
package ghidra.pcode.emu.symz3.full;
import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertTrue;
import static org.junit.Assert.*;
import org.junit.Before;
import org.junit.Test;
@@ -28,6 +27,7 @@ import ghidra.app.services.DebuggerEmulationService;
import ghidra.app.services.DebuggerEmulationService.EmulationResult;
import ghidra.pcode.emu.PcodeMachine;
import ghidra.pcode.emu.symz3.SymZ3EmulatorFactory;
import ghidra.pcode.emu.symz3.SymZ3TestUtils;
import ghidra.pcode.emu.symz3.state.SymZ3PcodeEmulator;
import ghidra.pcode.emu.symz3.state.SymZ3PcodeExecutorState;
import ghidra.trace.database.ToyDBTraceBuilder.ToySchemaBuilder;
@@ -43,6 +43,8 @@ public class SymZ3DebuggerPcodeEmulatorTest extends AbstractGhidraHeadedDebugger
@Before
public void setUpSymTest() throws Throwable {
SymZ3TestUtils.skipTestIfUnsupportedPlatform();
emuService = addPlugin(tool, DebuggerEmulationServicePlugin.class);
}
@@ -15,7 +15,7 @@
*/
package ghidra.pcode.emu.symz3.plain;
import static org.junit.Assert.assertEquals;
import static org.junit.Assert.*;
import java.math.BigInteger;
@@ -33,6 +33,7 @@ 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.SymZ3TestUtils;
import ghidra.pcode.emu.symz3.lib.*;
import ghidra.pcode.emu.symz3.state.SymZ3PcodeEmulator;
import ghidra.pcode.emu.sys.EmuProcessExitedException;
@@ -73,6 +74,8 @@ public class SymZ3PcodeEmulatorTest extends AbstractGhidraHeadlessIntegrationTes
@Before
public void setUpSymZ3Test() throws Exception {
SymZ3TestUtils.skipTestIfUnsupportedPlatform();
program = createDefaultProgram("HelloSymZ3", "x86:LE:64:default", "gcc", this);
space = program.getAddressFactory().getDefaultAddressSpace();
start = space.getAddress(0x00400000);
@@ -18,6 +18,7 @@ package ghidra.pcode.emu.symz3.trace;
import java.util.List;
import org.apache.commons.lang3.tuple.Pair;
import org.junit.Before;
import org.junit.Test;
import com.microsoft.z3.BitVecExpr;
@@ -26,6 +27,7 @@ import com.microsoft.z3.Context;
import db.Transaction;
import ghidra.pcode.emu.PcodeThread;
import ghidra.pcode.emu.symz3.SymZ3EmulatorFactory;
import ghidra.pcode.emu.symz3.SymZ3TestUtils;
import ghidra.pcode.emu.symz3.state.SymZ3PcodeEmulator;
import ghidra.pcode.emu.symz3.state.SymZ3PieceHandler;
import ghidra.pcode.exec.PcodeExecutorStatePiece.Reason;
@@ -56,6 +58,11 @@ public class SymZ3TracePcodeEmulatorTest extends AbstractTracePcodeEmulatorTest
return new SymZ3PcodeEmulator(platform.getLanguage(), writer.callbacks());
}
@Before
public void setUpSymTest() throws Throwable {
SymZ3TestUtils.skipTestIfUnsupportedPlatform();
}
/**
* Test that state is properly read from trace memory
*