Skip to content

Commit

Permalink
Merge pull request #49 from sei-eschwartz/main
Browse files Browse the repository at this point in the history
Several improvements to kaiju
  • Loading branch information
sei-eschwartz authored Sep 22, 2023
2 parents da38a32 + 9141930 commit 2563fec
Show file tree
Hide file tree
Showing 8 changed files with 126 additions and 47 deletions.
11 changes: 11 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,17 @@

# Current Release

## 240921

- Bugfixes:
* Fix packaged extensions so they can use the included z3 libraries
* Add workaround for when HighCFG entry vertex is incorrectly identified (Fix #40)
* Add workaround for #38, where an Indirect pcode op causes an exception

- Improvements:
* Improve UI responsiveness during DisasmImprovements
* Avoid relinking z3 when rebuilding with gradle

## 230921

- Updated to build extensions for Ghidra 10.3.1, 10.3.2, 10.3.3
Expand Down
39 changes: 23 additions & 16 deletions build.gradle
Original file line number Diff line number Diff line change
Expand Up @@ -221,7 +221,9 @@ task downloadAndUnzipZ3Source(dependsOn: downloadZ3Source, type: Copy) {
}
}

outputs.upToDateWhen { file('3rdparty/z3/CMakeLists.txt').exists() }
onlyIf {
!file('3rdparty/z3/CMakeLists.txt').exists()
}
}

buildExtension.dependsOn(downloadAndUnzipZ3Source)
Expand Down Expand Up @@ -275,15 +277,23 @@ cmake {
}

tasks.clean.dependsOn(tasks.cmakeClean)
tasks.build.dependsOn(tasks.cmakeBuild)
tasks.cmakeBuild.dependsOn(downloadAndUnzipZ3Source)
// since we are building the same version of z3, no need to rebuild
// once we built it once because it won't change
tasks.cmakeBuild.outputs.upToDateWhen( (output)-> {
file('build/cmake/z3/linux-amd64/libz3.so').exists() ||
file('build/cmake/z3/windows-amd64/libz3.dll').exists() ||
file('build/cmake/z3/osx-amd64/libz3.dylib').exists()
})

// This is our task for building z3. It's only really needed to work around a
// bug in the gradle cmake plugin that always causes linking to occur, which is
// slow because LTO. So we dynamically decide whether to set tasks.cmakeBuild as
// a dependency depending on whether z3 appears to be built.
task buildZ3 {
if (!(file('build/cmake/z3/linux-amd64/libz3.so').exists() ||
file('build/cmake/z3/windows-amd64/libz3.dll').exists() ||
file('build/cmake/z3/osx-amd64/libz3.dylib').exists())) {
logger.warn("We are adding a dependency")
dependsOn(tasks.cmakeBuild)
}
}

tasks.build.dependsOn(tasks.buildZ3)
buildExtension.dependsOn(tasks.buildZ3)
copyToLib.dependsOn(tasks.buildZ3)

project.getTasks().matching(
(task)-> {
Expand All @@ -295,17 +305,14 @@ project.getTasks().matching(
}
);

buildExtension.dependsOn(tasks.cmakeBuild)
copyToLib.dependsOn(tasks.cmakeBuild)

if (os.isLinux()) {
task copyZ3toOsLinux(type: Copy) {
from ("build/cmake/z3/linux-amd64/libz3.so")
from ("build/cmake/z3/linux-amd64/libz3java.so")
into "os/linux_x86_64"
}

copyZ3toOsLinux.dependsOn(tasks.cmakeBuild)
copyZ3toOsLinux.dependsOn(tasks.buildZ3)
copyToLib.dependsOn(copyZ3toOsLinux)
}

Expand All @@ -316,7 +323,7 @@ if (os.isWindows()) {
into "os/win_x86_64"
}

copyZ3toOsWin.dependsOn(tasks.cmakeBuild)
copyZ3toOsWin.dependsOn(tasks.buildZ3)
copyToLib.dependsOn(copyZ3toOsWin)
}

