GP-6412: restoring high-/low- absint options

GP-6412: restoring high-/low- absint options
GP-6412: first pass, untested
GP-6412: first pass, untested

Ghidra/Extensions/Lisa/ghidra_scripts/LisaLaunchScript.java

@@ -43,8 +43,8 @@ public class LisaLaunchScript extends GhidraScript {
 			return;
 		}
 
-		PcodeFrontend frontend = new PcodeFrontend();
-		Program p = frontend.doWork(currentProgram.getListing(), currentAddress);
+		PcodeFrontend frontend = new PcodeFrontend(state.getTool());
+		Program p = frontend.doWork(currentProgram.getListing(), currentAddress, false);
 
 		DefaultConfiguration conf = new DefaultConfiguration();
 		conf.serializeResults = true;

Ghidra/Extensions/Lisa/ghidra_scripts/Lisa_ResolveX86orX64LinuxSyscallsScript.java

@@ -297,7 +297,7 @@ public class Lisa_ResolveX86orX64LinuxSyscallsScript extends GhidraScript {
 		initLisa();
 		Set<CFG> cfgs = new HashSet<>();
 		for (Function func : funcsToCalls.keySet()) {
-			CFG cfg = frontend.visitFunction(func, func.getEntryPoint());
+			CFG cfg = frontend.visitFunction(func, func.getEntryPoint(), false);
 			cfgs.add(cfg);
 		}
 		it.unive.lisa.program.Program p = frontend.getProgram();
@@ -390,7 +390,7 @@ public class Lisa_ResolveX86orX64LinuxSyscallsScript extends GhidraScript {
 	}
 
 	private void initLisa() {
-		frontend = new PcodeFrontend();
+		frontend = new PcodeFrontend(state.getTool());
 
 		DefaultConfiguration conf = new DefaultConfiguration();
 		conf.serializeResults = true;

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/gui/LisaOptions.java

@@ -15,11 +15,13 @@
  */
 package ghidra.lisa.gui;
 
+import ghidra.framework.options.OptionsChangeListener;
 import ghidra.framework.options.ToolOptions;
 import ghidra.framework.plugintool.Plugin;
 import ghidra.lisa.pcode.analyses.*;
 import ghidra.program.model.listing.Program;
 import ghidra.util.HelpLocation;
+import ghidra.util.bean.opteditor.OptionsVetoException;
 import it.unive.lisa.DefaultConfiguration;
 import it.unive.lisa.analysis.dataflow.*;
 import it.unive.lisa.analysis.heap.*;
@@ -42,7 +44,7 @@ import it.unive.lisa.interprocedural.context.*;
 /**
  * Parameters used to control LiSA
  */
-public class LisaOptions {
+public class LisaOptions implements OptionsChangeListener {
 
 	// ResourceManager may be able to pull these from a configuration.
 
@@ -58,6 +60,9 @@ public class LisaOptions {
 	public final static String OP_KEY_LISA_ANALYSIS_POST = "Post-State (vs Pre-)";
 	public final static String OP_KEY_LISA_ANALYSIS_SHOW_TOP = "Display 'top' values";
 	public final static String OP_KEY_LISA_ANALYSIS_SHOW_UNIQUE = "Display 'unique' values";
+	public final static String OP_KEY_LISA_ANALYSIS_USE_HIGH_PCODE = "Use high pcode (experimental)";
+	public final static String OP_KEY_LISA_ANALYSIS_SIMPLIFICATION_STYLE =
+		"Decompiler simplification style";
 	public final static String OP_KEY_LISA_ANALYSIS_CALL_DEPTH = "Compute CFGs to Depth";
 	public final static String OP_KEY_LISA_ANALYSIS_THRESH = "Threshhold";
 
@@ -80,9 +85,11 @@ public class LisaOptions {
 	public final static boolean DEFAULT_LISA_ANALYSIS_POST = false;
 	public final static boolean DEFAULT_LISA_ANALYSIS_SHOW_TOP = false;
 	public final static boolean DEFAULT_LISA_ANALYSIS_SHOW_UNIQUE = false;
-	public final static int DEFAULT_LISA_ANALYSIS_CALL_DEPTH = 0;
-	public final static int DEFAULT_LISA_ANALYSIS_THRESH = 5;
-
+	public final static boolean DEFAULT_LISA_ANALYSIS_USE_HIGH_PCODE = false;
+	public final static String DEFAULT_LISA_ANALYSIS_SIMPLIFICATION_STYLE = "normalize";
+	public final static int    DEFAULT_LISA_ANALYSIS_CALL_DEPTH = 0;
+	public final static int    DEFAULT_LISA_ANALYSIS_THRESH = 5;
+	
 	public final static String DEFAULT_LISA_ANALYSIS_OUTDIR = "";
 	public final static String DEFAULT_LISA_ANALYSIS_GRAPH = GraphOption.DEFAULT.optionString;
 	public final static boolean DEFAULT_LISA_ANALYSIS_SERIAL = false;
@@ -90,6 +97,8 @@ public class LisaOptions {
 	public final static String DEFAULT_LISA_TOP_REPRESENTATION = "#TOP#";
 	private static String suppress;  // Suppressed in results (typically #TOP#)
 
+	private LisaPlugin plugin;
+
 	private HeapDomainOption heapDomainOption;
 	private TypeDomainOption typeDomainOption;
 	private ValueDomainOption valueDomainOption;
@@ -106,6 +115,12 @@ public class LisaOptions {
 	private boolean postState;
 	private boolean showTop;
 	private boolean showUnique;
+	private boolean useHighPcode;
+	private String simplificationStyle;
+
+	public LisaOptions(LisaPlugin lisaPlugin) {
+		this.plugin = lisaPlugin;
+	}
 
 	public static enum HeapDomainOption {
 		HEAP_MONOLITHIC("Monolithic"),
@@ -166,9 +181,11 @@ public class LisaOptions {
 	public static enum ValueDomainOption {
 		VALUE_CONSTPROP("Numeric: ConstantPropagation"),
 		VALUE_INTERVAL("Numeric: Interval"),
+		VALUE_INTERVAL_LX86("Numeric: Interval (Low X86)"),
 		VALUE_POWERSET("Numeric: NonRedundantPowersetOfInterval"),
 		VALUE_PARITY("Numeric: Parity"),
 		VALUE_PENTAGON("Numeric: Pentagon"),
+		VALUE_PENTAGON_LX86("Numeric: Pentagon (Low X86)"),
 		VALUE_SIGN("Numeric: Sign"),
 		VALUE_UPPERBOUND("Numeric: UpperBound"),
 		DDATA_AVAILABLE("Dataflow: AvailableExpressions"),
@@ -197,7 +214,11 @@ public class LisaOptions {
 		@SuppressWarnings({ "rawtypes", "unchecked" })
 		public ValueDomain getDomain(Program program) {
 			suppress = DEFAULT_LISA_TOP_REPRESENTATION;
-			if (this == VALUE_INTERVAL || this == VALUE_POWERSET) {
+			if (this == VALUE_INTERVAL ||
+				this == VALUE_INTERVAL_LX86 ||
+				this == VALUE_PENTAGON ||
+				this == VALUE_PENTAGON_LX86 ||
+				this == VALUE_POWERSET) {
 				suppress = "[-Inf, +Inf]";
 			}
 			if (this == VALUE_UPPERBOUND) {
@@ -216,8 +237,10 @@ public class LisaOptions {
 				case VALUE_CONSTPROP -> new ValueEnvironment<>(
 					new PcodeByteBasedConstantPropagation(program.getLanguage()));
 				case VALUE_INTERVAL -> new ValueEnvironment<>(new PcodeInterval());
+				case VALUE_INTERVAL_LX86 -> new ValueEnvironment<>(new PcodeIntervalLowX86());
 				case VALUE_PARITY -> new ValueEnvironment<>(new PcodeParity());
 				case VALUE_PENTAGON -> new PcodePentagon();
+				case VALUE_PENTAGON_LX86 -> new PcodePentagonLowX86();
 				case VALUE_POWERSET -> new ValueEnvironment<>(
 					new PcodeNonRedundantPowersetOfInterval());
 				case VALUE_SIGN -> new ValueEnvironment<>(new PcodeSign());
@@ -461,6 +484,7 @@ public class LisaOptions {
 			"Call graph input");
 
 		grabFromToolAndProgram(ownerPlugin, opt, program);
+		opt.addOptionsChangeListener(this);
 	}
 
 	/**
@@ -490,8 +514,10 @@ public class LisaOptions {
 		callGraphOption = opt.getEnum(OP_KEY_LISA_ANALYSIS_CALL_GRAPH, CallGraphOption.RTA);
 		postState = opt.getBoolean(OP_KEY_LISA_ANALYSIS_POST, DEFAULT_LISA_ANALYSIS_POST);
 		showTop = opt.getBoolean(OP_KEY_LISA_ANALYSIS_SHOW_TOP, DEFAULT_LISA_ANALYSIS_SHOW_TOP);
-		showUnique =
-			opt.getBoolean(OP_KEY_LISA_ANALYSIS_SHOW_UNIQUE, DEFAULT_LISA_ANALYSIS_SHOW_UNIQUE);
+		showUnique = opt.getBoolean(OP_KEY_LISA_ANALYSIS_SHOW_UNIQUE, DEFAULT_LISA_ANALYSIS_SHOW_UNIQUE);
+		useHighPcode = opt.getBoolean(OP_KEY_LISA_ANALYSIS_USE_HIGH_PCODE, DEFAULT_LISA_ANALYSIS_USE_HIGH_PCODE);
+		simplificationStyle = opt.getString(OP_KEY_LISA_ANALYSIS_SIMPLIFICATION_STYLE,
+			DEFAULT_LISA_ANALYSIS_SIMPLIFICATION_STYLE);
 		cfgDepth = opt.getInt(OP_KEY_LISA_ANALYSIS_CALL_DEPTH, DEFAULT_LISA_ANALYSIS_CALL_DEPTH);
 		threshhold = opt.getInt(OP_KEY_LISA_ANALYSIS_THRESH, DEFAULT_LISA_ANALYSIS_THRESH);
 		outputDir = opt.getString(OP_KEY_LISA_ANALYSIS_OUTDIR, DEFAULT_LISA_ANALYSIS_OUTDIR);
@@ -612,6 +638,22 @@ public class LisaOptions {
 		this.showUnique = showUnique;
 	}
 
+	public boolean isHighPcode() {
+		return useHighPcode;
+	}
+
+	public void setHighPcode(boolean useHighPcode) {
+		this.useHighPcode = useHighPcode;
+	}
+
+	public String getSimplificationStyle() {
+		return simplificationStyle;
+	}
+
+	public void setSimplificationStyle(String style) {
+		this.simplificationStyle = style;
+	}
+
 	public GraphOption getGraphOption() {
 		return graphOption;
 	}
@@ -632,4 +674,12 @@ public class LisaOptions {
 		return suppress;
 	}
 
+	@Override
+	public void optionsChanged(ToolOptions options, String optionName, Object oldValue,
+			Object newValue) throws OptionsVetoException {
+		if (optionName.equals(OP_KEY_LISA_ANALYSIS_USE_HIGH_PCODE)) {
+			plugin.clearCfgs(null);
+		}	
+	}
+
 }

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/gui/LisaPlugin.java

@@ -96,7 +96,7 @@ public class LisaPlugin extends ProgramPlugin implements OptionsChangeListener,
 
 	public LisaPlugin(PluginTool tool) {
 		super(tool);
-		setOptions(new LisaOptions());
+		setOptions(new LisaOptions(this));
 		createActions();
 	}
 
@@ -268,7 +268,7 @@ public class LisaPlugin extends ProgramPlugin implements OptionsChangeListener,
 			return;
 		}
 		Msg.info(this, "Adding "+f);
-		CFG cfg = frontend.visitFunction(f, f.getEntryPoint());
+		CFG cfg = frontend.visitFunction(f, f.getEntryPoint(), options.isHighPcode());
 		cfgs.add(cfg);
 	}
 
@@ -278,6 +278,9 @@ public class LisaPlugin extends ProgramPlugin implements OptionsChangeListener,
 		}
 		Set<Function> calledFunctions = f.getCalledFunctions(new DummyCancellableTaskMonitor());
 		for (Function func : calledFunctions) {
+			if (func.isThunk()) {
+				continue;
+			}
 			Address entryPoint = func.getEntryPoint();
 			if (entryPoint.getAddressSpace().equals(f.getEntryPoint().getAddressSpace())) {
 				addFunction(cfgs, func);
@@ -286,7 +289,7 @@ public class LisaPlugin extends ProgramPlugin implements OptionsChangeListener,
 		}
 	}
 	
-	private void clearCfgs(ProgramLocationActionContext context) {
+	protected void clearCfgs(ProgramLocationActionContext context) {
 		initProgram();
 		frontend.clearTargets();
 	}
@@ -404,7 +407,7 @@ public class LisaPlugin extends ProgramPlugin implements OptionsChangeListener,
 	}
 
 	private void initProgram() {
-		frontend = new PcodeFrontend();
+		frontend = new PcodeFrontend(this.getTool());
 	}
 	
 	@SuppressWarnings("unchecked")

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/PcodeBranch.java

@@ -84,4 +84,12 @@ public class PcodeBranch extends ControlFlowStructure {
 		}
 	}
 
+	public Statement getBranch() {
+		return branch;
+	}
+
+	public Statement getFallThrough() {
+		return fallThrough;
+	}
+
 }

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/PcodeCodeMemberVisitor.java

@@ -22,7 +22,9 @@ import org.apache.commons.lang3.tuple.Pair;
 import ghidra.lisa.pcode.WorkItem.PredType;
 import ghidra.lisa.pcode.contexts.*;
 import ghidra.lisa.pcode.expressions.*;
+import ghidra.lisa.pcode.locations.PcodeLocation;
 import ghidra.lisa.pcode.statements.PcodeNop;
+import ghidra.program.model.address.Address;
 import ghidra.program.model.listing.Listing;
 import ghidra.program.model.pcode.PcodeOp;
 import ghidra.program.model.pcode.SequenceNumber;
@@ -64,7 +66,7 @@ public class PcodeCodeMemberVisitor {
 
 	private UnitContext currentUnit;
 
-	private Map<String, PcodeBranch> flows;
+	private Map<Address, PcodeBranch> flows;
 
 	private int varCount = 0;
 
@@ -181,7 +183,8 @@ public class PcodeCodeMemberVisitor {
 			}
 			PredType type = item.getType();
 			if (!type.equals(PredType.SEQ)) {
-				String loc = pred.getLocation().getCodeLocation();
+				PcodeLocation location = (PcodeLocation) pred.getLocation();
+				Address loc = location.getAddress();
 				PcodeBranch flow = flows.get(loc);
 				if (flow == null) {
 					flow = new PcodeBranch(cfg.getNodeList(), pred);
@@ -194,10 +197,12 @@ public class PcodeCodeMemberVisitor {
 		else {
 			entrypoints.add(st);
 		}
+
 		if (st instanceof Ret || st instanceof Return) {
 			return;
 		}
-		List<StatementContext> branches = ctx.branch(this.listing, this.currentUnit);
+
+		List<StatementContext> branches = currentUnit.branch(ctx, this.listing);
 		for (StatementContext branch : branches) {
 			WorkItem n = new WorkItem(st, branch);
 			if (ctx.isConditional()) {
@@ -205,7 +210,7 @@ public class PcodeCodeMemberVisitor {
 			}
 			workItems.add(n);
 		}
-		StatementContext next = ctx.next(this.listing);
+		StatementContext next = currentUnit.next(ctx, this.listing);
 		if (next != null) {
 			WorkItem n = new WorkItem(st, next);
 			if (ctx.isBranch()) {
@@ -273,6 +278,8 @@ public class PcodeCodeMemberVisitor {
 		PcodeContext right = ctx.expression();
 
 		int opcode = ctx.opcode();
+
+		// Special case logic first
 		switch (opcode) {
 			case PcodeOp.COPY -> {
 				Expression target = visitVariable(loc, left, true);
@@ -302,12 +309,20 @@ public class PcodeCodeMemberVisitor {
 				Expression expression = visitVarnode(loc, left, false);
 				return new Assignment(cfg, loc, target, expression);
 			}
+			case PcodeOp.MULTIEQUAL -> {
+				Expression target = visitVariable(loc, left, true);
+				//Expression expression = visitVariable(loc, left, true);
+				Expression expression = visitVarargsExpr(new VarargsExprContext(right));
+				return new Assignment(cfg, loc, target, expression);
+			}
 		}
 
 		if (right == null) {
 			throw new UnsupportedOperationException("Type of expression not supported: " + ctx);
 		}
 
+		// Everything else...
+		// NB: left is the output of the assignment, right the complete expression
 		return switch (right.getNumInputs()) {
 			case 1 -> {
 				Expression target = visitVariable(loc, left, true);
@@ -319,6 +334,12 @@ public class PcodeCodeMemberVisitor {
 				Expression expression = visitBinaryExpr(new BinaryExprContext(right));
 				yield new Assignment(cfg, loc, target, expression);
 			}
+			// NB: This may be unnecssary with the move of LOAD and STORE to the special-case section
+			case 3 -> {
+				Expression target = visitVariable(loc, left, true);
+				Expression expression = visitTernaryExpr(new TernaryExprContext(right));
+				yield new Assignment(cfg, loc, target, expression);
+			}
 			default -> throw new UnsupportedOperationException(
 				"Type of expression not supported: " + ctx);
 		};
@@ -343,8 +364,25 @@ public class PcodeCodeMemberVisitor {
 		return new PcodeBinaryExpression(cfg, ctx, lexp, rexp);
 	}
 
-	public Expression visitVarnode(CodeLocation loc, VarnodeContext ctx, Type type,
-			boolean define) {
+
+	public Expression visitTernaryExpr(TernaryExprContext ctx) {
+		CodeLocation loc = ctx.location();
+		Expression lexp = visitVariable(loc, ctx.left, false);
+		Expression mexp = visitVariable(loc, ctx.middle, false);
+		Expression rexp = visitVarnode(loc, ctx.right, false);
+		return new PcodeTernaryExpression(cfg, ctx, lexp, mexp, rexp);
+	}
+
+	public Expression visitVarargsExpr(VarargsExprContext ctx) {
+		CodeLocation loc = ctx.location();
+		Expression[] exps = new Expression[ctx.varargs.length];
+		for (int i = 0; i < ctx.varargs.length; i++) {
+			exps[i] = visitVariable(loc, ctx.varargs[i], false);
+		}
+		return new PcodeVarargsExpression(cfg, ctx, exps);
+	}
+
+	public Expression visitVarnode(CodeLocation loc, VarnodeContext ctx, Type type, boolean define) {
 		if (ctx.isConstant()) {
 			return visitConstant(loc, ctx);
 		}
@@ -384,7 +422,7 @@ public class PcodeCodeMemberVisitor {
 		return ref;
 	}
 
-	public Map<String, PcodeBranch> getFlows() {
+	public Map<Address, PcodeBranch> getFlows() {
 		return flows;
 	}
 

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/PcodeFrontend.java

@@ -17,6 +17,12 @@ package ghidra.lisa.pcode;
 
 import java.util.*;
 
+import ghidra.app.decompiler.*;
+import ghidra.app.decompiler.component.DecompilerUtils;
+import ghidra.framework.options.ToolOptions;
+import ghidra.framework.plugintool.PluginTool;
+import ghidra.lisa.gui.LisaOptions;
+import ghidra.lisa.pcode.contexts.HighUnitContext;
 import ghidra.lisa.pcode.contexts.UnitContext;
 import ghidra.lisa.pcode.locations.PcodeLocation;
 import ghidra.lisa.pcode.types.PcodeTypeSystem;
@@ -24,6 +30,8 @@ import ghidra.program.model.address.Address;
 import ghidra.program.model.lang.Register;
 import ghidra.program.model.lang.RegisterValue;
 import ghidra.program.model.listing.*;
+import ghidra.program.model.pcode.HighFunction;
+import ghidra.util.task.TaskMonitor;
 import it.unive.lisa.program.Program;
 import it.unive.lisa.program.cfg.*;
 import it.unive.lisa.program.cfg.Parameter;
@@ -38,18 +46,34 @@ public class PcodeFrontend {
 
 	//private static final Logger log = LogManager.getLogger(PcodeFrontend.class);
 
+	private PluginTool tool;
+	private ToolOptions options;
 	private final Program program;
 	private Map<Address, Set<Statement>> nodeMap = new HashMap<>();
 	private Map<Address, CFG> targets = new HashMap<>();
 	private Set<CFG> cfgs = new HashSet<>();
 
-	public PcodeFrontend() {
+	// High Pcode-only
+	private final Map<Function, HighFunction> decompCache = new HashMap<>();
+	private String simplificationStyle;
+
+	public PcodeFrontend(PluginTool tool) {
+		this.tool = tool;
+		ToolOptions[] optionsList = tool.getOptions();
+		for (ToolOptions opt : optionsList) {
+			if (opt.getName().equals("Abstract Interpretation")) {
+				this.options = opt;
+				simplificationStyle =
+					options.getString(LisaOptions.OP_KEY_LISA_ANALYSIS_SIMPLIFICATION_STYLE,
+						LisaOptions.DEFAULT_LISA_ANALYSIS_SIMPLIFICATION_STYLE);
+			}
+		}
 		program = new Program(new PcodeFeatures(), new PcodeTypeSystem());
 	}
 
-	public Program doWork(Listing listing, Address startAddress) {
+	public Program doWork(Listing listing, Address startAddress, boolean useHighPcode) {
 
-		Program p = visitListing(listing, startAddress);
+		Program p = visitListing(listing, startAddress, useHighPcode);
 
 		Collection<CFG> baseline = p.getAllCFGs();
 		for (CFG cfg : cfgs) {
@@ -60,36 +84,65 @@ public class PcodeFrontend {
 		return p;
 	}
 
-	public Program visitListing(Listing listing, Address startAddress) {
+	public Program visitListing(Listing listing, Address startAddress, boolean useHighPcode) {
 		Program p = getProgram();
 		for (Function f : listing.getFunctions(startAddress, false)) {
-			CFG cfg = visitFunction(f, startAddress);
+			CFG cfg = visitFunction(f, startAddress, useHighPcode);
 			cfgs.add(cfg);
 		}
 		return p;
 	}
 
-	public CFG visitFunction(Function f, Address start) {
+	public CFG visitFunction(Function f, Address start, boolean useHighPcode) {
 		Program p = getProgram();
-		UnitContext ctx = new UnitContext(this, program, f, start);
+		UnitContext ctx = getUnitContext(f, start, useHighPcode);
 
 		CodeMemberDescriptor descr = mkDescriptor(ctx);
 		PcodeCodeMemberVisitor visitor =
 			new PcodeCodeMemberVisitor(descr, ctx.getListing());
 		CFG cfg = visitor.visitCodeMember(ctx);
-		targets.put(f.getEntryPoint(), cfg);
-		cfgs.add(cfg);
-
-		ctx.unit().addCodeMember(cfg);
-		p.addUnit(ctx.unit());
 		Collection<Statement> nodes = cfg.getNodes();
 		for (Statement statement : nodes) {
 			Address addr = toAddr(statement.getLocation());
 			nodeMap.computeIfAbsent(addr, a -> new HashSet<>()).add(statement);
 		}
+
+		targets.put(f.getEntryPoint(), cfg);
+		cfgs.add(cfg);
+
+		ctx.unit().addCodeMember(cfg);
+		p.addUnit(ctx.unit());
 		return cfg;
 	}
 
+	private UnitContext getUnitContext(Function f, Address start, boolean useHighPcode) {
+		if (useHighPcode) {
+			DecompInterface decomp = null;
+			try {
+				decomp = new DecompInterface();
+				decomp.toggleSyntaxTree(true);
+				decomp.setSimplificationStyle(simplificationStyle);
+
+				DecompileOptions opts = DecompilerUtils.getDecompileOptions(tool, f.getProgram());
+				decomp.setOptions(opts);
+
+				decomp.openProgram(f.getProgram());
+				DecompileResults results =
+					decomp.decompileFunction(f, opts.getDefaultTimeout(), TaskMonitor.DUMMY);
+				HighFunction hfunc = results.getHighFunction();
+				return new HighUnitContext(this, program, f, hfunc, start);
+			}
+			finally {
+				if (decomp != null) {
+					decomp.closeProgram();
+					decomp.dispose();
+				}
+			}
+		}
+
+		return new UnitContext(this, program, f, start);
+	}
+
 	private Address toAddr(CodeLocation location) {
 		if (location instanceof PcodeLocation loc) {
 			return loc.op.getSeqnum().getTarget();

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/analyses/LongInterval.java

@@ -3,7 +3,6 @@
  */
 package ghidra.lisa.pcode.analyses;
 
-import java.math.BigDecimal;
 import java.util.Iterator;
 
 import it.unive.lisa.util.numeric.*;
@@ -185,8 +184,7 @@ public class LongInterval implements Iterable<Long>, Comparable<LongInterval> {
 	 * @return {@code true} if that condition holds
 	 */
 	public boolean is(long n) {
-		BigDecimal number = low.getNumber();
-		return isSingleton() && number != null && number.equals(new BigDecimal(n));
+		return isSingleton() && low.is((int) n);
 	}
 
 	private static LongInterval cacheAndRound(
@@ -235,6 +233,35 @@ public class LongInterval implements Iterable<Long>, Comparable<LongInterval> {
 		return cacheAndRound(new LongInterval(low.subtract(other.high), high.subtract(other.low)));
 	}
 
+	// NB: This is NOT really a set-theoretic complement because the domain doesn't support sets of
+	//   intervals.  Rather it handles two cases - (1) intervals unbounded at one end, and (2) intervals
+	//   representing booleans.  Caveat emptor.
+	public LongInterval complement() {
+		if (this.equals(ONE)) {
+			return ZERO;
+		}
+		if (this.equals(ZERO)) {
+			return ONE;
+		}
+		if (high.equals(INFINITY.getHigh())) {
+			return cacheAndRound(new LongInterval(INFINITY.getLow(), low.subtract(MathNumber.ONE)));
+		}
+		if (low.equals(INFINITY.getLow())) {
+			return cacheAndRound(new LongInterval(high.add(MathNumber.ONE), INFINITY.getHigh()));
+		}
+		return INFINITY;
+	}
+
+	public LongInterval flip() {
+		if (high.equals(INFINITY.getHigh())) {
+			return cacheAndRound(new LongInterval(INFINITY.getLow(), low));
+		}
+		if (low.equals(INFINITY.getLow())) {
+			return cacheAndRound(new LongInterval(high, INFINITY.getHigh()));
+		}
+		return INFINITY;
+	}
+
 	private static MathNumber min(
 			MathNumber... nums) {
 		if (nums.length == 0) {

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/analyses/PcodeByteBasedConstantPropagation.java

@@ -9,6 +9,7 @@ import java.util.Objects;
 import ghidra.lisa.pcode.locations.PcodeLocation;
 import ghidra.lisa.pcode.statements.PcodeBinaryOperator;
 import ghidra.pcode.exec.BytesPcodeArithmetic;
+import ghidra.pcode.opbehavior.*;
 import ghidra.pcode.utils.Utils;
 import ghidra.program.model.lang.Language;
 import ghidra.program.model.lang.RegisterValue;
@@ -152,6 +153,11 @@ public class PcodeByteBasedConstantPropagation
 
 		PcodeLocation ploc = (PcodeLocation) pp.getLocation();
 		PcodeOp op = ploc.op;
+		OpBehavior opBehavior = OpBehaviorFactory.getOpBehavior(op.getOpcode());
+		if (opBehavior instanceof SpecialOpBehavior) {
+			// TODO
+			return top();
+		}
 
 		byte[] bytes = arithmetic.unaryOp(op.getOpcode(), op.getOutput().getSize(),
 			op.getInput(0).getSize(), arg.getValue(op.getInput(0).getSize()));
@@ -183,6 +189,11 @@ public class PcodeByteBasedConstantPropagation
 
 		PcodeLocation ploc = (PcodeLocation) pp.getLocation();
 		PcodeOp op = ploc.op;
+		OpBehavior opBehavior = OpBehaviorFactory.getOpBehavior(op.getOpcode());
+		if (opBehavior instanceof SpecialOpBehavior) {
+			// TODO
+			return left;
+		}
 		if (left.isTop) {
 			return specialCaseLogic(op);
 		}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/analyses/PcodeDataflowConstantPropagation.java

@@ -8,6 +8,7 @@ import java.util.*;
 import ghidra.lisa.pcode.locations.InstLocation;
 import ghidra.lisa.pcode.locations.PcodeLocation;
 import ghidra.pcode.exec.BytesPcodeArithmetic;
+import ghidra.pcode.opbehavior.*;
 import ghidra.pcode.utils.Utils;
 import ghidra.program.model.address.Address;
 import ghidra.program.model.address.AddressFormatException;
@@ -134,13 +135,16 @@ public class PcodeDataflowConstantPropagation implements
 		PcodeOp op = ploc.op;
 
 		if (e instanceof UnaryExpression unary) {
-			Long i = eval(unary.getExpression(), pp, domain);
-
-			if (i == null) {
-				return i;
+			OpBehavior opBehavior = OpBehaviorFactory.getOpBehavior(op.getOpcode());
+			if (opBehavior instanceof SpecialOpBehavior) {
+				// TODO
+				return null;
+			}
+			Long exp = eval(unary.getExpression(), pp, domain);
+			if (exp == null) {
+				return exp;
 			}
 
-			Long exp = eval(unary.getExpression(), pp, domain);
 			byte[] bytes = arithmetic.unaryOp(op.getOpcode(), op.getOutput().getSize(),
 				op.getInput(0).getSize(), getValue(exp, op.getInput(0).getSize()));
 			return Utils.bytesToLong(bytes, op.getOutput().getSize(), isBigEndian);

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/analyses/PcodeInterval.java

@@ -6,10 +6,12 @@ package ghidra.lisa.pcode.analyses;
 import java.math.BigInteger;
 import java.util.Objects;
 
+import generic.stl.Pair;
 import ghidra.lisa.pcode.locations.PcodeLocation;
 import ghidra.lisa.pcode.statements.PcodeBinaryOperator;
 import ghidra.program.model.lang.RegisterValue;
 import ghidra.program.model.pcode.PcodeOp;
+import ghidra.program.model.pcode.Varnode;
 import ghidra.util.Msg;
 import it.unive.lisa.analysis.*;
 import it.unive.lisa.analysis.lattices.Satisfiability;
@@ -19,6 +21,7 @@ import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.value.*;
 import it.unive.lisa.symbolic.value.operator.binary.*;
 import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator;
+import it.unive.lisa.type.Untyped;
 import it.unive.lisa.util.numeric.IntInterval;
 import it.unive.lisa.util.numeric.MathNumber;
 import it.unive.lisa.util.representation.StringRepresentation;
@@ -47,6 +50,11 @@ public class PcodeInterval
 	 */
 	public static final PcodeInterval ZERO = new PcodeInterval(LongInterval.ZERO);
 
+	/**
+	 * The abstract true ({@code [1, 1]}) element.
+	 */
+	public static final PcodeInterval ONE = new PcodeInterval(LongInterval.ONE);
+
 	/**
 	 * The abstract top ({@code [-Inf, +Inf]}) element.
 	 */
@@ -62,10 +70,16 @@ public class PcodeInterval
 	 */
 	public final LongInterval interval;
 
+	public PcodeOp target;
+	public MathNumber bound;
+	public LongInterval intEq;
+	public LongInterval intNeq;
+	public boolean rightIsExpr;
+
 	/**
 	 * Builds the interval.
 	 * 
-	 * @param interval the underlying {@link IntInterval}
+	 * @param interval the underlying {@link LongInterval}
 	 */
 	public PcodeInterval(
 			LongInterval interval) {
@@ -84,18 +98,6 @@ public class PcodeInterval
 		this(new LongInterval(low, high));
 	}
 
-	/**
-	 * Builds the interval.
-	 * 
-	 * @param low  the lower bound
-	 * @param high the higher bound
-	 */
-	public PcodeInterval(
-			long low,
-			long high) {
-		this(new LongInterval(low, high));
-	}
-
 	/**
 	 * Builds the top interval.
 	 */
@@ -137,6 +139,40 @@ public class PcodeInterval
 		return representation().toString();
 	}
 
+	@Override
+	public PcodeInterval evalIdentifier(
+			Identifier id,
+			ValueEnvironment<PcodeInterval> environment,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		if (id.getCodeLocation() instanceof PcodeLocation ploc) {
+			Varnode vn = id2vn(id);
+			if (vn != null && vn.isConstant()) {
+				return evalNonNullConstant(new Constant(Untyped.INSTANCE, vn.getOffset(), ploc), pp,
+					oracle);
+			}
+		}
+		return environment.getState(id);
+	}
+
+	private Varnode id2vn(Identifier id) {
+		String name = id.getName();
+		PcodeLocation loc = (PcodeLocation) id.getCodeLocation();
+		Varnode output = loc.op.getOutput();
+		if (output != null) {
+			if (name.equals(output.getAddress().toString())) {
+				return output;
+			}
+		}
+		for (Varnode vn : loc.op.getInputs()) {
+			if (name.equals(vn.getAddress().toString())) {
+				return vn;
+			}
+		}
+		return null;
+	}
+
 	@Override
 	public PcodeInterval evalNonNullConstant(
 			Constant constant,
@@ -174,14 +210,18 @@ public class PcodeInterval
 		PcodeLocation ploc = (PcodeLocation) pp.getLocation();
 		PcodeOp op = ploc.op;
 		int opcode = op.getOpcode();
+		PcodeInterval result = arg;
 		if (opcode == PcodeOp.INT_NEGATE || opcode == PcodeOp.INT_2COMP ||
 			opcode == PcodeOp.FLOAT_NEG) {
-			if (arg.isTop()) {
-				return top();
-			}
-			return new PcodeInterval(arg.interval.mul(LongInterval.MINUS_ONE));
+			result = arg.isTop() ? top()
+					: new PcodeInterval(arg.interval.mul(LongInterval.MINUS_ONE));
 		}
-		return top();
+		if (opcode == PcodeOp.BOOL_NEGATE) {
+			result = arg.isTop() ? top()
+					: new PcodeInterval(arg.interval.complement());
+			result.target = ploc.op;
+		}
+		return result;
 	}
 
 	/**
@@ -205,8 +245,52 @@ public class PcodeInterval
 			PcodeInterval right,
 			ProgramPoint pp,
 			SemanticOracle oracle) {
-		PcodeLocation ploc = (PcodeLocation) pp.getLocation();
-		PcodeOp op = ploc.op;
+		if (!(pp.getLocation() instanceof PcodeLocation ploc)) {
+			return top();
+		}
+		Pair<PcodeInterval, PcodeInterval> pair = new Pair<>(left, right);
+
+		if (operator instanceof PcodeBinaryOperator) {
+			return evalPcodeBinaryExpression(pair, ploc.op);
+		}
+
+		try {
+			LongInterval interval1 = pair.first.interval;
+			LongInterval interval2 = pair.second.interval;
+			boolean exprOnRight = interval2.isFinite();
+			if (exprOnRight && interval1.isFinite()) {
+				exprOnRight = interval2.getLow().equals(interval2.getHigh());
+			}
+			PcodeInterval result = evalBooleanBinaryExpression(pair, operator);
+
+			result.target = ploc.op;
+			if (!(operator instanceof LogicalOperation)) {
+				Pair<PcodeInterval, PcodeInterval> basePair =
+					new Pair<>(exprOnRight ? top() : left, exprOnRight ? right : top());
+				PcodeInterval init = exprOnRight ? left : right;
+				PcodeInterval bounds = exprOnRight ? right : left;
+				PcodeInterval baseResult = evalBooleanBinaryExpression(basePair, operator);
+				PcodeInterval eq = baseResult.narrowing(init);
+				PcodeInterval neq = baseResult.complement().narrowing(init);
+				result.bound = bounds.interval.isFinite() ? bounds.interval.getLow() : null;
+				result.rightIsExpr = exprOnRight;
+				result.intEq = eq.interval;
+				result.intNeq = neq.interval;
+			}
+			return result;
+		}
+		catch (SemanticException e) {
+			Msg.error(this, e.getMessage());
+		}
+
+		return top();
+	}
+
+	protected PcodeInterval evalPcodeBinaryExpression(Pair<PcodeInterval, PcodeInterval> pair,
+			PcodeOp op) {
+
+		PcodeInterval left = pair.first;
+		PcodeInterval right = pair.second;
 		int opcode = op.getOpcode();
 		if (!(opcode == PcodeOp.INT_DIV) && !(opcode == PcodeOp.FLOAT_DIV) &&
 			(left.isTop() || right.isTop())) {
@@ -268,8 +352,8 @@ public class PcodeInterval
 				}
 
 				if (left.interval.getHigh().compareTo(MathNumber.ZERO) < 0) {
-					yield new PcodeInterval(
-						M.multiply(MathNumber.MINUS_ONE).add(MathNumber.ONE), MathNumber.ZERO);
+					yield new PcodeInterval(M.multiply(MathNumber.MINUS_ONE).add(MathNumber.ONE),
+						MathNumber.ZERO);
 				}
 				if (left.interval.getLow().compareTo(MathNumber.ZERO) > 0) {
 					yield new PcodeInterval(MathNumber.ZERO, M.subtract(MathNumber.ONE));
@@ -281,14 +365,74 @@ public class PcodeInterval
 		};
 	}
 
+	protected PcodeInterval evalBooleanBinaryExpression(Pair<PcodeInterval, PcodeInterval> pair,
+			BinaryOperator operator) throws SemanticException {
+		boolean exprOnRight = pair.second.interval.isFinite();
+
+		PcodeInterval starting = exprOnRight ? pair.first : pair.second;
+		PcodeInterval eval = exprOnRight ? pair.second : pair.first;
+		LongInterval lval = eval.interval;
+
+		boolean lowIsMinusInfinity = lval.lowIsMinusInfinity();
+		PcodeInterval low_inf = new PcodeInterval(lval.getLow(), MathNumber.PLUS_INFINITY);
+		PcodeInterval lowp1_inf =
+			new PcodeInterval(lval.getLow().add(MathNumber.ONE), MathNumber.PLUS_INFINITY);
+		PcodeInterval inf_high = new PcodeInterval(MathNumber.MINUS_INFINITY, lval.getHigh());
+		PcodeInterval inf_highm1 =
+			new PcodeInterval(MathNumber.MINUS_INFINITY, lval.getHigh().subtract(MathNumber.ONE));
+
+		PcodeInterval update = switch (operator) {
+			case ComparisonEq op -> new PcodeInterval(lval);
+			case ComparisonNe op -> new PcodeInterval(lval.complement());
+			case ComparisonLe op -> {
+				if (exprOnRight) {
+					yield starting.glb(inf_high);
+				}
+				yield lowIsMinusInfinity ? null : starting.glb(low_inf);
+			}
+			case ComparisonLt op -> {
+				if (exprOnRight) {
+					yield lowIsMinusInfinity ? eval : starting.glb(inf_highm1);
+				}
+				yield lowIsMinusInfinity ? null : starting.glb(lowp1_inf);
+			}
+			case ComparisonGe op -> {
+				if (exprOnRight) {
+					yield lowIsMinusInfinity ? null : starting.glb(low_inf);
+				}
+				yield starting.glb(inf_high);
+			}
+			case ComparisonGt op -> {
+				if (exprOnRight) {
+					yield lowIsMinusInfinity ? null : starting.glb(lowp1_inf);
+				}
+				yield lowIsMinusInfinity ? eval : starting.glb(inf_highm1);
+			}
+			case LogicalOr op -> {
+				MathNumber min = starting.interval.getLow().min(eval.interval.getLow());
+				MathNumber max = starting.interval.getHigh().max(eval.interval.getHigh());
+				yield new PcodeInterval(min, max);
+			}
+			default -> throw new AssertionError();
+		};
+
+		if (update == null || update.isBottom()) {
+			return new PcodeInterval(LongInterval.ZERO);
+		}
+		return update;
+	}
+
 	@Override
 	public PcodeInterval lubAux(
 			PcodeInterval other)
 			throws SemanticException {
 		MathNumber newLow = interval.getLow().min(other.interval.getLow());
 		MathNumber newHigh = interval.getHigh().max(other.interval.getHigh());
-		return newLow.isMinusInfinity() && newHigh.isPlusInfinity() ? top()
+		PcodeInterval res = newLow.isMinusInfinity() && newHigh.isPlusInfinity() ? top()
 				: new PcodeInterval(newLow, newHigh);
+		res.target = this.target;
+		res.bound = this.bound;
+		return res;
 	}
 
 	@Override
@@ -351,78 +495,6 @@ public class PcodeInterval
 			PcodeInterval right,
 			ProgramPoint pp,
 			SemanticOracle oracle) {
-		if (left.isTop() || right.isTop()) {
-			return Satisfiability.UNKNOWN;
-		}
-
-		if (!(operator instanceof PcodeBinaryOperator)) {
-			if (operator instanceof ComparisonEq) {
-				PcodeInterval glb = null;
-				try {
-					glb = left.glb(right);
-				}
-				catch (SemanticException e) {
-					return Satisfiability.UNKNOWN;
-				}
-
-				if (glb.isBottom()) {
-					return Satisfiability.NOT_SATISFIED;
-				}
-				else if (left.interval.isSingleton() && left.equals(right)) {
-					return Satisfiability.SATISFIED;
-				}
-				return Satisfiability.UNKNOWN;
-			}
-			else if (operator instanceof ComparisonLe) {
-				PcodeInterval glb = null;
-				try {
-					glb = left.glb(right);
-				}
-				catch (SemanticException e) {
-					return Satisfiability.UNKNOWN;
-				}
-
-				if (glb.isBottom()) {
-					return Satisfiability.fromBoolean(
-						left.interval.getHigh().compareTo(right.interval.getLow()) <= 0);
-				}
-				// we might have a singleton as glb if the two intervals share a
-				// bound
-				if (glb.interval.isSingleton() &&
-					left.interval.getHigh().compareTo(right.interval.getLow()) == 0) {
-					return Satisfiability.SATISFIED;
-				}
-				return Satisfiability.UNKNOWN;
-			}
-			else if (operator instanceof ComparisonLt) {
-				PcodeInterval glb = null;
-				try {
-					glb = left.glb(right);
-				}
-				catch (SemanticException e) {
-					return Satisfiability.UNKNOWN;
-				}
-
-				if (glb.isBottom()) {
-					return Satisfiability.fromBoolean(
-						left.interval.getHigh().compareTo(right.interval.getLow()) < 0);
-				}
-				return Satisfiability.UNKNOWN;
-			}
-			else if (operator instanceof ComparisonNe) {
-				PcodeInterval glb = null;
-				try {
-					glb = left.glb(right);
-				}
-				catch (SemanticException e) {
-					return Satisfiability.UNKNOWN;
-				}
-				if (glb.isBottom()) {
-					return Satisfiability.SATISFIED;
-				}
-				return Satisfiability.UNKNOWN;
-			}
-		}
 		return Satisfiability.UNKNOWN;
 	}
 
@@ -457,62 +529,52 @@ public class PcodeInterval
 			ProgramPoint dest,
 			SemanticOracle oracle)
 			throws SemanticException {
-		Identifier id;
-		PcodeInterval eval;
-		boolean rightIsExpr;
-		if (left instanceof Identifier) {
+
+		if (operator instanceof PcodeBinaryOperator) {
+			return environment;
+		}
+
+		Identifier id = null;
+		PcodeInterval eval = null;
+		PcodeInterval val = null;
+		boolean complement = false;
+		if (left instanceof Identifier leftId) {
+			id = leftId;
 			eval = eval(right, environment, src, oracle);
-			id = (Identifier) left;
-			rightIsExpr = true;
-		}
-		else if (right instanceof Identifier) {
-			eval = eval(left, environment, src, oracle);
-			id = (Identifier) right;
-			rightIsExpr = false;
-		}
-		else
-			return environment;
-
-		PcodeInterval starting = environment.getState(id);
-		if (eval.isBottom() || starting.isBottom()) {
-			return environment.bottom();
-		}
-
-		boolean lowIsMinusInfinity = eval.interval.lowIsMinusInfinity();
-		PcodeInterval low_inf = new PcodeInterval(eval.interval.getLow(), MathNumber.PLUS_INFINITY);
-		PcodeInterval lowp1_inf =
-			new PcodeInterval(eval.interval.getLow().add(MathNumber.ONE), MathNumber.PLUS_INFINITY);
-		PcodeInterval inf_high =
-			new PcodeInterval(MathNumber.MINUS_INFINITY, eval.interval.getHigh());
-		PcodeInterval inf_highm1 = new PcodeInterval(MathNumber.MINUS_INFINITY,
-			eval.interval.getHigh().subtract(MathNumber.ONE));
-
-		PcodeInterval update = null;
-		if (!(operator instanceof PcodeBinaryOperator)) {
-			if (operator instanceof ComparisonEq) {
-				update = eval;
+			val = environment.getState(leftId);
+			if (val.isBottom()) {
+				return environment.bottom();
 			}
-			else if (operator instanceof ComparisonLe) {
-				update = rightIsExpr ? starting.glb(inf_high)
-						: lowIsMinusInfinity ? null : starting.glb(low_inf);
-			}
-			else if (operator instanceof ComparisonLt) {
-				if (rightIsExpr) {
-					update = lowIsMinusInfinity ? eval : starting.glb(inf_highm1);
-				}
-				else {
-					update = lowIsMinusInfinity ? null : starting.glb(lowp1_inf);
-				}
+			if (operator instanceof ComparisonNe) {
+				eval = new PcodeInterval(eval.interval.complement());
+				complement = true;
 			}
 		}
-
-		if (update == null) {
+		if (id == null) {
 			return environment;
 		}
-		else if (update.isBottom()) {
-			return environment.bottom();
+
+		environment = updateImpliedConditions(environment, src, dest, val, complement);
+
+		return environment.putState(id, eval);
+	}
+
+	protected ValueEnvironment<PcodeInterval> updateImpliedConditions(
+			ValueEnvironment<PcodeInterval> environment,
+			ProgramPoint src, ProgramPoint dest, PcodeInterval val, boolean complement) {
+		if (val.target != null && val.bound != null) {
+			Varnode tgt = val.rightIsExpr ? val.target.getInput(0) : val.target.getInput(1);
+			Identifier vnId =
+				new Variable(Untyped.INSTANCE, tgt.getAddress().toString(), dest.getLocation());
+			PcodeInterval res = new PcodeInterval(complement ? val.intNeq : val.intEq);
+			return environment.putState(vnId, res);
 		}
-		return environment.putState(id, update);
+		return environment;
+	}
+
+	protected PcodeInterval complement() {
+		PcodeInterval comp = new PcodeInterval(this.interval.complement());
+		return comp;
 	}
 
 	@Override
@@ -538,9 +600,10 @@ public class PcodeInterval
 		if (rv != null) {
 			BigInteger val = rv.getUnsignedValue();
 			if (val != null) {
-				return new PcodeInterval(val.longValue(), val.longValue());
+				return new PcodeInterval(new LongInterval(val.longValue(), val.longValue()));
 			}
 		}
 		return top();
 	}
+
 }

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/analyses/PcodeIntervalLowX86.java

@@ -0,0 +1,215 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Map.Entry;
+
+import ghidra.program.model.address.Address;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.program.model.pcode.Varnode;
+import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
+import it.unive.lisa.program.cfg.ProgramPoint;
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.symbolic.value.Variable;
+import it.unive.lisa.type.Untyped;
+import it.unive.lisa.util.numeric.MathNumber;
+
+/**
+ * This class represents a pretty-extensive hack to enable low-pcode interval logic.  Low pcode differs from both source and high pcode
+ * in that the calculations made to determine a branch are not co-located with the branch.  The information needed for the "assume"
+ * processing (i.e. variables values assumed as a result fo the branch) is therefore not local.  The UpdateImpliedConditions is 
+ * essentially a table match against the default X86 implementation of flag-lookups representing a particular branch condition.
+ * 
+ * 		JBE	CF || ZF
+ * 		JB  CF  (unhandled)
+ * 		JL  SF==OF 
+ * 		JLE SF==OF || ZF
+ * 
+ */
+public class PcodeIntervalLowX86 extends PcodeInterval {
+
+	private class KeyPattern {
+
+		// NB: At some point, we may want to convert this to a more generic type
+		private String key;
+		private PcodeInterval kinterval;
+
+		public KeyPattern() {
+			this.key = "";
+		}
+
+		public KeyPattern(String key) {
+			this.key = key;
+		}
+
+		public void append(KeyPattern kp) {
+			this.key += kp.key;
+			if (this.kinterval == null) {
+				this.kinterval = kp.kinterval;
+			}
+		}
+
+		public void setKey(String key) {
+			this.key = key;
+		}
+
+		public void setInterval(PcodeInterval interval) {
+			if (this.kinterval == null) {
+				this.kinterval = interval;
+			}
+		}
+
+	}
+
+	@Override
+	protected ValueEnvironment<PcodeInterval> updateImpliedConditions(
+			ValueEnvironment<PcodeInterval> environment,
+			ProgramPoint src, ProgramPoint dest, PcodeInterval val, boolean complement) {
+		KeyPattern key = buildKey(indexEnv(environment), val.target);
+		LongInterval update = buildInterval(key, complement);
+		if (update == null) {
+			return environment;
+		}
+		PcodeOp tgt = key.kinterval.target;
+		Varnode vn = key.kinterval.rightIsExpr ? tgt.getInput(0) : tgt.getInput(1);
+		Identifier vnId =
+			new Variable(Untyped.INSTANCE, vn.getAddress().toString(), dest.getLocation());
+		PcodeInterval state = environment.getState(vnId);
+		if (vn.isUnique()) {
+			vnId = swapId(environment, dest, vnId, state);
+		}
+		PcodeInterval res = new PcodeInterval(update);
+		res = intersection(res, state);
+		return environment.putState(vnId, res);
+	}
+
+	private Map<String, PcodeInterval> indexEnv(ValueEnvironment<PcodeInterval> environment) {
+		Map<String, PcodeInterval> map = new HashMap<>();
+		for (Entry<Identifier, PcodeInterval> entry : environment) {
+			map.put(entry.getKey().getName(), entry.getValue());
+		}
+		return map;
+	}
+
+	private KeyPattern buildKey(Map<String, PcodeInterval> envMap, PcodeOp op) {
+
+		KeyPattern key = new KeyPattern();
+		for (Varnode in : op.getInputs()) {
+			String envKey = in.getAddress().toString();
+			if (envMap.containsKey(envKey)) {
+				PcodeInterval envVal = envMap.get(envKey);
+				if (envVal.target != null) {
+					key.append(buildKey(envMap, envVal.target));
+				}
+				else {
+					Varnode out = op.getOutput();
+					Address addr = out.getAddress();
+					key = new KeyPattern(key.key + "(" + Long.toHexString(addr.getOffset()) + ")");
+					if (isTerminal(op)) {
+						key.setInterval(envMap.get(addr.toString()));
+					}
+					return key;
+				}
+			}
+		}
+
+		key.setKey(op.getMnemonic() + key.key);
+		return key;
+	}
+
+	private boolean isTerminal(PcodeOp op) {
+		Varnode out = op.getOutput();
+		if (!out.isRegister()) {
+			return false;
+		}
+		Address addr = out.getAddress();
+		if ((addr.getOffset() & 0x200) == 0) {
+			return false;
+		}
+		return (op.getInput(0).isRegister() || op.getInput(1).isRegister());
+	}
+
+	private String key2op(KeyPattern kp, boolean complement) {
+		String ret = switch (kp.key) {
+			case "BOOL_OR(206)INT_NOTEQUAL(20b)(207)", "BOOL_OR(206)INT_NOTEQUAL(207)(20b)" -> "JLE";
+			case "BOOL_ANDBOOL_NEGATE(206)INT_EQUAL(20b)(207)", "BOOL_ANDBOOL_NEGATE(206)INT_EQUAL(207)(20b)" -> "JG";
+			case "INT_NOTEQUAL(20b)(207)", "INT_NOTEQUAL(207)(20b)" -> "JL";
+			case "INT_EQUAL(20b)(207)", "INT_EQUAL(207)(20b)" -> "JGE";
+			case "BOOL_OR(200)(206)", "BOOL_OR(206)(200)" -> "JBE";
+			case "BOOL_NEGATEBOOL_OR(200)(206)", "BOOL_NEGATEBOOL_OR(206)(200)" -> "JA";
+			case "(200)" -> "JB";
+			case "BOOL_NEGATE(200)" -> "JAE";
+			default -> null;
+		};
+		if (ret == null) {
+			return ret;
+		}
+		if (kp.kinterval != null && !kp.kinterval.rightIsExpr) {
+			ret = ret.contains("A") ? ret.replace("A", "B") : ret.replace("B", "A");
+			ret = ret.contains("G") ? ret.replace("G", "L") : ret.replace("L", "G");
+		}
+		if (complement) {
+			ret = switch (ret) {
+				case "JLE" -> "JG";
+				case "JG" -> "JLE";
+				case "JL" -> "JGE";
+				case "JGE" -> "JL";
+				case "JA" -> "JBE";
+				case "JBE" -> "JA";
+				case "JB" -> "JAE";
+				case "JAE" -> "JB";
+				default -> null;
+			};
+		}
+		return ret;
+	}
+
+	private LongInterval buildInterval(KeyPattern key, boolean complement) {
+		String comparison = key2op(key, complement);
+		if (key.kinterval == null) {
+			//Msg.error(this, "Null interval for key: " + key.key);
+			return null;
+		}
+		MathNumber bnd = key.kinterval.bound;
+		return switch (comparison) {
+			case "JG" -> new LongInterval(bnd.add(MathNumber.ONE), MathNumber.PLUS_INFINITY);
+			case "JLE" -> new LongInterval(MathNumber.MINUS_INFINITY, bnd);
+			case "JGE" -> new LongInterval(bnd, MathNumber.PLUS_INFINITY);
+			case "JL" -> new LongInterval(MathNumber.MINUS_INFINITY,
+				bnd.subtract(MathNumber.ONE));
+			case "JA" -> new LongInterval(bnd.add(MathNumber.ONE), MathNumber.PLUS_INFINITY);
+			case "JBE" -> new LongInterval(MathNumber.MINUS_INFINITY, bnd);
+			case "JAE" -> new LongInterval(bnd, MathNumber.PLUS_INFINITY);
+			case "JB" -> new LongInterval(MathNumber.MINUS_INFINITY,
+				bnd.subtract(MathNumber.ONE));
+			default -> null;
+		};
+	}
+
+	private Identifier swapId(ValueEnvironment<PcodeInterval> environment, ProgramPoint dest,
+			Identifier vnId, PcodeInterval state) {
+		for (Entry<Identifier, PcodeInterval> n : environment) {
+			PcodeInterval v = n.getValue();
+			if (v.interval.equals(state.interval) && !n.getKey().equals(vnId) &&
+				n.getKey().toString().contains("register")) {
+				vnId = new Variable(Untyped.INSTANCE, n.getKey().getName(),
+					dest.getLocation());
+				break;
+			}
+		}
+		return vnId;
+	}
+
+	private PcodeInterval intersection(PcodeInterval a, PcodeInterval b) {
+		if (a.interval.intersects(b.interval)) {
+			MathNumber min = a.interval.getHigh().min(b.interval.getHigh());
+			MathNumber max = a.interval.getLow().max(b.interval.getLow());
+			return new PcodeInterval(min, max);
+		}
+		return bottom();
+	}
+
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/analyses/PcodeNonRedundantPowersetOfInterval.java

@@ -29,13 +29,13 @@ import it.unive.lisa.util.numeric.MathNumber;
  */
 public class PcodeNonRedundantPowersetOfInterval
 		extends
-		NonRedundantPowersetOfBaseNonRelationalValueDomain<PcodeNonRedundantPowersetOfInterval, Interval> {
+		NonRedundantPowersetOfBaseNonRelationalValueDomain<PcodeNonRedundantPowersetOfInterval, PcodeInterval> {
 
 	/**
 	 * Constructs an empty non redundant set of intervals.
 	 */
 	public PcodeNonRedundantPowersetOfInterval() {
-		super(new TreeSet<>(), Interval.BOTTOM);
+		super(new TreeSet<>(), PcodeInterval.BOTTOM);
 	}
 
 	/**
@@ -44,8 +44,8 @@ public class PcodeNonRedundantPowersetOfInterval
 	 * @param elements the set of intervals
 	 */
 	public PcodeNonRedundantPowersetOfInterval(
-			SortedSet<Interval> elements) {
-		super(elements, Interval.BOTTOM);
+			SortedSet<PcodeInterval> elements) {
+		super(elements, PcodeInterval.BOTTOM);
 	}
 
 	/**
@@ -62,19 +62,19 @@ public class PcodeNonRedundantPowersetOfInterval
 	 * </p>
 	 * s'<sub>1</sub> can be chosen randomly but in this case is chosen to be
 	 * the closest interval to s<sub>2</sub> (closest based on
-	 * {@link #middlePoint(Interval) middle point}).
+	 * {@link #middlePoint(PcodeInterval) middle point}).
 	 */
 	@Override
 	protected PcodeNonRedundantPowersetOfInterval EgliMilnerConnector(
 			PcodeNonRedundantPowersetOfInterval other)
 			throws SemanticException {
-		SortedSet<Interval> newElementsSet = new TreeSet<>();
-		SortedSet<Interval> notCoverSet = new TreeSet<>();
+		SortedSet<PcodeInterval> newElementsSet = new TreeSet<>();
+		SortedSet<PcodeInterval> notCoverSet = new TreeSet<>();
 
 		// first side of the union
-		for (Interval s2 : other.elementsSet) {
+		for (PcodeInterval s2 : other.elementsSet) {
 			boolean existsLower = false;
-			for (Interval s1 : elementsSet) {
+			for (PcodeInterval s1 : elementsSet) {
 				if (s1.lessOrEqual(s2)) {
 					existsLower = true;
 					break;
@@ -89,12 +89,12 @@ public class PcodeNonRedundantPowersetOfInterval
 		}
 
 		// second side of the union
-		for (Interval s2 : notCoverSet) {
+		for (PcodeInterval s2 : notCoverSet) {
 			MathNumber middlePoint = middlePoint(s2);
 			MathNumber closestValue = middlePoint;
 			MathNumber closestDiff = closestValue.subtract(middlePoint).abs();
-			Interval closest = Interval.TOP;
-			for (Interval s1 : elementsSet) {
+			PcodeInterval closest = PcodeInterval.TOP;
+			for (PcodeInterval s1 : elementsSet) {
 				if (closestValue.compareTo(middlePoint) == 0) {
 					closest = s1;
 					closestValue = middlePoint(s1);
@@ -127,7 +127,7 @@ public class PcodeNonRedundantPowersetOfInterval
 	 * @return the middle point of the interval
 	 */
 	protected MathNumber middlePoint(
-			Interval interval) {
+			PcodeInterval interval) {
 		if (interval.interval.isFinite()) {
 			return interval.interval.getLow()
 					.add(interval.interval.getHigh())
@@ -175,18 +175,19 @@ public class PcodeNonRedundantPowersetOfInterval
 			return environment.bottom();
 		}
 
-		SortedSet<Interval> newSet = new TreeSet<>();
+		SortedSet<PcodeInterval> newSet = new TreeSet<>();
 
-		for (Interval startingInterval : starting.elementsSet)
-			for (Interval interval : eval.elementsSet) {
+		for (PcodeInterval startingInterval : starting.elementsSet)
+			for (PcodeInterval interval : eval.elementsSet) {
 				boolean lowIsMinusInfinity = interval.interval.lowIsMinusInfinity();
-				Interval lowInf =
-					new Interval(interval.interval.getLow(), MathNumber.PLUS_INFINITY);
-				Interval lowp1Inf = new Interval(interval.interval.getLow().add(MathNumber.ONE),
+				PcodeInterval lowInf =
+					new PcodeInterval(interval.interval.getLow(), MathNumber.PLUS_INFINITY);
+				PcodeInterval lowp1Inf =
+					new PcodeInterval(interval.interval.getLow().add(MathNumber.ONE),
 					MathNumber.PLUS_INFINITY);
-				Interval infHigh =
-					new Interval(MathNumber.MINUS_INFINITY, interval.interval.getHigh());
-				Interval infHighm1 = new Interval(MathNumber.MINUS_INFINITY,
+				PcodeInterval infHigh =
+					new PcodeInterval(MathNumber.MINUS_INFINITY, interval.interval.getHigh());
+				PcodeInterval infHighm1 = new PcodeInterval(MathNumber.MINUS_INFINITY,
 					interval.interval.getHigh().subtract(MathNumber.ONE));
 
 				if (!(operator instanceof PcodeBinaryOperator)) {
@@ -234,7 +235,7 @@ public class PcodeNonRedundantPowersetOfInterval
 
 	@Override
 	protected PcodeNonRedundantPowersetOfInterval mk(
-			SortedSet<Interval> elements) {
+			SortedSet<PcodeInterval> elements) {
 		return new PcodeNonRedundantPowersetOfInterval(elements);
 	}
 

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/analyses/PcodePentagon.java

@@ -45,12 +45,12 @@ public class PcodePentagon implements ValueDomain<PcodePentagon>, BaseLattice<Pc
 	/**
 	 * The interval environment.
 	 */
-	private final ValueEnvironment<PcodeInterval> intervals;
+	protected ValueEnvironment<PcodeInterval> intervals;
 
 	/**
 	 * The upper bounds environment.
 	 */
-	private final ValueEnvironment<PcodeUpperBounds> upperBounds;
+	protected ValueEnvironment<PcodeUpperBounds> upperBounds;
 
 	/**
 	 * Builds the PcodePentagons.

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/analyses/PcodePentagonLowX86.java

@@ -0,0 +1,38 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
+import it.unive.lisa.analysis.value.ValueDomain;
+
+/**
+ * /** The pentagons abstract domain, a weakly relational numeric abstract
+ * domain. This abstract domain captures properties of the form of x \in [a, b]
+ * ∧ x < y. It is more precise than the well known interval domain, but
+ * it is less precise than the octagon domain. It is implemented as a
+ * {@link ValueDomain}.
+ * 
+ * <p>
+ * Modified to handle pcode from original source written by:
+ * <p>
+ * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
+ * @author <a href="mailto:vincenzo.arceri@unipr.it">Vincenzo Arceri</a>
+ * 
+ * <p>
+ * @see <a href=
+ *          "https://www.sciencedirect.com/science/article/pii/S0167642309000719?ref=cra_js_challenge&fr=RR-1">Pentagons:
+ *          A weakly relational abstract domain for the efficient validation of
+ *          array accesses</a>
+ */
+public class PcodePentagonLowX86 extends PcodePentagon {
+
+	/**
+	 * Builds the PcodePentagons.
+	 */
+	public PcodePentagonLowX86() {
+		this.intervals = new ValueEnvironment<>(new PcodeIntervalLowX86()).top();
+		this.upperBounds = new ValueEnvironment<>(new PcodeUpperBounds(true)).top();
+	}
+
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/ConditionContext.java

@@ -21,11 +21,11 @@ public class ConditionContext extends PcodeContext {
 
 	public ConditionContext(PcodeOp op) {
 		super(op);
+		assert (op.getOpcode() == PcodeOp.CBRANCH);
 	}
 
 	public VarnodeContext expression() {
-		// opcode should be CBRANCH
-		assert (op.getInputs().length < 2);
+		assert (op.getInputs().length <= 2);
 		return new VarnodeContext(op.getInput(1));
 	}
 

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/HighInstructionContext.java

@@ -0,0 +1,32 @@
+/* ###
+ * 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.lisa.pcode.contexts;
+
+import java.util.ArrayList;
+
+public class HighInstructionContext extends InstructionContext {
+
+	public HighInstructionContext(HighStatementContext ctx) {
+		ops = new ArrayList<>();
+		ops.add(ctx);
+	}
+
+	@Override
+	public HighInstructionContext next() {
+		return null;  // UNUSED
+	}
+
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/HighStatementContext.java

@@ -0,0 +1,73 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.pcode.contexts;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import ghidra.program.model.address.AddressFactory;
+import ghidra.program.model.pcode.HighFunction;
+import ghidra.program.model.pcode.PcodeOp;
+
+public class HighStatementContext extends StatementContext {
+
+	// High pcode-only
+	private HighFunction hfunc;
+	private HighStatementContext prev;
+	private HighStatementContext succ;
+	private List<StatementContext> branches = new ArrayList<>();
+	
+
+	public HighStatementContext(HighFunction hfunc, PcodeOp op) {
+		super(op);
+		this.hfunc = hfunc; 
+	}
+
+	@Override
+	public String toString() {
+		return op.getSeqnum() + ": " + op;
+	}
+
+	@Override
+	public AddressFactory getAddressFactory() {
+		return hfunc.getAddressFactory();
+	}
+
+	public HighStatementContext getPrev() {
+		 return prev;
+	}
+	
+	public void setPrev(HighStatementContext ctx) {
+		this.prev = ctx;
+	}
+
+	public HighStatementContext getNext() {
+		 return succ;
+	}
+	
+	public void setNext(HighStatementContext ctx) {
+		this.succ = ctx;
+	}
+
+	public List<StatementContext> getBranches() {
+		return branches;
+	}
+
+	public void addBranch(HighStatementContext ctx) {
+		branches.add(ctx);
+	}
+
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/HighUnitContext.java

@@ -0,0 +1,118 @@
+/* ###
+ * 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.lisa.pcode.contexts;
+
+import java.util.*;
+
+import ghidra.lisa.pcode.PcodeFrontend;
+import ghidra.program.model.address.Address;
+import ghidra.program.model.listing.Function;
+import ghidra.program.model.listing.Listing;
+import ghidra.program.model.pcode.*;
+import it.unive.lisa.program.Program;
+
+public class HighUnitContext extends UnitContext {
+
+	// High pcode-only
+	private HighFunction hfunc;
+	Map<SequenceNumber, HighStatementContext> map = new HashMap<>();
+
+	public HighUnitContext(PcodeFrontend frontend, Program program, Function f, HighFunction hfunc, Address entry) {
+		super(frontend, program, f, entry);
+		this.hfunc = hfunc;
+	}
+
+	@Override
+	public InstructionContext entry() {
+		return initEdges();
+	}
+
+	@Override
+	public List<StatementContext> branch(StatementContext ctx, Listing listing) {
+		if (ctx instanceof HighStatementContext hctx) {
+			return hctx.getBranches();
+		}
+		return new ArrayList<StatementContext>();
+	}
+
+	@Override
+	public HighStatementContext next(StatementContext ctx, Listing listing) {
+		if (ctx instanceof HighStatementContext hctx) {
+			return hctx.getNext();
+		}
+		return null;
+	}
+
+	public void setBranches(PcodeBlockBasic bb) {
+		PcodeOp lastOp = bb.getLastOp();
+		HighStatementContext ctx = map.get(lastOp.getSeqnum());
+		for (int i = 0; i < bb.getOutSize(); i++) {
+			if (bb.getOut(i) instanceof PcodeBlockBasic basic) {
+				PcodeOp op = basic.getFirstOp();
+				if (lastOp.getOpcode() == PcodeOp.CBRANCH) {
+					if (basic.equals(bb.getFalseOut())) {
+						ctx.setNext(map.get(op.getSeqnum()));
+					}
+					else {
+						ctx.addBranch(map.get(op.getSeqnum()));
+					}
+				}
+				else if (lastOp.getOpcode() == PcodeOp.BRANCH ||
+					lastOp.getOpcode() == PcodeOp.BRANCHIND) {
+					ctx.addBranch(map.get(op.getSeqnum()));
+				}
+				else {
+					ctx.setNext(map.get(op.getSeqnum()));
+				}
+			}
+		}
+	}
+
+	private InstructionContext initEdges() {
+		Iterator<PcodeOpAST> pcodeOps = hfunc.getPcodeOps();
+		while (pcodeOps.hasNext()) {
+			PcodeOpAST next = pcodeOps.next();
+			HighStatementContext ctx = new HighStatementContext(hfunc, next);
+			map.put(next.getSeqnum(), ctx);
+		}
+		ArrayList<PcodeBlockBasic> basicBlocks = hfunc.getBasicBlocks();
+		HighStatementContext first = null;
+		for (PcodeBlockBasic b : basicBlocks) {
+			Iterator<PcodeOp> iterator = b.getIterator();
+			PcodeOp prev = null;
+			while (iterator.hasNext()) {
+				PcodeOp next = iterator.next();
+				HighStatementContext n = map.get(next.getSeqnum());
+				if (prev != null) {
+					HighStatementContext p = map.get(prev.getSeqnum());
+					if (p != null && n != null) {
+						p.setNext(n);
+						n.setPrev(p);
+					}
+				}
+				else if (first == null) {
+					first = n;			
+				}
+				prev = next;
+			}
+		}
+		for (PcodeBlockBasic b : basicBlocks) {
+			setBranches(b);
+		}
+		return new HighInstructionContext(first);
+	}
+
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/InstructionContext.java

@@ -25,10 +25,10 @@ import it.unive.lisa.program.cfg.CodeLocation;
 
 public class InstructionContext {
 
-	private Function function;
-	private Instruction inst;
-	private List<StatementContext> ops;
-	private InstLocation loc;
+	protected Function function;
+	protected Instruction inst;
+	protected List<StatementContext> ops;
+	protected InstLocation loc;
 
 	public InstructionContext(Function function, Instruction inst) {
 		this.function = function;
@@ -41,6 +41,10 @@ public class InstructionContext {
 		loc = new InstLocation(function, inst.getAddress());
 	}
 
+	public InstructionContext() {
+		// For HighInstructionContext
+	}
+
 	public Collection<StatementContext> getPcodeOps() {
 		return ops;
 	}
@@ -49,11 +53,10 @@ public class InstructionContext {
 		return ops.get(i);
 	}
 
-	public Instruction getInstruction() {
-		return inst;
-	}
-
 	public InstructionContext next() {
+		if (inst == null) {
+			return null;
+		}
 		Listing listing = inst.getProgram().getListing();
 		Address nextAddress = inst.getAddress().add(inst.getLength());
 		Instruction next = listing.getInstructionAt(nextAddress);

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/MemLocContext.java

@@ -24,8 +24,11 @@ public class MemLocContext extends VarnodeContext {
 
 	public MemLocContext(StatementContext ctx) {
 		super(ctx.getOp().getInput(1));
-		AddressFactory addressFactory = ctx.inst.getProgram().getAddressFactory();
-		space = addressFactory.getAddressSpace((int) ctx.getOp().getInput(0).getOffset());
+		AddressFactory addressFactory = ctx.getAddressFactory();
+		space = addressFactory.getAddressSpace((int)ctx.getOp().getInput(0).getOffset());
+		if (space == null) {
+			space = addressFactory.getDefaultAddressSpace();
+		}
 	}
 
 	@Override

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/PcodeContext.java

@@ -40,10 +40,7 @@ public class PcodeContext {
 	}
 
 	public VarnodeContext basicExpr() {
-		if (op.getNumInputs() == 1) {
-			return new VarnodeContext(op.getInput(0));
-		}
-		return null;
+		return new VarnodeContext(op.getInput(0));
 	}
 
 	public int opcode() {

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/StatementContext.java

@@ -15,29 +15,22 @@
  */
 package ghidra.lisa.pcode.contexts;
 
-import java.util.ArrayList;
-import java.util.List;
-
-import ghidra.program.model.address.Address;
+import ghidra.program.model.address.AddressFactory;
 import ghidra.program.model.listing.Instruction;
-import ghidra.program.model.listing.Listing;
 import ghidra.program.model.pcode.PcodeOp;
-import ghidra.program.model.pcode.Varnode;
-import ghidra.program.model.symbol.*;
 
 public class StatementContext extends PcodeContext {
 
 	public StatementContext otherwise;
 	public StatementContext then;
 
-	private int opcode;
-	public Instruction inst;
+	protected int opcode;
+	protected Instruction inst;
 	public VarDefContext left;
 	public PcodeContext right;
-
-	public StatementContext(Instruction inst, PcodeOp op) {
+	
+	protected StatementContext(PcodeOp op) {
 		super(op);
-		this.inst = inst;
 		if (op != null) {
 			this.opcode = op.getOpcode();
 			if (op.getOutput() != null) {
@@ -50,6 +43,11 @@ public class StatementContext extends PcodeContext {
 		}
 	}
 
+	public StatementContext(Instruction inst, PcodeOp op) {
+		this(op);
+		this.inst = inst; 
+	}
+
 	public VarDefContext target() {
 		return left;
 	}
@@ -74,68 +72,13 @@ public class StatementContext extends PcodeContext {
 		return opcode == PcodeOp.CBRANCH;
 	}
 
-	public List<StatementContext> branch(Listing listing, UnitContext currentUnit) {
-		List<StatementContext> list = new ArrayList<>();
-		if (opcode == PcodeOp.BRANCH || opcode == PcodeOp.CBRANCH) {
-			Varnode vn = op.getInput(0);
-			if (vn.getAddress().isConstantAddress()) {
-				int order = op.getSeqnum().getTime();
-				order += vn.getOffset();
-				list.add(new StatementContext(inst, inst.getPcode()[order]));
-			}
-			else {
-				Instruction next =
-					listing.getInstructionAt(vn.getAddress().getNewAddress(vn.getOffset()));
-				if (next == null || next.getPcode().length == 0) {
-					return list;
-				}
-				list.add(new StatementContext(next, next.getPcode()[0]));
-			}
-		}
-		if (opcode == PcodeOp.BRANCHIND) {
-			ReferenceManager referenceManager =
-				currentUnit.function().getProgram().getReferenceManager();
-			Reference[] refs = referenceManager.getReferencesFrom(inst.getAddress());
-			for (Reference ref : refs) {
-				Address fromAddress = ref.getToAddress();
-				Instruction next = listing.getInstructionAt(fromAddress);
-				if (next == null || next.getPcode().length == 0) {
-					return list;
-				}
-				list.add(new StatementContext(next, next.getPcode()[0]));
-			}
-		}
-		return list;
-	}
-
-	public StatementContext next(Listing listing) {
-		PcodeOp[] pcode = inst.getPcode();
-		if (op != null) {
-			int order = op.getSeqnum().getTime();
-			if (order + 1 < pcode.length) {
-				return new StatementContext(inst, inst.getPcode()[order + 1]);
-			}
-		}
-		Instruction next = listing.getInstructionAt(inst.getAddress().add(inst.getLength()));
-		while (next != null && next.getPcode().length == 0) {
-			next = listing.getInstructionAt(next.getAddress().add(next.getLength()));
-		}
-		if (next == null) {
-			return null;
-		}
-		return new StatementContext(next, next.getPcode()[0]);
-	}
-
-	public PcodeContext ret() {
-		if (opcode == PcodeOp.RETURN) {
-			return new PcodeContext(op);
-		}
-		return null;
-	}
-
 	@Override
 	public String toString() {
 		return inst.getAddress() + ": " + inst + ":" + op;
 	}
 
+	public AddressFactory getAddressFactory() {
+		return inst.getProgram().getAddressFactory();
+	}
+
 }

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/TernaryExprContext.java

@@ -0,0 +1,49 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.pcode.contexts;
+
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.program.model.pcode.PcodeOp;
+import it.unive.lisa.program.cfg.CodeLocation;
+
+public class TernaryExprContext {
+
+	public PcodeOp op;
+	public VarnodeContext left;
+	public VarnodeContext middle;
+	public VarnodeContext right;
+
+	public TernaryExprContext(PcodeContext ctx) {
+		this.op = ctx.op;
+		left = new VarnodeContext(op.getInput(0));
+		middle = new VarnodeContext(op.getInput(1));
+		right = new VarnodeContext(op.getInput(2));
+	}
+
+	public int opcode() {
+		return op.getOpcode();
+	}
+
+
+	public CodeLocation location() {
+		return new PcodeLocation(op);
+	}
+
+	public String mnemonic() {
+		return op.getMnemonic();
+	}
+
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/UnitContext.java

@@ -15,10 +15,17 @@
  */
 package ghidra.lisa.pcode.contexts;
 
+import java.util.ArrayList;
+import java.util.List;
+
 import ghidra.lisa.pcode.PcodeFrontend;
 import ghidra.lisa.pcode.locations.InstLocation;
 import ghidra.program.model.address.Address;
 import ghidra.program.model.listing.*;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.program.model.pcode.Varnode;
+import ghidra.program.model.symbol.Reference;
+import ghidra.program.model.symbol.ReferenceManager;
 import it.unive.lisa.program.CodeUnit;
 import it.unive.lisa.program.Program;
 import it.unive.lisa.program.SyntheticLocation;
@@ -26,18 +33,11 @@ import it.unive.lisa.program.cfg.CodeLocation;
 
 public class UnitContext {
 
-	private PcodeFrontend frontend;
-	private Function function;
-	private CodeUnit unit;
-	private Address start;
-
-	public UnitContext(PcodeFrontend frontend, Program program, Function f) {
-		this.frontend = frontend;
-		this.function = f;
-		unit = new CodeUnit(SyntheticLocation.INSTANCE, program, f.getName());
-		start = function.getEntryPoint();
-	}
-
+	protected PcodeFrontend frontend;
+	protected Function function;
+	protected CodeUnit unit;
+	protected Address start;
+	
 	public UnitContext(PcodeFrontend frontend, Program program, Function f, Address entry) {
 		this.frontend = frontend;
 		this.function = f;
@@ -82,6 +82,56 @@ public class UnitContext {
 		return inst == null ? null : new InstructionContext(function, inst);
 	}
 
+	public List<StatementContext> branch(StatementContext ctx, Listing listing) {
+		List<StatementContext> list = new ArrayList<>();	
+		if (ctx.opcode == PcodeOp.BRANCH || ctx.opcode == PcodeOp.CBRANCH) {
+			Varnode vn = ctx.op.getInput(0);
+			if (vn.getAddress().isConstantAddress()) {
+				int order = ctx.op.getSeqnum().getTime();
+				order += vn.getOffset();
+				list.add(new StatementContext(ctx.inst.getPcode()[order]));
+			}
+			else {
+				Instruction next = listing.getInstructionAt(vn.getAddress().getNewAddress(vn.getOffset()));
+				if (next == null || next.getPcode().length == 0) {
+					return list;
+				}
+				list.add(new StatementContext(next, next.getPcode()[0]));
+			}
+		}
+		if (ctx.opcode == PcodeOp.BRANCHIND) {
+			ReferenceManager referenceManager = function().getProgram().getReferenceManager();
+			Reference[] refs = referenceManager.getReferencesFrom(ctx.inst.getAddress());
+			for (Reference ref : refs) {
+				Address fromAddress = ref.getToAddress();
+				Instruction next = listing.getInstructionAt(fromAddress);
+				if (next == null || next.getPcode().length == 0) {
+					return list;
+				}
+				list.add(new StatementContext(next, next.getPcode()[0]));
+			}
+		}
+		return list;
+	}
+
+	public StatementContext next(StatementContext ctx, Listing listing) {
+		PcodeOp[] pcode = ctx.inst.getPcode();
+		if (ctx.op != null) {
+			int order = ctx.op.getSeqnum().getTime();
+			if (order+1 < pcode.length) {
+				return new StatementContext(ctx.inst, ctx.inst.getPcode()[order+1]);
+			}
+		}
+		Instruction next = listing.getInstructionAt(ctx.inst.getAddress().add(ctx.inst.getLength()));
+		while (next != null && next.getPcode().length == 0) {
+			next = listing.getInstructionAt(next.getAddress().add(next.getLength()));
+		}
+		if (next == null) {
+			return null;
+		}
+		return new StatementContext(next, next.getPcode()[0]);
+	}
+
 	public boolean contains(Address target) {
 		return function.getBody().contains(target);
 	}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/VarargsExprContext.java

@@ -0,0 +1,48 @@
+/* ###
+ * 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.lisa.pcode.contexts;
+
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.program.model.pcode.PcodeOp;
+import it.unive.lisa.program.cfg.CodeLocation;
+
+public class VarargsExprContext {
+
+	public PcodeOp op;
+	public VarnodeContext[] varargs;
+
+	public VarargsExprContext(PcodeContext ctx) {
+		this.op = ctx.op;
+		varargs = new VarnodeContext[op.getNumInputs()];
+		for (int i = 0; i < op.getNumInputs(); i++) {
+			varargs[i] = new VarnodeContext(op.getInput(i));
+		}
+	}
+
+	public int opcode() {
+		return op.getOpcode();
+	}
+
+
+	public CodeLocation location() {
+		return new PcodeLocation(op);
+	}
+
+	public String mnemonic() {
+		return op.getMnemonic();
+	}
+
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/expressions/PcodeBinaryExpression.java

@@ -44,8 +44,9 @@ public class PcodeBinaryExpression extends it.unive.lisa.program.cfg.statement.B
 			case PcodeOp.BOOL_OR -> LogicalOr.INSTANCE;
 			case PcodeOp.INT_EQUAL, PcodeOp.FLOAT_EQUAL -> ComparisonEq.INSTANCE;
 			case PcodeOp.INT_NOTEQUAL, PcodeOp.FLOAT_NOTEQUAL -> ComparisonNe.INSTANCE;
-			case PcodeOp.INT_LESSEQUAL, PcodeOp.FLOAT_LESSEQUAL -> ComparisonLe.INSTANCE;
-			case PcodeOp.INT_LESS, PcodeOp.FLOAT_LESS -> ComparisonLt.INSTANCE;
+			case PcodeOp.INT_LESSEQUAL, PcodeOp.INT_SLESSEQUAL, PcodeOp.FLOAT_LESSEQUAL -> ComparisonLe.INSTANCE;
+			// NB: Some chance we're going to get burned by including SBORROW here
+			case PcodeOp.INT_LESS, PcodeOp.INT_SLESS, PcodeOp.INT_SBORROW, PcodeOp.FLOAT_LESS -> ComparisonLt.INSTANCE;
 			default -> new PcodeBinaryOperator(ctx.op);
 		};
 	}
@@ -70,8 +71,12 @@ public class PcodeBinaryExpression extends it.unive.lisa.program.cfg.statement.B
 				getStaticType(),
 				left,
 				right,
-				operator,
+				getOperator(),
 				getLocation()),
 			this);
 	}
+
+	public BinaryOperator getOperator() {
+		return operator;
+	}
 }

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/expressions/PcodeCallExpression.java

@@ -20,10 +20,8 @@ import java.util.Set;
 
 import ghidra.lisa.pcode.contexts.CallContext;
 import ghidra.lisa.pcode.locations.PcodeLocation;
-import ghidra.program.model.address.Address;
 import ghidra.program.model.lang.PrototypeModel;
 import ghidra.program.model.listing.Function;
-import ghidra.program.model.listing.ProgramContext;
 import ghidra.program.model.pcode.Varnode;
 import it.unive.lisa.analysis.*;
 import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
@@ -77,8 +75,6 @@ public class PcodeCallExpression extends UnresolvedCall {
 		if (unaffected.isEmpty()) {
 			return entryState;
 		}
-		ProgramContext programContext = function.getProgram().getProgramContext();
-		Address entryPoint = function.getEntryPoint();
 		if (entryState.getState() instanceof SimpleAbstractState sas) {
 			ValueDomain<?> vDomain = sas.getValueState();
 			if (vDomain instanceof ValueEnvironment vEnv) {
@@ -102,25 +98,6 @@ public class PcodeCallExpression extends UnresolvedCall {
 						}
 					}
 				}
-//				for (Register r : programContext.getRegisters()) {
-//					RegisterValue rv = programContext.getRegisterValue(r, entryPoint);
-//					if (rv != null && rv.hasAnyValue()) {
-//						Variable v = new Variable(Untyped.INSTANCE,
-//							r.getAddress().toString(), new InstLocation(entryPoint));
-//						if (vEnv.lattice instanceof PcodeNonRelationalValueDomain pcodeDomain) {
-//							PcodeNonRelationalValueDomain<?> value = pcodeDomain.getValue(rv);
-//							if (value != null) {
-//								vEnv.function.put(v, value);
-//							}
-//						}
-//						if (vEnv.lattice instanceof PcodeDataflowConstantPropagation pcodeDomain) {
-//							PcodeDataflowConstantPropagation value = pcodeDomain.getValue(v, rv);
-//							if (value != null) {
-//								vEnv.function.put(v, value);
-//							}
-//						}
-//					}
-//				}
 			}
 		}
 		return entryState;

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/expressions/PcodeTernaryExpression.java

@@ -0,0 +1,72 @@
+/* ###
+ * 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.lisa.pcode.expressions;
+
+import ghidra.lisa.pcode.contexts.TernaryExprContext;
+import ghidra.lisa.pcode.statements.PcodeTernaryOperator;
+import it.unive.lisa.analysis.*;
+import it.unive.lisa.interprocedural.InterproceduralAnalysis;
+import it.unive.lisa.program.cfg.CFG;
+import it.unive.lisa.program.cfg.statement.Expression;
+import it.unive.lisa.program.cfg.statement.Statement;
+import it.unive.lisa.symbolic.SymbolicExpression;
+import it.unive.lisa.symbolic.value.TernaryExpression;
+import it.unive.lisa.symbolic.value.operator.ternary.TernaryOperator;
+
+public class PcodeTernaryExpression extends it.unive.lisa.program.cfg.statement.TernaryExpression {
+
+	private TernaryOperator operator;
+
+	public PcodeTernaryExpression(
+			CFG cfg,
+			TernaryExprContext ctx,
+			Expression left,
+			Expression middle,
+			Expression right) {
+		super(cfg, ctx.location(), ctx.mnemonic(), cfg.getDescriptor().getUnit().getProgram().getTypes().getIntegerType(), left, middle, right);
+
+		this.operator = switch (ctx.op.getOpcode()) {
+			default -> new PcodeTernaryOperator(ctx.op);
+		};
+	}
+
+	@Override
+	protected int compareSameClassAndParams(
+			Statement o) {
+		return 0; // no extra fields to compare
+	}
+
+	@Override
+	public <A extends AbstractState<A>> AnalysisState<A> fwdTernarySemantics(
+			InterproceduralAnalysis<A> interprocedural,
+			AnalysisState<A> state,
+			SymbolicExpression left,
+			SymbolicExpression middle,
+			SymbolicExpression right,
+			StatementStore<A> expressions)
+			throws SemanticException {
+
+		return state.smallStepSemantics(
+				new TernaryExpression(
+						getStaticType(),
+						left,
+						middle,
+						right,
+						operator,
+						getLocation()),
+				this);
+	}
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/expressions/PcodeVarargsExpression.java

@@ -0,0 +1,81 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.pcode.expressions;
+
+import ghidra.lisa.pcode.contexts.VarargsExprContext;
+import it.unive.lisa.analysis.*;
+import it.unive.lisa.analysis.lattices.ExpressionSet;
+import it.unive.lisa.interprocedural.InterproceduralAnalysis;
+import it.unive.lisa.program.cfg.CFG;
+import it.unive.lisa.program.cfg.statement.Expression;
+import it.unive.lisa.program.cfg.statement.Statement;
+import it.unive.lisa.symbolic.SymbolicExpression;
+import it.unive.lisa.symbolic.value.BinaryExpression;
+import it.unive.lisa.symbolic.value.operator.binary.LogicalOr;
+
+public class PcodeVarargsExpression extends it.unive.lisa.program.cfg.statement.NaryExpression {
+
+	public PcodeVarargsExpression(CFG cfg, 
+			VarargsExprContext ctx, 
+			Expression[] exps) {
+		super(cfg, ctx.location(), ctx.mnemonic(), cfg.getDescriptor().getUnit().getProgram().getTypes().getIntegerType(), exps);
+	}
+
+	@Override
+	protected int compareSameClassAndParams(
+			Statement o) {
+		return 0; // no extra fields to compare
+	}
+
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
+			InterproceduralAnalysis<A> interprocedural,
+			AnalysisState<A> state,
+			SymbolicExpression left,
+			SymbolicExpression right,
+			StatementStore<A> expressions)
+			throws SemanticException {
+
+		return state.smallStepSemantics(
+			new BinaryExpression(
+				getStaticType(),
+				left,
+				right,
+				LogicalOr.INSTANCE,
+				getLocation()),
+			this);
+	}
+
+	@Override
+	public <A extends AbstractState<A>> AnalysisState<A> forwardSemanticsAux(
+			InterproceduralAnalysis<A> interprocedural,
+			AnalysisState<A> state,
+			ExpressionSet[] params,
+			StatementStore<A> expressions)
+			throws SemanticException {
+		AnalysisState<A> result = state.bottom();
+		for (SymbolicExpression expBase : params[0]) {
+			for (int i = 1; i < params.length; i++) {
+				for (SymbolicExpression exp : params[i]) {
+					//result = result.lub(state.smallStepSemantics(exp, this));
+					result = result.lub(
+						fwdBinarySemantics(interprocedural, state, expBase, exp, expressions));
+				}
+			}
+		}
+		return result;
+	}
+	
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/statements/PcodeTernaryOperator.java

@@ -0,0 +1,53 @@
+/* ###
+ * 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.lisa.pcode.statements;
+
+import java.util.Collections;
+import java.util.Set;
+
+import ghidra.program.model.pcode.PcodeOp;
+import it.unive.lisa.symbolic.value.operator.ternary.TernaryOperator;
+import it.unive.lisa.type.*;
+
+public class PcodeTernaryOperator implements TernaryOperator {
+
+		private PcodeOp op;
+
+		public PcodeTernaryOperator(PcodeOp op) {
+			this.op = op;
+		}
+
+		public PcodeOp getOp() {
+			return op;
+		}
+
+		@Override
+		public String toString() {
+			return op.getMnemonic();
+		}
+
+		@Override
+		public Set<Type> typeInference(
+				TypeSystem types,
+				Set<Type> left,
+				Set<Type> middle,
+				Set<Type> right) {
+			Set<Type> set = NumericType.commonNumericalType(left, right);
+			if (!set.isEmpty())
+				return set;
+			return Collections.singleton(types.getBooleanType());
+		}
+	}

Ghidra/Extensions/Lisa/src/test/java/ghidra/lisa/AbstractLisaTest.java

@@ -91,17 +91,23 @@ public class AbstractLisaTest extends AbstractGhidraHeadedIntegrationTest {
 
 	@Rule
 	public TestName name = new TestName();
-
+	private int pgmIndex;
+	
 	public AbstractLisaTest() {
-		init();
+		init(0);
+	}
+	
+	public AbstractLisaTest(int n) {
+		init(n);
 	}
 
 	protected String getProgramName() {
 		return "static-" + getClass().getCanonicalName() + "." + name.getMethodName();
 	}
-
-	public void init() {
+	
+	public void init(int n) {
 		try {
+			pgmIndex = n;
 			env = new TestEnv();
 			tool = env.getTool();
 			programManager = tool.getService(ProgramManager.class);
@@ -207,6 +213,235 @@ public class AbstractLisaTest extends AbstractGhidraHeadedIntegrationTest {
 		decompilerPanel = decompilerProvider.getDecompilerPanel();
 	}
 
+	private AssemblyBuffer getProgram(int index) throws Throwable {
+		return switch (index) {
+			case 7 -> getProgram_v7();
+			case 6 -> getProgram_v6();
+			case 5 -> getProgram_v5();
+			case 4 -> getProgram_v4();
+			case 3 -> getProgram_v3();
+			case 2 -> getProgram_v2();
+			case 1 -> getProgram_v1();
+			default -> getProgram_v0();
+		};
+	}
+	
+	protected AssemblyBuffer getProgram_v0() throws Throwable {
+		Assembler asm = Assemblers.getAssembler(program.getLanguage(), NO_16BIT_CALLS);
+		Address entry = addr(program, 0x00400000);
+		AssemblyBuffer buf = new AssemblyBuffer(asm, entry);
+
+		buf.assemble("PUSH RBP");
+		buf.assemble("MOV RBP, RSP");
+		buf.assemble("MOV RAX, 0x4");
+		buf.assemble("SUB RAX, 0x5");
+		buf.assemble("MOV RDX, RAX");
+		buf.assemble("RET");
+		return buf;
+	}
+
+	protected AssemblyBuffer getProgram_v1() throws Throwable {
+		Assembler asm = Assemblers.getAssembler(program.getLanguage(), NO_16BIT_CALLS);
+		Address entry = addr(program, 0x00400000);
+		AssemblyBuffer buf = new AssemblyBuffer(asm, entry);
+
+		buf.assemble("MOV RCX, 0x3");
+		buf.assemble("MOV RDX, 0x9");
+		buf.assemble("CMP ECX, EAX");
+		Address tgt0 = buf.getNext();
+		buf.assemble("JLE 0x%s".formatted(tgt0.add(5)));
+		buf.assemble("RET 0x8");
+		buf.assemble("SUB RAX, RCX");
+		buf.assemble("RET 0x8");
+		return buf;
+	}
+
+	protected AssemblyBuffer getProgram_v2() throws Throwable {
+		Assembler asm = Assemblers.getAssembler(program.getLanguage(), NO_16BIT_CALLS);
+		Address entry = addr(program, 0x00400000);
+		AssemblyBuffer buf = new AssemblyBuffer(asm, entry);
+
+		buf.assemble("MOV RCX, 0x3");
+		buf.assemble("MOV RDX, 0x9");
+		buf.assemble("CMP ECX, EAX");
+		Address tgt0 = buf.getNext();
+		buf.assemble("JLE 0x%s".formatted(tgt0.add(5)));
+		buf.assemble("RET 0x8");
+		buf.assemble("SUB RAX, RCX");
+		buf.assemble("CMP EAX, EDX");
+		Address tgt1 = buf.getNext();
+		buf.assemble("JG 0x%s".formatted(tgt1.add(5)));  // RAX > 9
+		buf.assemble("RET 0x8");
+		buf.assemble("ADD RCX, 0x3");
+		buf.assemble("SUB RAX, RCX");
+		buf.assemble("RET 0x8");
+		return buf;
+	}
+
+	protected AssemblyBuffer getProgram_v3() throws Throwable {
+		Assembler asm = Assemblers.getAssembler(program.getLanguage(), NO_16BIT_CALLS);
+		Address entry = addr(program, 0x00400000);
+		AssemblyBuffer buf = new AssemblyBuffer(asm, entry);
+
+		buf.assemble("MOV RAX, RAX");
+		buf.assemble("MOV RCX, 0x3");
+		buf.assemble("MOV RDX, 0x9");
+		buf.assemble("CMP ECX, EAX");
+		Address tgt0 = buf.getNext();
+		buf.assemble("JLE 0x%s".formatted(tgt0.add(11)));   // RAX >= 3
+		buf.assemble("SUB RAX, 0x5");   // RAX <= 3
+		buf.assemble("MOV RDX, RAX");   // RAX <= -2
+		Address tgt1 = buf.getNext();
+		buf.assemble("JMP 0x%s".formatted(tgt1.add(10)));
+		buf.assemble("CMP EAX, EDX");   // RAX >= 3
+		Address tgt2 = buf.getNext();
+		buf.assemble("JGE 0x%s".formatted(tgt2.add(10)));  // RAX >= 9
+		buf.assemble("ADD RCX, 0x5");   // 3 <= RAX < 9
+		buf.assemble("ADD RAX, 0x1F");  // RAX >= 3
+		buf.assemble("SAR RAX, 0x3");   // RAX >= -2
+		buf.assemble("AND RAX, -4");
+		buf.assemble("SUB RAX, 0x5");   
+		buf.assemble("SUB RAX, RCX");
+		buf.assemble("RET 0x8");
+		return buf;
+	}
+
+	protected AssemblyBuffer getProgram_v4() throws Throwable {
+		Assembler asm = Assemblers.getAssembler(program.getLanguage(), NO_16BIT_CALLS);
+		Address entry = addr(program, 0x00400000);
+		AssemblyBuffer buf = new AssemblyBuffer(asm, entry);
+
+		buf.assemble("MOV RAX, RAX");
+		buf.assemble("MOV RCX, 0x2");
+		buf.assemble("MOV RDX, 0x8");
+		buf.assemble("CMP ECX, EAX");
+		Address tgt0 = buf.getNext();
+		buf.assemble("JL 0x%s".formatted(tgt0.add(11)));   // RAX > 4
+		buf.assemble("SUB RAX, 0x5");   // RAX <= 3
+		buf.assemble("MOV RDX, RAX");   // RAX <= -2
+		Address tgt1 = buf.getNext();
+		buf.assemble("JMP 0x%s".formatted(tgt1.add(10)));
+		buf.assemble("CMP EAX, EDX");   // RAX >= 4
+		Address tgt2 = buf.getNext();
+		buf.assemble("JG 0x%s".formatted(tgt2.add(10)));  // RAX > 8
+		buf.assemble("ADD RCX, 0x5");   // 3 <= RAX <= 8
+		buf.assemble("ADD RAX, 0x1F");
+		buf.assemble("SAR RAX, 0x3");
+		buf.assemble("AND RAX, -4");
+		buf.assemble("SUB RAX, 0x5");
+		buf.assemble("SUB RAX, RCX");
+		buf.assemble("RET 0x8");
+		return buf;
+	}
+
+	protected AssemblyBuffer getProgram_v5() throws Throwable {
+		Assembler asm = Assemblers.getAssembler(program.getLanguage(), NO_16BIT_CALLS);
+		Address entry = addr(program, 0x00400000);
+		AssemblyBuffer buf = new AssemblyBuffer(asm, entry);
+
+		buf.assemble("MOV RAX, RAX");
+		buf.assemble("MOV RCX, 0x3");
+		buf.assemble("MOV RDX, 0x8");
+		buf.assemble("CMP ECX, EAX");
+		Address tgt0 = buf.getNext();
+		buf.assemble("JBE 0x%s".formatted(tgt0.add(11)));   // RAX >= 3
+		buf.assemble("SUB RAX, 0x5");   // RAX < 3
+		buf.assemble("MOV RDX, RAX");   // RAX < 8
+		Address tgt1 = buf.getNext();
+		buf.assemble("JMP 0x%s".formatted(tgt1.add(10)));
+		buf.assemble("CMP EAX, EDX");   // RAX >= 3
+		Address tgt2 = buf.getNext();
+		buf.assemble("JA 0x%s".formatted(tgt2.add(10)));  // RAX >= 9
+		buf.assemble("ADD RCX, 0x5");   // 3 <= RAX < 9
+		buf.assemble("ADD RAX, 0x1F");  // RAX >= 3
+		buf.assemble("SAR RAX, 0x3");   // RAX >= -2
+		buf.assemble("AND RAX, -4");
+		buf.assemble("SUB RAX, 0x5");
+		buf.assemble("SUB RAX, RCX");
+		buf.assemble("RET 0x8");
+		return buf;
+	}
+
+	protected AssemblyBuffer getProgram_v6() throws Throwable {
+		Assembler asm = Assemblers.getAssembler(program.getLanguage(), NO_16BIT_CALLS);
+		Address entry = addr(program, 0x00400000);
+		AssemblyBuffer buf = new AssemblyBuffer(asm, entry);
+
+		buf.assemble("MOV RAX, RAX");
+		buf.assemble("MOV RCX, 0x3");
+		buf.assemble("MOV RDX, 0x8");
+		buf.assemble("MOV RBX, 0x6");
+		buf.assemble("CMP EAX, ECX");
+		Address tgt0 = buf.getNext();
+		buf.assemble("JLE 0x%s".formatted(tgt0.add(32)));
+		Address tgt1 = buf.getNext();
+		buf.assemble("CMP RAX, RDX");			// RAX >= 4
+		buf.assemble("JG 0x%s".formatted(tgt1.add(27)));
+		buf.assemble("CMP AX, BX"); 			// 8 >= RAX >= 4
+		Address tgt2 = buf.getNext();
+		buf.assemble("JGE 0x%s".formatted(tgt2.add(16)));
+		buf.assemble("ADD RCX, 0x1");			// 5 >= RAX >= 4
+		buf.assemble("CMP EAX, ECX");
+		Address tgt3 = buf.getNext();
+		buf.assemble("JA 0x%s".formatted(tgt3.add(5)));
+		buf.assemble("RET 0x8");				// RAX == 4
+		buf.assemble("RET 0x8");				// RAX == 5
+		buf.assemble("RET 0x8");				// 8 >= RAX >= 6
+		buf.assemble("RET 0x8");				// RAX >= 9
+		buf.assemble("SUB RCX, 0x3");			// 3 >= RAX
+		buf.assemble("CMP EAX, ECX");
+		Address tgt4 = buf.getNext();
+		buf.assemble("JL 0x%s".formatted(tgt4.add(5)));
+		buf.assemble("RET 0x8");				// 3 >= RAX >= 1
+		buf.assemble("CMP AX, BX"); 			// -1 >= RAX
+		Address tgt5 = buf.getNext();
+		buf.assemble("JBE 0x%s".formatted(tgt5.add(5)));
+		buf.assemble("RET 0x8");				//  bottom
+		buf.assemble("RET 0x8");				// -1 >= RAX
+		buf.assemble("RET 0x8");				// 
+		return buf;
+	}
+
+	protected AssemblyBuffer getProgram_v7() throws Throwable {
+		Assembler asm = Assemblers.getAssembler(program.getLanguage(), NO_16BIT_CALLS);
+		Address entry = addr(program, 0x00400000);
+		AssemblyBuffer buf = new AssemblyBuffer(asm, entry);
+
+		buf.assemble("MOV RAX, RAX");
+		buf.assemble("MOV RCX, -0x3");
+		buf.assemble("MOV RDX, -0x8");
+		buf.assemble("MOV RBX, -0x6");
+		buf.assemble("CMP ECX, EAX");
+		Address tgt0 = buf.getNext();
+		buf.assemble("JLE 0x%s".formatted(tgt0.add(32)));
+		Address tgt1 = buf.getNext();
+		buf.assemble("CMP RDX, RAX");			// RAX >= 4
+		buf.assemble("JG 0x%s".formatted(tgt1.add(27)));
+		buf.assemble("CMP BX, AX"); 			// 8 >= RAX >= 4
+		Address tgt2 = buf.getNext();
+		buf.assemble("JGE 0x%s".formatted(tgt2.add(16)));
+		buf.assemble("SUB RCX, 0x1");			// 5 >= RAX >= 4
+		buf.assemble("CMP ECX, EAX");
+		Address tgt3 = buf.getNext();
+		buf.assemble("JA 0x%s".formatted(tgt3.add(5)));
+		buf.assemble("RET 0x8");				// RAX == 4
+		buf.assemble("RET 0x8");				// RAX == 5
+		buf.assemble("RET 0x8");				// 8 >= RAX >= 6
+		buf.assemble("RET 0x8");				// RAX >= 9
+		buf.assemble("ADD RCX, 0x3");			// 3 >= RAX
+		buf.assemble("CMP ECX, EAX");
+		Address tgt4 = buf.getNext();
+		buf.assemble("JL 0x%s".formatted(tgt4.add(5)));
+		buf.assemble("RET 0x8");				// 3 >= RAX >= 1
+		buf.assemble("CMP BX, AX"); 			// -1 >= RAX
+		Address tgt5 = buf.getNext();
+		buf.assemble("JBE 0x%s".formatted(tgt5.add(5)));
+		buf.assemble("RET 0x8");				//  bottom
+		buf.assemble("RET 0x8");				// -1 >= RAX
+		buf.assemble("RET 0x8");				// 
+		return buf;
+	}
+
 	protected Function createSimpleProgramX86_64() throws Throwable {
 		createProgram("x86:LE:64:default", "gcc");
 		intoProject(program);
@@ -224,15 +459,7 @@ public class AbstractLisaTest extends AbstractGhidraHeadedIntegrationTest {
 			program.getMemory()
 					.createInitializedBlock(".text", entry, 0x1000, (byte) 0, monitor, false);
 
-			Assembler asm = Assemblers.getAssembler(program.getLanguage(), NO_16BIT_CALLS);
-			AssemblyBuffer buf = new AssemblyBuffer(asm, entry);
-
-			buf.assemble("PUSH RBP");
-			buf.assemble("MOV RBP, RSP");
-			buf.assemble("MOV RAX, 0x4");
-			buf.assemble("SUB AX, 0x5");
-			buf.assemble("MOV RDX, RAX");
-			buf.assemble("RET");
+			AssemblyBuffer buf = getProgram(pgmIndex);
 			Address end = buf.getNext();
 
 			program.getMemory().setBytes(entry, buf.getBytes());

Ghidra/Extensions/Lisa/src/test/java/ghidra/lisa/NumericAnalysesTest.java

@@ -29,8 +29,8 @@ public class NumericAnalysesTest extends AbstractLisaTest {
 		lisaOptions.setValueDomain(ValueDomainOption.VALUE_CONSTPROP);
 		runTest();
 		equalsAssert(valueOf("0040000b:0:register:00000000"), "4");    	 //SUB AX, 0x5
-		equalsAssert(valueOf("0040000f:0:register:00000000"), "ffff");   //MOV RDX, RAX
-		equalsAssert(valueOf("00400012:0:register:00000010"), "ffff");   //RET
+		equalsAssert(valueOf("0040000f:0:register:00000000"), "-1");     //MOV RDX, RAX
+		equalsAssert(valueOf("00400012:0:register:00000010"), "-1");     //RET
 	}
 
 	@Category(AbstractLisaTest.class)
@@ -67,7 +67,6 @@ public class NumericAnalysesTest extends AbstractLisaTest {
 	@Category(AbstractLisaTest.class)
 	@Test
 	public void testPentagons() {
-		init();
 		lisaOptions.setValueDomain(ValueDomainOption.VALUE_PENTAGON);
 		runTest();
 		equalsAssert(valueOf("0040000b:0:register:00000000"), "[4, 4]");     //SUB AX, 0x5
@@ -94,4 +93,149 @@ public class NumericAnalysesTest extends AbstractLisaTest {
 		equalsAssert(valueOf("0040000f:0:register:00000000"), "{}");  //MOV RDX, RAX
 		equalsAssert(valueOf("00400012:0:register:00000010"), "{}");  //RET
 	}
+	
+	@Category(AbstractLisaTest.class)
+	@Test
+	public void testIntervalHighPcodePreState() {
+		init(1);
+		lisaOptions.setValueDomain(ValueDomainOption.VALUE_INTERVAL);
+		lisaOptions.setPostState(false);
+		lisaOptions.setHighPcode(true);
+		runTest();
+		equalsAssert(valueOf("0040000e:37:register:00000000"), null);
+		equalsAssert(valueOf("00400010:13:register:00000000"), "[-Inf, +Inf]");
+		equalsAssert(valueOf("00400018:47:register:00000000"), "[0, +Inf]");  // [3, +Inf] optimized out
+		equalsAssert(valueOf("00400012:46:register:00000000"), "[-Inf, 2]");
+	}
+
+	@Category(AbstractLisaTest.class)
+	@Test
+	public void testIntervalHighPcodePostState() {
+		init(2);
+		lisaOptions.setValueDomain(ValueDomainOption.VALUE_INTERVAL);
+		lisaOptions.setPostState(true);
+		lisaOptions.setHighPcode(true);
+		runTest();
+		equalsAssert(valueOf("0040000e:76:register:00000000"), "[-Inf, +Inf]");
+		equalsAssert(valueOf("00400012:18:register:00000000"), "[-Inf, 2]");
+		equalsAssert(valueOf("00400018:78:register:00000000"), "[0, +Inf]");  // [3, +Inf] optimized out
+		equalsAssert(valueOf("0040001c:45:register:00000000"), "[0, 9]");
+		equalsAssert(valueOf("00400026:67:register:00000000"), "[1, +Inf]");
+	}
+
+	@Category(AbstractLisaTest.class)
+	@Test
+	public void testIntervalHighPcodePhi() {
+		init(3);
+		lisaOptions.setValueDomain(ValueDomainOption.VALUE_INTERVAL);
+		lisaOptions.setPostState(true);
+		lisaOptions.setHighPcode(true);
+		runTest();
+		equalsAssert(valueOf("0040000a:2:register:00000000"), null);
+		equalsAssert(valueOf("00400011:142:register:00000000"), "[-Inf, +Inf]");
+		equalsAssert(valueOf("0040001c:26:register:00000000"), "[-Inf, -3]");
+		equalsAssert(valueOf("00400011:142:register:00000000"), "[-Inf, +Inf]");
+		equalsAssert(valueOf("00400020:111:register:00000000"), "[3, +Inf]");
+		equalsAssert(valueOf("00400022:115:register:00000000"), "[3, 8]");
+		equalsAssert(valueOf("00400026:29:register:00000000"), "[-Inf, 39]");
+		equalsAssert(valueOf("0040002a:38:register:00000000"), "[-Inf, +Inf]");
+	}
+
+	@Category(AbstractLisaTest.class)
+	@Test
+	public void testIntervalLowPcodePhiJLE() {
+		init(3);
+		lisaOptions.setValueDomain(ValueDomainOption.VALUE_INTERVAL_LX86);
+		lisaOptions.setPostState(true);
+		lisaOptions.setHighPcode(false);
+		runTest();
+		equalsAssert(valueOf("00400011:0:register:00000000"), "[-Inf, +Inf]");
+		equalsAssert(valueOf("0040001c:0:register:00000000"), "[-Inf, -3]");
+		equalsAssert(valueOf("0040001e:0:register:00000000"), "[3, +Inf]");
+		equalsAssert(valueOf("00400022:0:register:00000000"), "[3, 8]");
+		equalsAssert(valueOf("00400026:0:register:00000000"), "[-Inf, 8]");
+		equalsAssert(valueOf("00400026:3:register:00000000"), "[-Inf, 39]");
+		equalsAssert(valueOf("0040002a:0:register:00000000"), "[-Inf, +Inf]");
+	}
+
+	@Category(AbstractLisaTest.class)
+	@Test
+	public void testIntervalLowPcodePhiJL() {
+		init(4);
+		lisaOptions.setValueDomain(ValueDomainOption.VALUE_INTERVAL_LX86);
+		lisaOptions.setPostState(true);
+		lisaOptions.setHighPcode(false);
+		runTest();
+		equalsAssert(valueOf("00400011:0:register:00000000"), "[-Inf, +Inf]");
+		equalsAssert(valueOf("0040001c:0:register:00000000"), "[-Inf, -3]");
+		equalsAssert(valueOf("0040001e:0:register:00000000"), "[3, +Inf]");
+		equalsAssert(valueOf("00400022:0:register:00000000"), "[3, 8]");
+		equalsAssert(valueOf("00400026:0:register:00000000"), "[-Inf, 8]");
+		equalsAssert(valueOf("00400026:3:register:00000000"), "[-Inf, 39]");
+		equalsAssert(valueOf("0040002a:0:register:00000000"), "[-Inf, +Inf]");
+	}
+
+	@Category(AbstractLisaTest.class)
+	@Test
+	public void testIntervalLowPcodePhiJBE() {
+		init(5);
+		lisaOptions.setValueDomain(ValueDomainOption.VALUE_INTERVAL_LX86);
+		lisaOptions.setPostState(true);
+		lisaOptions.setHighPcode(false);
+		runTest();
+		equalsAssert(valueOf("00400011:0:register:00000000"), "[-Inf, +Inf]");
+		equalsAssert(valueOf("0040001c:0:register:00000000"), "[-Inf, -3]");
+		equalsAssert(valueOf("0040001e:0:register:00000000"), "[3, +Inf]");
+		equalsAssert(valueOf("00400022:0:register:00000000"), "[3, 8]");
+		equalsAssert(valueOf("00400026:0:register:00000000"), "[-Inf, 8]");
+		equalsAssert(valueOf("00400026:3:register:00000000"), "[-Inf, 39]");
+		equalsAssert(valueOf("0040002a:0:register:00000000"), "[-Inf, +Inf]");
+	}
+
+	@Category(AbstractLisaTest.class)
+	@Test
+	public void testIntervalLowAll() {
+		init(6);
+		lisaOptions.setValueDomain(ValueDomainOption.VALUE_INTERVAL_LX86);
+		lisaOptions.setPostState(true);
+		lisaOptions.setHighPcode(false);
+		runTest();
+		equalsAssert(valueOf("00400011:0:register:00000000"), "[-Inf, +Inf]");
+		equalsAssert(valueOf("0040001c:0:register:00000000"), "[4, +Inf]");
+		equalsAssert(valueOf("00400021:0:register:00000000"), "[4, 8]");
+		equalsAssert(valueOf("00400026:0:register:00000000"), "[4, 5]");
+		equalsAssert(valueOf("0040002e:0:register:00000000"), "[4, 4]");
+		equalsAssert(valueOf("00400031:0:register:00000000"), "[5, 5]");
+		equalsAssert(valueOf("00400034:0:register:00000000"), "[6, 8]");
+		equalsAssert(valueOf("00400037:0:register:00000000"), "[9, +Inf]");
+		equalsAssert(valueOf("0040003a:0:register:00000000"), "[-Inf, 3]");
+		equalsAssert(valueOf("00400042:0:register:00000000"), "[0, 3]");
+		equalsAssert(valueOf("00400045:0:register:00000000"), "[-Inf, -1]");
+		equalsAssert(valueOf("0040004a:0:register:00000000"), "[-Inf, -1]");  // Should be _|_
+		equalsAssert(valueOf("0040004d:0:register:00000000"), "[-Inf, -1]");
+	}
+
+	@Category(AbstractLisaTest.class)
+	@Test
+	public void testIntervalLowAllRev() {
+		init(7);
+		lisaOptions.setValueDomain(ValueDomainOption.VALUE_INTERVAL_LX86);
+		lisaOptions.setPostState(true);
+		lisaOptions.setHighPcode(false);
+		runTest();
+		equalsAssert(valueOf("00400011:0:register:00000000"), "[-Inf, +Inf]");
+		equalsAssert(valueOf("0040001c:0:register:00000000"), "[-Inf, -4]");
+		equalsAssert(valueOf("00400021:0:register:00000000"), "[-8, -4]");
+		equalsAssert(valueOf("00400026:0:register:00000000"), "[-5, -4]");
+		equalsAssert(valueOf("0040002e:0:register:00000000"), "[-4, -4]");
+		equalsAssert(valueOf("00400031:0:register:00000000"), "[-5, -5]");
+		equalsAssert(valueOf("00400034:0:register:00000000"), "[-8, -6]");
+		equalsAssert(valueOf("00400037:0:register:00000000"), "[-Inf, -9]");
+		equalsAssert(valueOf("0040003a:0:register:00000000"), "[-3, +Inf]");
+		equalsAssert(valueOf("00400042:0:register:00000000"), "[-3, 0]");
+		equalsAssert(valueOf("00400045:0:register:00000000"), "[1, +Inf]");
+		equalsAssert(valueOf("0040004a:0:register:00000000"), "_|_");
+		equalsAssert(valueOf("0040004d:0:register:00000000"), "[1, +Inf]");
+	}
+
 }