Improve error messages during hornification (#39)

CERTCC · Apr 6, 2023 · 7e70d78 · 7e70d78
1 parent aa79a7f
commit 7e70d78
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 3 deletions.
diff --git a/src/main/java/kaiju/tools/ghihorn/hornifer/GhiHornifier.java b/src/main/java/kaiju/tools/ghihorn/hornifer/GhiHornifier.java
@@ -799,7 +799,7 @@ protected void hornifyCfg(final HornProgram hornProgram, final HornFunction horn
             // Go through each pcode operation and add it as an expression for
             // this block
             for (final PcodeOp pcode : vertex.getEntity().getPcode()) {
-                PcodeExpression pcX = new PcodeExpression(pcode);
+                PcodeExpression pcX = new PcodeExpression(pcode, vertex.getLocator());
                 pcX.getUseVariables().forEach(newBlock::addUseVariable);
                 pcX.getDefVariables().forEach(newBlock::addDefVariable);
                 newBlock.addExpression(pcode, pcX);

diff --git a/src/main/java/kaiju/tools/ghihorn/hornifer/horn/expression/PcodeExpression.java b/src/main/java/kaiju/tools/ghihorn/hornifer/horn/expression/PcodeExpression.java
@@ -6,6 +6,7 @@
 import com.microsoft.z3.BoolExpr;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.Sort;
+import ghidra.program.model.address.Address;
 import ghidra.program.model.pcode.HighVariable;
 import ghidra.program.model.pcode.PcodeOp;
 import ghidra.program.model.pcode.Varnode;
@@ -32,13 +33,20 @@ public class PcodeExpression implements HornExpression {
     private HornVariable outVariable;
     private HornExpression operation;
     private final PcodeOp pcode;
+    private Address address;
 
     /**
      * @param defVariables
      * @param useVariables
      * @param inVariables
      * @param outVariable
      */
+
+    public PcodeExpression(PcodeOp pcode, Address address) {
+        this(pcode);
+        this.address = address;
+    }
+
     public PcodeExpression(PcodeOp pcode) {
 
         this.defVariables = new ArrayList<>();
@@ -47,13 +55,23 @@ public PcodeExpression(PcodeOp pcode) {
         this.outVariable = null;
         this.operation = null;
         this.pcode = pcode;
+        this.address = null;
 
         // First the I/O variables must be computed
         try {
             computeIOVariables();
         } catch (Exception e) {
-            Msg.error(this, "Failed to generate variables for p-code: " + pcode);
-            throw new GhiHornException("Failed to generate variables for p-code: " + pcode + ". This is an issue with Ghidra's HighConstant class");
+            StringBuilder errorMessage = new StringBuilder("Failed to generate variables for p-code");
+            if (this.address != null) {
+                errorMessage.append(" at address " + this.address + ":");
+            } else {
+                errorMessage.append(":");
+            }
+            errorMessage.append(pcode);
+            errorMessage.append(", exception: " + e.getMessage());
+            errorMessage.append(". This is an issue with Ghidra's HighConstant class.");
+            Msg.error(this, errorMessage);
+            throw new GhiHornException(errorMessage.toString());
         }
 
         // Second the operations need to be generated from the I/O variables. This will