Expand All @@ -327,7 +334,7 @@ if (os.isMacOsX()) {
into "os/mac_x86_64"
}

copyZ3toOsMac.dependsOn(tasks.cmakeBuild)
copyZ3toOsMac.dependsOn(tasks.buildZ3)
copyToLib.dependsOn(copyZ3toOsMac)
}

Expand Down
19 changes: 9 additions & 10 deletions src/main/java/kaiju/tools/disasm/DisasmImprovementsAnalyzer.java
Original file line number Diff line number Diff line change
Expand Up @@ -195,26 +195,25 @@ public boolean added(final Program program, final AddressSetView set, final Task
// loop over the undefined addresses until either they are identified
// or there's no heuristics left to run.
// CancelledListener cancelledListener
GProgressBar progress = new GProgressBar​(null, true, true, true, 12);
progress.setMessage("Analyzing gaps...");
progress.initialize(0);
//GProgressBar progress = new GProgressBar​(null, true, true, true, 12);

long num_addrs_undefined = 0;
undefinedAddresses = this.listing.getUndefinedRanges(allAddresses, false, monitor);
for (final AddressRange range : undefinedAddresses) {
num_addrs_undefined += range.getLength();
}
progress.setMaximum(num_addrs_undefined);

long iteration = 0;

while (true) {
long changed = 0;
debug(this, "Analyzing gaps...");
iteration++;
debug(this, "Analyzing gaps (iteration " + iteration + ")...");
monitor.setMessage("Analyzing gaps (iteration " + iteration + ")...");

monitor.initialize(undefinedAddresses.getNumAddressRanges());
for (final AddressRange range : undefinedAddresses) {
monitor.checkCancelled();
//long range_change = improver.analyzeGap(range);
Pair<AddressRange, Integer> range_pair = improver.analyzeGap(range);
long range_change = range_pair.second;
progress.incrementProgress(range_change);
monitor.incrementProgress(1);
changed += range_change;
}
if (changed == 0)
Expand Down
43 changes: 27 additions & 16 deletions src/main/java/kaiju/tools/ghihorn/GhiHornPlugin.java
Original file line number Diff line number Diff line change
Expand Up @@ -85,10 +85,15 @@ public class GhiHornPlugin extends ProgramPlugin implements AutoAnalysisManagerL
KaijuNativeLibraryLoaderUtil.loadLibrary("z3");
KaijuNativeLibraryLoaderUtil.loadLibrary("z3java");
}

// Tell z3 not to reload the z3 libraries!
System.setProperty("z3.skipLibraryLoad", "true");

String z3status = "Z3 version: " + Version.getFullVersion();
z3LibsFound = true;
} catch (Throwable t) {
z3LibsFound = false;
Msg.warn(GhiHornPlugin.class, "Error while loading Z3 libraries: " + t.getMessage(), t);
}
}

Expand Down Expand Up @@ -152,14 +157,7 @@ protected void programActivated(final Program program) {

super.programActivated(program);

// Rerun auto analysis to remove/fix badness, such as non-returning
// functions
AutoAnalysisManager aam = AutoAnalysisManager.getAnalysisManager(program);
if (!aam.isAnalyzing()) {
Msg.info(this, "Rerunning auto-analysis");
aam.reAnalyzeAll(program.getMemory());
}

aam.addListener(this);

// Install a new action to show the GhiHorn interface
Expand All @@ -178,8 +176,21 @@ protected void programActivated(final Program program) {
.keyBinding("ctrl G")
.enabled(false)
.buildAndInstall(tool);

if (z3LibsFound) {
ghihornAction.setEnabled(true);
} else {
ghihornAction.setMenuBarData(new MenuData(new String[]{"&Kaiju", "GhiHorn is missing Z3"}));
}
} else {
Msg.info(this, "Running in headless mode, use the GhiHorn script!");

// Rerun auto analysis to remove/fix badness, such as non-returning
// functions
if (!aam.isAnalyzing()) {
Msg.info(this, "Rerunning auto-analysis");
aam.reAnalyzeAll(program.getMemory());
}
}

if (!SystemUtilities.isInHeadlessMode()) {
Expand All @@ -188,6 +199,8 @@ protected void programActivated(final Program program) {
this.apiDatabase = new GhiHornApiDatabase(new GhiHornParallelDecompiler(this.tool));
}

updateEntryPoints();

Msg.info(this, PLUGIN_NAME + " activated");
}

Expand Down Expand Up @@ -224,10 +237,7 @@ public ApiDatabase getApiDatabase() {
return this.apiDatabase;
}


@Override
public void analysisEnded(AutoAnalysisManager manager) {

public void updateEntryPoints() {
List<Address> entryPoints = new ArrayList<>();
AddressIterator ai = this.currentProgram.getSymbolTable().getExternalEntryPointIterator();

Expand All @@ -247,10 +257,11 @@ public void analysisEnded(AutoAnalysisManager manager) {

provider.setEntryPoints(entryPoints);

if (z3LibsFound) {
ghihornAction.setEnabled(true);
} else {
ghihornAction.setMenuBarData(new MenuData(new String[]{"&Kaiju", "GhiHorn is missing Z3"}));
}

}

@Override
public void analysisEnded(AutoAnalysisManager manager) {
updateEntryPoints();
}
}
29 changes: 27 additions & 2 deletions src/main/java/kaiju/tools/ghihorn/cfg/HighCfg.java
Original file line number Diff line number Diff line change
Expand Up @@ -274,7 +274,7 @@ private static List<PcodeOp> getPcodeInBBOrder(final PcodeBlockBasic bb) {
* The CFG builder. The CFG is constructed in a way that splits basic blocks
* when a call is made, which ghidra does not do by default. The resulting CFG
* is based on the addresses used in the high function p-code, which may not
* correspond to actuall basic block addresses, but should suffice for CHC
* correspond to actual basic block addresses, but should suffice for CHC
* encoding
*
* @param highFunction
Expand Down Expand Up @@ -389,7 +389,7 @@ public static HighCfg<Address, VertexAttributes> build(final HighFunction highFu
blockStopAddress = bb.getStop();
}

// Add the fiinal block or the only block
// Add the final block or the only block
final HighCfgVertex<Address, VertexAttributes> newVtx = new HighCfgVertex<>(blockStartAddress,
new VertexAttributes(new AddressSet(blockStartAddress, blockStopAddress),
bbPcodeList.subList(blockStartIndex, blockStopIndex + 1)));
Expand Down Expand Up @@ -531,6 +531,31 @@ public static HighCfg<Address, VertexAttributes> build(final HighFunction highFu
edge.setGuard(guard);
}

// Sometimes there is not a HighCFG vertex for the Function's entry point.
// This is a hack to try to find the entry point from the first pcode op.
if (cfg.getEntryVertex() == null) {
var firstop = highFunction.getPcodeOps().next();
var firstaddr = firstop.getSeqnum().getTarget();
// See if we can find the BB that contains firstaddr
var bbstart = (Address) null;
for (var bb : blocks) {
if (bb.contains(firstaddr)) {
bbstart = bb.getStart();
//cfg.setEntryLocation(bb.getStart());
break;
}
}
if (bbstart == null) {
throw new RuntimeException("No entry point found for function: " + highFunction.getFunction().getName() + ".");
} else {
Msg.warn(HighCfg.class, "No entry point found for function: " + highFunction.getFunction().getName() + ". I'm going to try the first pcode op at " + bbstart.toString() + ". This is experimental and might not work right!");
cfg.setEntryLocation(bbstart);
if (cfg.getEntryVertex() == null) {
throw new RuntimeException("The workaround did not work for function " + highFunction.getFunction().getName());
}
}
}

return cfg;
}

Expand Down
16 changes: 15 additions & 1 deletion src/main/java/kaiju/tools/ghihorn/hornifer/GhiHornifier.java
Original file line number Diff line number Diff line change
Expand Up @@ -348,13 +348,16 @@ public HornProgram hornify(final Program program, TaskMonitor monitor)
// rules/relations for each function. Calls will be connected in
// subseqent steps

monitor.setMessage("Hornifying function " + hornFunction.getName());

hornifyFunction(hornProgram, hornFunction, monitor);

monitor.setMessage("Completed hornification of function " + hornFunction.getName());
monitor.incrementProgress(1);
}

Msg.info(this, "Hornification completed");
monitor.setMessage("Encoding function calls");
monitor.setIndeterminate(true);
Msg.info(this, "Encoding function calls");

// Encoding the function instances makes the call connections
Expand All @@ -376,6 +379,7 @@ public HornProgram hornify(final Program program, TaskMonitor monitor)
Msg.info(this, "Encoding completed");

Msg.info(this, "Propagating state through calls");
monitor.setMessage("Propagating state through calls");

// Once all the connections have been made propgate the state based on calls
propagateStateThruCalls(hornProgram);
Expand Down Expand Up @@ -783,6 +787,7 @@ protected void hornifyCfg(final HornProgram hornProgram, final HornFunction horn

var highCfg = hornFunction.getHighCfg();
if (highCfg == null) {
Msg.warn(this, "No CFG for function " + hornFunction.getName());
return;
}

Expand Down Expand Up @@ -869,6 +874,11 @@ protected void hornifyCfg(final HornProgram hornProgram, final HornFunction horn
// (external) API
if (calledFunc == null) {
CodeUnit cu = listing.getCodeUnitAt(calledAddr);
if (cu == null) {
throw new RuntimeException("Cannot find code unit at " + calledAddr
+ " for call at " + endPcode.getSeqnum().getTarget()
+ " in function " + hornFunction.getName());
}
Reference ref = cu.getPrimaryReference(0);
if (ref != null) {
Symbol s = cu.getProgram().getSymbolTable()
Expand Down Expand Up @@ -1054,6 +1064,8 @@ protected void hornifyFunction(final HornProgram hornProgram, final HornFunction
HornVariable hvp = new HornVariable(param);
hornFunction.addParameter(p, hvp);
} else {
Msg.warn(this, "Unable to find HighParam for parameter " + p + " in function " +
function.getName() + " in program " + program.getName());
HornVariable hvp = new HornVariable();
hornFunction.addParameter(p, hvp);
}
Expand Down Expand Up @@ -1268,6 +1280,8 @@ public void maxProgressChanged(long id, GhiHornArgument<?> item,
queue.addProgressListener(progressListener);
queue.add(arguments);

monitor.setMessage("Solving horn clauses with Z3...");

try {

// Every five seconds check for termination
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,9 @@ public static HornFunctionInstance createInstance(
// parameters

HornBlock entryBlock = hornFunction.getEntryBlock();
if (entryBlock == null) {
throw new RuntimeException("No entry block for function " + function.getName());
}
startLoc = new ProgramLocation(function.getProgram(), entryBlock.getStartAddress());

// TODO: Really handle multiple output parameters
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -55,15 +55,24 @@ public PcodeExpression(PcodeOp pcode) {
this.outVariable = null;
this.operation = null;
this.pcode = pcode;
this.address = null;
this.address = pcode.getSeqnum().getTarget();

if (pcode.getOpcode() == PcodeOp.INDIRECT) {
// INDIRECT pcodes are ignored by makeOperation(), but can still
// raise an exception when the input is a constant larger than 64
// bits. Ideally we should move the call to computeIOVariables into
// makeOperation, but for now we'll just exit early when we see
// INDIRECT.
return;
}

// First the I/O variables must be computed
try {
computeIOVariables();
} catch (Exception e) {
StringBuilder errorMessage = new StringBuilder("Failed to generate variables for p-code");
if (this.address != null) {
errorMessage.append(" at address " + this.address + ":");
errorMessage.append(" at address " + this.address.toString() + ": ");
} else {
errorMessage.append(":");
}
Expand Down

0 comments on commit 2563fec

Please sign in to comment.