GP-6225: Adds abstract interpretation via the Software and System

Verification (SSV) group @ Università Ca' Foscari's Library for Static
Analysis (LiSA)

Ghidra/Extensions/Lisa/Module.manifest

@@ -0,0 +1,4 @@
+MODULE FILE LICENSE: lib/lisa-analyses-0.1.jar MIT
+MODULE FILE LICENSE: lib/lisa-program-0.1.jar MIT
+MODULE FILE LICENSE: lib/lisa-sdk-0.1.jar MIT
+MODULE FILE LICENSE: lib/joda-time-2.14.0.jar Apache License 2.0

Ghidra/Extensions/Lisa/build.gradle

@@ -0,0 +1,57 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+apply from: "$rootProject.projectDir/gradle/distributableGhidraExtension.gradle"
+//apply from: "$rootProject.projectDir/gradle/distributableGhidraModule.gradle"
+apply from: "$rootProject.projectDir/gradle/javaProject.gradle"
+apply from: "$rootProject.projectDir/gradle/helpProject.gradle"
+apply from: "$rootProject.projectDir/gradle/javaTestProject.gradle"
+
+apply plugin: 'eclipse'
+eclipse.project.name = 'Xtra Lisa'
+
+dependencies {
+	api project(':Base')
+	api project(':Decompiler')
+	api project(':DecompilerDependent')
+	
+    api("io.github.lisa-analyzer:lisa-analyses:0.1") {
+        exclude group: 'org.apache.commons'
+        exclude group: 'org.apache.logging.log4j'
+        exclude group: 'com.fasterxml.jackson.core'
+        exclude group: 'org.graphstream'
+        exclude group: 'org.reflections'
+    }
+    api("io.github.lisa-analyzer:lisa-program:0.1") {
+        exclude group: 'org.apache.commons'
+        exclude group: 'org.apache.logging.log4j'
+        exclude group: 'com.fasterxml.jackson.core'
+        exclude group: 'org.graphstream'
+        exclude group: 'org.reflections'
+    }
+    api("io.github.lisa-analyzer:lisa-sdk:0.1") {
+        exclude group: 'org.apache.commons'
+        exclude group: 'org.apache.logging.log4j'
+        exclude group: 'com.fasterxml.jackson.core'
+        exclude group: 'org.graphstream'
+        exclude group: 'org.reflections'
+    }	
+
+    // Joda is needed at run time
+    api "joda-time:joda-time:2.14.0"
+}
+
+
+

Ghidra/Extensions/Lisa/certification.manifest

@@ -0,0 +1,8 @@
+##VERSION: 2.0
+##MODULE IP: Apache License 2.0
+##MODULE IP: MIT
+Module.manifest||GHIDRA||||END|
+extension.properties||GHIDRA||||END|
+src/main/help/help/TOC_Source.xml||GHIDRA||||END|
+src/main/help/help/topics/LisaPlugin/LisaPlugin.html||GHIDRA||||END|
+src/main/java/ghidra/lisa/pcode/analyses/README.md||GHIDRA||||END|

Ghidra/Extensions/Lisa/extension.properties

@@ -0,0 +1,5 @@
+name=Lisa
+description=Abstract interpretation engine based on the Universita Ca Foscari's Library for Static Analysis (LiSA)
+author=Ghidra Team
+createdOn=9/9/2025
+version=@extversion@

Ghidra/Extensions/Lisa/ghidra_scripts/LisaLaunchScript.java

@@ -0,0 +1,116 @@
+/* ###
+ * 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.
+ */
+
+//Template for running analyses using Lisa (does very little, as is)
+//@category PCode
+
+import java.util.*;
+
+import ghidra.app.script.GhidraScript;
+import ghidra.lisa.pcode.PcodeFrontend;
+import ghidra.lisa.pcode.analyses.PcodeByteBasedConstantPropagation;
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.util.Msg;
+import it.unive.lisa.*;
+import it.unive.lisa.analysis.*;
+import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
+import it.unive.lisa.interprocedural.InterproceduralAnalysis;
+import it.unive.lisa.program.Program;
+import it.unive.lisa.program.cfg.CFG;
+import it.unive.lisa.program.cfg.statement.Statement;
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.util.representation.StructuredRepresentation;
+
+public class LisaLaunchScript extends GhidraScript {
+
+	@Override
+	public void run() throws Exception {
+		if (isRunningHeadless()) {
+			popup("Script is not running in GUI");
+			return;
+		}
+
+		PcodeFrontend frontend = new PcodeFrontend();
+		Program p = frontend.doWork(currentProgram.getListing(), currentAddress);
+
+		DefaultConfiguration conf = new DefaultConfiguration();
+		conf.serializeResults = true;
+		conf.abstractState = DefaultConfiguration.simpleState(
+			DefaultConfiguration.defaultHeapDomain(),
+			//new DefiniteDataflowDomain<>(new ConstantPropagation()),
+			new ValueEnvironment<>(
+				new PcodeByteBasedConstantPropagation(currentProgram.getLanguage())),
+			DefaultConfiguration.defaultTypeDomain());
+		LiSA lisa = new LiSA(conf);
+
+		LiSAReport report = lisa.run(p);
+		InterproceduralAnalysis<?> interproceduralAnalysis =
+			report.getConfiguration().interproceduralAnalysis;
+		Collection<CFG> ep = p.getEntryPoints();
+		for (CFG cfg : ep) {
+			Collection<?> results = interproceduralAnalysis.getAnalysisResultsOf(cfg);
+			Iterator<?> iterator = results.iterator();
+			while (iterator.hasNext()) {
+				Object next = iterator.next();
+				if (next instanceof AnalyzedCFG<?> acfg) {
+					processCFG(cfg, acfg);
+				}
+			}
+		}
+
+	}
+
+	private void processCFG(CFG cfg, AnalyzedCFG<?> acfg) {
+		if (!cfg.getNodes().isEmpty()) {
+			for (Statement st : cfg.getNodes()) {
+				AnalysisState<?> s = acfg.getAnalysisStateAfter(st);
+				AbstractState<?> abs = s.getState();
+				if (abs instanceof SimpleAbstractState sas) {
+					processState(sas, st);
+				}
+			}
+		}
+	}
+
+	@SuppressWarnings("rawtypes")
+	private void processState(SimpleAbstractState sas, Statement st) {
+		ValueEnvironment<?> valueState =
+			(ValueEnvironment<?>) sas.getValueState();
+		//DefiniteDataflowDomain valueState = (DefiniteDataflowDomain) sas.getValueState();
+		Map<Identifier, ?> function = valueState.function;
+		if (function != null) {
+			for (Object key : function.keySet()) {
+				Object val = valueState.function.get(key);
+				exampleAnalysis(st, key, val);
+			}
+		}
+	}
+
+	private void exampleAnalysis(Statement st, Object key, Object val) {
+		if (val instanceof PcodeByteBasedConstantPropagation icp) {
+			StructuredRepresentation representation =
+				icp.representation();
+			String rep = representation.toString();
+			if (!rep.contains("TOP")) {
+				PcodeLocation loc =
+					(PcodeLocation) st.getLocation();
+				Msg.info(this, loc.getCodeLocation() +
+					" ==> " + key + ":" + representation);
+			}
+		}
+	}
+
+}

Ghidra/Extensions/Lisa/ghidra_scripts/Lisa_ResolveX86orX64LinuxSyscallsScript.java

@@ -0,0 +1,457 @@
+/* ###
+ * 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.
+ */
+
+//Uses overriding references and the LiSA constant propagator to resolve system calls
+//@category Analysis
+
+import java.io.*;
+import java.util.*;
+import java.util.Map.Entry;
+import java.util.function.Predicate;
+
+import generic.jar.ResourceFile;
+import ghidra.app.cmd.function.ApplyFunctionDataTypesCmd;
+import ghidra.app.cmd.memory.AddUninitializedMemoryBlockCmd;
+import ghidra.app.plugin.core.analysis.AutoAnalysisManager;
+import ghidra.app.script.GhidraScript;
+import ghidra.app.services.DataTypeManagerService;
+import ghidra.app.util.opinion.ElfLoader;
+import ghidra.framework.Application;
+import ghidra.lisa.pcode.PcodeFrontend;
+import ghidra.lisa.pcode.analyses.PcodeByteBasedConstantPropagation;
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.program.model.address.*;
+import ghidra.program.model.data.DataTypeManager;
+import ghidra.program.model.lang.Register;
+import ghidra.program.model.lang.SpaceNames;
+import ghidra.program.model.listing.*;
+import ghidra.program.model.mem.MemoryAccessException;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.program.model.symbol.*;
+import ghidra.util.Msg;
+import ghidra.util.exception.CancelledException;
+import ghidra.util.task.TaskMonitor;
+import it.unive.lisa.*;
+import it.unive.lisa.analysis.*;
+import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
+import it.unive.lisa.interprocedural.InterproceduralAnalysis;
+import it.unive.lisa.program.cfg.CFG;
+import it.unive.lisa.program.cfg.statement.Statement;
+import it.unive.lisa.symbolic.value.Identifier;
+
+/**
+ * This script will resolve system calls for x86 or x64 Linux binaries.
+ * It assumes that in the x64 case, the syscall native instruction is used to make system calls,
+ * and in the x86 case, system calls are made via an indirect call to GS:[0x10].
+ * It should be straightforward to modify this script for other cases.
+ */
+public class Lisa_ResolveX86orX64LinuxSyscallsScript extends GhidraScript {
+
+	//disassembles to "CALL dword ptr GS:[0x10]"
+	private static final byte[] x86_bytes = { 0x65, -1, 0x15, 0x10, 0x00, 0x00, 0x00 };
+
+	private static final String X86 = "x86";
+
+	private static final String SYSCALL_SPACE_NAME = "syscall";
+
+	private static final int SYSCALL_SPACE_LENGTH = 0x10000;
+
+	//this is the name of the userop (aka CALLOTHER) in the pcode translation of the
+	//native "syscall" instruction
+	private static final String SYSCALL_X64_CALLOTHER = "syscall";
+
+	//a set of names of all syscalls that do not return
+	private static final Set<String> noreturnSyscalls = Set.of("exit", "exit_group");
+
+	//tests whether an instruction is making a system call
+	private Predicate<Instruction> tester;
+
+	//register holding the syscall number
+	private String syscallRegister;
+
+	//datatype archive containing signature of system calls
+	private String datatypeArchiveName;
+
+	//file containing map from syscall numbers to syscall names
+	//note that different architectures can have different system call numbers, even
+	//if they're both Linux...
+	private String syscallFileName;
+
+	//the type of overriding reference to apply 
+	private RefType overrideType;
+
+	//the calling convention to use for system calls (must be defined in the appropriate .cspec file)
+	private String callingConvention;
+
+	private InterproceduralAnalysis<?> ipa;
+
+	private PcodeFrontend frontend;
+
+	private LiSA lisa;
+
+	private Map<Address, CFG> targets = new HashMap<>();
+
+	@Override
+	protected void run() throws Exception {
+
+		if (!(currentProgram.getExecutableFormat().equals(ElfLoader.ELF_NAME) &&
+			currentProgram.getLanguage().getProcessor().toString().equals(X86))) {
+			popup("This script is intended for x86 or x64 Linux files");
+			return;
+		}
+
+		//determine whether the executable is 32 or 64 bit and set fields appropriately
+		int size = currentProgram.getLanguage().getLanguageDescription().getSize();
+		if (size == 64) {
+			tester = Lisa_ResolveX86orX64LinuxSyscallsScript::checkX64Instruction;
+			syscallRegister = "RAX";
+			datatypeArchiveName = "generic_clib_64";
+			syscallFileName = "x64_linux_syscall_numbers";
+			overrideType = RefType.CALLOTHER_OVERRIDE_CALL;
+			callingConvention = "syscall";
+		}
+		else {
+			tester = Lisa_ResolveX86orX64LinuxSyscallsScript::checkX86Instruction;
+			syscallRegister = "EAX";
+			datatypeArchiveName = "generic_clib";
+			syscallFileName = "x86_linux_syscall_numbers";
+			overrideType = RefType.CALL_OVERRIDE_UNCONDITIONAL;
+			callingConvention = "syscall";
+		}
+
+		//get the space where the system calls live.  
+		//If it doesn't exist, create it.
+		AddressSpace syscallSpace =
+			currentProgram.getAddressFactory().getAddressSpace(SYSCALL_SPACE_NAME);
+		if (syscallSpace == null) {
+			//don't muck with address spaces if you don't have exclusive access to the program.
+			if (!currentProgram.hasExclusiveAccess()) {
+				popup("Must have exclusive access to " + currentProgram.getName() +
+					" to run this script");
+				return;
+			}
+			Address startAddr = currentProgram.getAddressFactory()
+					.getAddressSpace(SpaceNames.OTHER_SPACE_NAME)
+					.getAddress(0x0L);
+			AddUninitializedMemoryBlockCmd cmd = new AddUninitializedMemoryBlockCmd(
+				SYSCALL_SPACE_NAME, null, this.getClass().getName(), startAddr,
+				SYSCALL_SPACE_LENGTH, true, true, true, false, true);
+			if (!cmd.applyTo(currentProgram)) {
+				popup("Failed to create " + SYSCALL_SPACE_NAME);
+				return;
+			}
+			syscallSpace = currentProgram.getAddressFactory().getAddressSpace(SYSCALL_SPACE_NAME);
+		}
+		else {
+			printf("AddressSpace %s found, continuing...\n", SYSCALL_SPACE_NAME);
+		}
+
+		//get all of the functions that contain system calls
+		//note that this will not find system call instructions that are not in defined functions
+		Map<Function, Set<Address>> funcsToCalls = getSyscallsInFunctions(currentProgram, monitor);
+
+		if (funcsToCalls.isEmpty()) {
+			popup("No system calls found (within defined functions)");
+			return;
+		}
+
+		//get the system call number at each callsite of a system call.
+		//note that this is not guaranteed to succeed at a given system call call site -
+		//it might be hard (or impossible) to determine a specific constant
+		Map<Address, Long> addressesToSyscalls =
+			resolveConstants(funcsToCalls, currentProgram, monitor);
+
+		if (addressesToSyscalls.isEmpty()) {
+			popup("Couldn't resolve any syscall constants");
+			return;
+		}
+
+		//get the map from system call numbers to system call names
+		//you might have to create this yourself!
+		Map<Long, String> syscallNumbersToNames = getSyscallNumberMap();
+
+		//at each system call call site where a constant could be determined, create
+		//the system call (if not already created), then add the appropriate overriding reference
+		//use syscallNumbersToNames to name the created functions
+		//if there's not a name corresponding to the constant use a default 
+		for (Entry<Address, Long> entry : addressesToSyscalls.entrySet()) {
+			Address callSite = entry.getKey();
+			Long offset = entry.getValue();
+			printerr(callSite + ":" + Long.toHexString(offset));
+			Address callTarget = syscallSpace.getAddress(offset);
+			Function callee = currentProgram.getFunctionManager().getFunctionAt(callTarget);
+			if (callee == null) {
+				String funcName = "syscall_" + String.format("%08X", offset);
+				if (syscallNumbersToNames.get(offset) != null) {
+					funcName = syscallNumbersToNames.get(offset);
+				}
+				callee = createFunction(callTarget, funcName);
+				if (callee == null) {
+					continue;
+				}
+				callee.setCallingConvention(callingConvention);
+
+				//check if the function name is one of the non-returning syscalls
+				if (noreturnSyscalls.contains(funcName)) {
+					callee.setNoReturn(true);
+				}
+			}
+			Reference ref = currentProgram.getReferenceManager()
+					.addMemoryReference(callSite, callTarget, overrideType, SourceType.USER_DEFINED,
+						Reference.MNEMONIC);
+			//overriding references must be primary to be active
+			currentProgram.getReferenceManager().setPrimary(ref, true);
+		}
+
+		//finally, open the appropriate data type archive and apply its function data types
+		//to the new system call space, so that the system calls have the correct signatures
+		AutoAnalysisManager mgr = AutoAnalysisManager.getAnalysisManager(currentProgram);
+		DataTypeManagerService service = mgr.getDataTypeManagerService();
+		List<DataTypeManager> dataTypeManagers = new ArrayList<>();
+		dataTypeManagers.add(service.openDataTypeArchive(datatypeArchiveName));
+		dataTypeManagers.add(currentProgram.getDataTypeManager());
+		ApplyFunctionDataTypesCmd cmd = new ApplyFunctionDataTypesCmd(dataTypeManagers,
+			new AddressSet(syscallSpace.getMinAddress(), syscallSpace.getMaxAddress()),
+			SourceType.USER_DEFINED, false, false);
+		cmd.applyTo(currentProgram);
+	}
+
+	private Map<Long, String> getSyscallNumberMap() {
+		Map<Long, String> syscallMap = new HashMap<>();
+		ResourceFile rFile = Application.findDataFileInAnyModule(syscallFileName);
+		if (rFile == null) {
+			popup("Error opening syscall number file, using default names");
+			return syscallMap;
+		}
+		try (FileReader fReader = new FileReader(rFile.getFile(false));
+				BufferedReader bReader = new BufferedReader(fReader)) {
+			String line = null;
+			while ((line = bReader.readLine()) != null) {
+				//lines starting with # are comments
+				if (!line.startsWith("#")) {
+					String[] parts = line.trim().split(" ");
+					Long number = Long.parseLong(parts[0]);
+					syscallMap.put(number, parts[1]);
+				}
+			}
+		}
+		catch (IOException e) {
+			Msg.showError(this, null, "Error reading syscall map file", e.getMessage(), e);
+		}
+		return syscallMap;
+	}
+
+	/**
+	 * Scans through all of the functions defined in {@code program} and returns
+	 * a map which takes a function to the set of address in its body which contain
+	 * system calls
+	 * @param program program containing functions
+	 * @param tMonitor monitor
+	 * @return map function -> addresses in function containing syscalls
+	 * @throws CancelledException if the user cancels
+	 */
+	private Map<Function, Set<Address>> getSyscallsInFunctions(Program program,
+			TaskMonitor tMonitor) throws CancelledException {
+		Map<Function, Set<Address>> funcsToCalls = new HashMap<>();
+		for (Function func : program.getFunctionManager().getFunctionsNoStubs(true)) {
+			tMonitor.checkCancelled();
+			for (Instruction inst : program.getListing().getInstructions(func.getBody(), true)) {
+				if (tester.test(inst)) {
+					Set<Address> callSites = funcsToCalls.get(func);
+					if (callSites == null) {
+						callSites = new HashSet<>();
+						funcsToCalls.put(func, callSites);
+					}
+					callSites.add(inst.getAddress());
+				}
+			}
+		}
+		return funcsToCalls;
+	}
+
+	/**
+	 * Uses the LiSA constant propagator to attempt to determine the constant value in
+	 * the syscall register at each system call instruction
+	 * 
+	 * @param funcsToCalls map from functions containing syscalls to address in each function of 
+	 * the system call
+	 * @param program containing the functions
+	 * @return map from addresses of system calls to system call numbers
+	 * @throws CancelledException if the user cancels
+	 */
+	private Map<Address, Long> resolveConstants(Map<Function, Set<Address>> funcsToCalls,
+			Program program, TaskMonitor tMonitor) throws CancelledException {
+		initLisa();
+		Set<CFG> cfgs = new HashSet<>();
+		for (Function func : funcsToCalls.keySet()) {
+			CFG cfg = frontend.visitFunction(func, func.getEntryPoint());
+			cfgs.add(cfg);
+		}
+		it.unive.lisa.program.Program p = frontend.getProgram();
+		Collection<CFG> baseline = p.getAllCFGs();
+		for (CFG cfg : cfgs) {
+			if (baseline.contains(cfg)) {
+				p.addEntryPoint(cfg);
+			}
+		}
+
+		LiSAReport report = lisa.run(p);
+		ipa = report.getConfiguration().interproceduralAnalysis;
+		storeResults(frontend.getProgram(), ipa);
+
+		Map<Address, Long> addressesToSyscalls = new HashMap<>();
+		Register syscallReg = program.getLanguage().getRegister(syscallRegister);
+		for (Function func : funcsToCalls.keySet()) {
+			for (Address callSite : funcsToCalls.get(func)) {
+				long val = getRegisterValue(callSite, syscallReg);
+				if (val == -1) {
+					//createBookmark(callSite, "System Call",
+					//	"Couldn't resolve value of " + syscallReg);
+					//printf("Couldn't resolve value of " + syscallReg + " at " + callSite + "\n");
+					continue;
+				}
+				addressesToSyscalls.put(callSite, val);
+			}
+		}
+		return addressesToSyscalls;
+	}
+
+	private long getRegisterValue(Address callSite, Register syscallReg) {
+		Set<Statement> set = frontend.getStatement(callSite);
+		if (set == null) {
+			printerr("Null set for " + callSite);
+			return -1;
+		}
+		String offset = syscallReg.getAddress().toString();
+		Function f = currentProgram.getListing().getFunctionContaining(callSite);
+		CFG cfg = targets.get(f.getEntryPoint());
+		if (cfg == null) {
+			printerr("Null cfg for " + callSite);
+			return -1;
+		}
+		Collection<?> results = ipa.getAnalysisResultsOf(cfg);
+		Statement st = null;
+		for (Statement obj : set) {
+			PcodeLocation loc = (PcodeLocation) obj.getLocation();
+			if (loc.op.getOpcode() >= PcodeOp.CALL && loc.op.getOpcode() <= PcodeOp.CALLOTHER) {
+				st = obj;
+			}
+		}
+		if (st == null) {
+			printerr("Null statement for " + callSite);
+			return -1;
+		}
+		Iterator<?> iterator = results.iterator();
+		while (iterator.hasNext()) {
+			Object next = iterator.next();
+			if (next instanceof AnalyzedCFG<?> acfg) {
+				AnalysisState<?> state1;
+				try {
+					state1 = acfg.getAnalysisStateBefore(st);
+					AbstractState<?> state2 = state1.getState();
+					if (state2 instanceof SimpleAbstractState sas) {
+						ValueEnvironment<?> valueState = (ValueEnvironment<?>) sas.getValueState();
+						Map<Identifier, ?> function = valueState.function;
+						if (function != null) {
+							for (Object key : function.keySet()) {
+								Object val = valueState.function.get(key);
+								if (val instanceof PcodeByteBasedConstantPropagation icp) {
+									String keyStr = key.toString();
+									if (keyStr.equals(offset)) {
+										String valstr = icp.representation().toString();
+										if (!valstr.contains("#TOP#")) {
+											return Long.parseLong(valstr);
+										}
+									}
+								}
+							}
+						}
+					}
+				}
+				catch (Exception e) {
+					printerr(e.getMessage());
+				}
+			}
+		}
+		return -1;
+	}
+
+	private void initLisa() {
+		frontend = new PcodeFrontend();
+
+		DefaultConfiguration conf = new DefaultConfiguration();
+		conf.serializeResults = true;
+		conf.abstractState = DefaultConfiguration.simpleState(
+			DefaultConfiguration.defaultHeapDomain(),
+			new ValueEnvironment<>(
+				new PcodeByteBasedConstantPropagation(currentProgram.getLanguage())),
+			DefaultConfiguration.defaultTypeDomain());
+		conf.serializeResults = false;
+		lisa = new LiSA(conf);
+	}
+
+	private void storeResults(it.unive.lisa.program.Program p,
+			InterproceduralAnalysis<?> interproceduralAnalysis) {
+		Collection<CFG> ep = p.getEntryPoints();
+		for (CFG cfg : ep) {
+			Collection<Statement> entrypoints = cfg.getEntrypoints();
+			for (Statement st : entrypoints) {
+				PcodeLocation loc = (PcodeLocation) st.getLocation();
+				Address target = loc.op.getSeqnum().getTarget();
+				Function f = currentProgram.getListing().getFunctionContaining(target);
+				targets.put(f.getEntryPoint(), cfg);
+			}
+		}
+	}
+
+	/**
+	 * Checks whether an x86 native instruction is a system call
+	 * @param inst instruction to check
+	 * @return true precisely when the instruction is a system call
+	 */
+	private static boolean checkX86Instruction(Instruction inst) {
+		try {
+			return Arrays.equals(x86_bytes, inst.getBytes());
+		}
+		catch (MemoryAccessException e) {
+			Msg.info(Lisa_ResolveX86orX64LinuxSyscallsScript.class,
+				"MemoryAccessException at " + inst.getAddress().toString());
+			return false;
+		}
+	}
+
+	/**
+	 * Checks whether an x64 instruction is a system call
+	 * @param inst instruction to check
+	 * @return true precisely when the instruction is a system call
+	 */
+	private static boolean checkX64Instruction(Instruction inst) {
+		boolean retVal = false;
+		for (PcodeOp op : inst.getPcode()) {
+			if (op.getOpcode() == PcodeOp.CALLOTHER) {
+				int index = (int) op.getInput(0).getOffset();
+				if (inst.getProgram()
+						.getLanguage()
+						.getUserDefinedOpName(index)
+						.equals(SYSCALL_X64_CALLOTHER)) {
+					retVal = true;
+				}
+			}
+		}
+		return retVal;
+	}
+
+}

Ghidra/Extensions/Lisa/src/main/help/help/TOC_Source.xml

@@ -0,0 +1,19 @@
+<?xml version='1.0' encoding='ISO-8859-1'?>
+<!-- See Base's TOC_Source.xml for help -->
+<tocroot>
+	<tocref id="Ghidra Functionality">
+		<tocdef id="Lisa Plugin" text="Lisa Plugin"
+			target="help/topics/LisaPlugin/LisaPlugin.html">
+
+			<tocdef id="add_cfgs" text="Add CFGs"
+				target="help/topics/LisaPlugin/LisaPlugin.html#add_cfgs" />
+				
+			<tocdef id="clear_cfgs" text="Clear CFGs"
+				target="help/topics/LisaPlugin/LisaPlugin.html#clear_cfgs" />
+				
+			<tocdef id="set_taint" text="Taint"
+				target="help/topics/LisaPlugin/LisaPlugin.html#set_taint" />
+
+		</tocdef>
+	</tocref>
+</tocroot>

Ghidra/Extensions/Lisa/src/main/help/help/topics/LisaPlugin/LisaPlugin.html

@@ -0,0 +1,134 @@
+<!DOCTYPE doctype PUBLIC "-//W3C//DTD HTML 4.0 Frameset//EN">
+
+<HTML>
+  <HEAD>
+    <META name="generator" content=
+    "HTML Tidy for Java (vers. 2009-12-01), see jtidy.sourceforge.net">
+
+    <TITLE>Abstract Interpretation: LiSA</TITLE>
+    <META http-equiv="Content-Type" content="text/html; charset=windows-1252">
+    <LINK rel="stylesheet" type="text/css" href="help/shared/DefaultStyle.css">
+  </HEAD>
+
+  <BODY lang="EN-US">
+    <H1><A name="LisaPlugin"></A>Abstract Interpretation: LiSA</H1>
+
+    <P>The Lisa Plugin uses the "Library for Static Analysis", <B>LiSA</B>, developed and maintained
+		by the Software and System Verification (SSV) group at Universita Ca' Foscari in Venice, Italy,
+		(lisa-analyzer.github.io), to implement and run static analyzers based on the theory of Abstract Interpretation.
+	</P>
+
+    <H2>Setup</H2>
+
+    <P>If MavenCentral is accessible, the gradle build command will download the requisite LiSA libraries.
+		Otherwise, you should install them and add them to the relevant build paths. Add the Lisa and 
+		Taint plugins to your project in the usual way. (The various analyses are started using the 
+		"default taint query" button in Decompiler.)
+	</P>
+
+    <H2>Options</H2>
+
+	<P>The analysis to run is chosen via the Edit &rarr; ToolOptions, which gives you a default category
+		<B>Abstract Interpretation</B> and two subcategories <B>Abstract Interpretation/Domains</B> and 
+		<B>Abstract Interpretation/Output</B>.  <B>Domains</b> is the most important of these, as it provides the list of available analyses.
+	</P>
+
+	<P>
+ 	 <B>Domains</B> has three options, corresponding to the choice of <B>Heap</B>, <B>Type</B>, and <B>Value</B> domains,
+	 the last being the option you are most likely to want to change.  
+	 </P>
+	  <UL>
+	  <LI><B>Heap<A name="domain_heap"></A></B>: the abstraction used to model the target program's heap.</LI>
+	  <LI><B>Type<A name="domain_type"></A></B>: the abstraction used to model types.</LI>
+	  <LI><B>Value<A name="domain_value"></A></B>: the abstraction used to model values. &larr; </LI>	  
+	  </UL>
+	  <P>
+	  The symbolic state of an analysis is the combination of these domains.
+	</P>
+	
+	<P>
+	 <B>Output</B> has several options (not well-tested), which correspond to fields in the LiSAConfiguration class.
+	 </P>
+	  <UL>
+	  <LI><B>WorkDir<A name="work_dir"></A></B>: the working directory to be used for output if <B>SerializeResults</B> is selected.</LI>
+	  <LI><B>GraphFormat<A name="graph_format"></A></B>: graph format if graph output is desired.</LI>
+	  <LI><B>SerializeResults<A name="serialize"></A></B>: causes the analysis results to be dumped as JSON.</LI>	  
+	  </UL>
+
+	  <P>
+	   <B>Abstract Interpretation</B> (the base option set) has additional execution-related options, associated again with LiSAConfiguration.
+	   </P>
+	    <UL>
+	    <LI><B>CallGraph<A name="call_graph"></A></B>: "Class Hierarchy" or "Rapid Type" analysis of calls.</LI>
+		<LI><B>DescendingPhase<A name="descending_phase"></A></B>: the descending phase applied by the fixpoint algorithm.</LI>
+		<LI><B>Interprocedural<A name="interprocedural"></A></B>: type of interprocedural analysis desired.</LI>
+		<LI><B>OpenCallPolicy<A name="open_call_policy"></A></B>: how to treat unresolved calls.</LI>
+		<LI><B>OptimizeResults<A name="optimize"></A></B>: whether to optimize fixpoint execution.</LI>	  
+		<LI><B>PostState<A name="post_state"></A></B>: evaluate state post- or pre-statement.</LI>	  
+		<LI><B>CallDepth<A name="call_depth"></A></B>: cfg-computation depth (-1 == unlimited).</LI>	  
+		<LI><B>Threshhold<A name="threshhold"></A></B>: applied to either widening or glb.</LI>	  
+	    </UL>
+	  <P>
+		For the most part, these options may be left to their defaults.  However, specific analyses may benefit from different choices.
+	  </P>
+
+	  <H2>Actions</H2>
+
+	  <H3><A name="add_cfgs">Add CFGs</A></H3>
+	  <P>By default, an analysis uses the current function and its callees as the basis for the analysis. Under certain circumstances,
+		you may want to add additional functions to the base. This action generates control-flow graphs for the current function and its
+		descendants without invoking a particular analysis.
+	  </P>
+
+	  <H3><A name="clear_cfgs">Clear CFGs</A></H3>
+	  <P>Successive analyses will add to the set of control-flow graphs under consideration without clearing the previous results.
+		To clear previous CFGs, you must explicitly do so. This action removes all active CFGs.
+	  </P>
+
+	  <H3><A name="set_taint">Set Taint</A></H3>
+	  <P>For the "Taint" and "ThreeLevelTaint" analyses, you will need to specify sources of taint. There are two ways to do this.
+		From the decompiler, you may use the normal taint analysis functions (or this action) to specify <B>SOURCES</B> of taint. 
+		(<B>SINKS</B> and <B>GATES</B> may also be used, but be aware they currently correspond only to "clean" annotations in LiSA.)  
+		Alternatively, from the disassembly view, you may use this action on a line of PCode to mark an input to the op, or on a line
+		of disassembly to get a dialog for entering the varnode ID by hand.  The varnode should be specified using its address, e.g.
+		"register:00000000" for RAX.
+	  </P>
+
+	  <P>Using either method may be imprecise. In particular, the analysis currently uses the low PCode, so tokens selected in the
+		decompiler (high PCode) may or may not have an equivalent. Similarly, varnodes marked in the disassembly are inputs only.
+		Marking an input as a source does not mark it as tainted in the analysis' state.  In most cases, the resulting output will 
+		be tainted, but not future references to the input, e.g. "(unique:5) INT_ADD (register:4), 0x12" taints future references 
+		to (unique:5) but not to (register:4).
+	  </P>
+
+	  <H2>Current Analyses (Value Domains)</H2>
+	  <UL>
+		<LI><B>Numeric: Constant Propagation</B>: overflow-insensitive basic constant propagation.</LI>
+		<LI><B>Numeric: Interval</B>: approximating numeric values as the minimum interval containing them.</LI>
+		<LI><B>Numeric: Non-redundant Power Sets Of Intervals</B>: approximating numeric values as a non-redundant set of intervals.</LI>
+		<LI><B>Numeric: Parity</B>: tracking whether numeric values are even or odd.</LI>
+		<LI><B>Numeric: Pentagon</B>: capturing properties of the form of x in [a, b] &and; x &lt; y.</LI>
+		<LI><B>Numeric: Sign</B>: tracking zero, strictly positive and strictly negative values.</LI>
+		<LI><B>Numeric: Upper Bound</B>: capturing upper bounds on a variable.</LI>
+		<LI><B>Dataflow: Available Expressions</B>: expressions stored in some variable.</LI>
+		<LI><B>Dataflow: Constant Propagation</B>: overflow-insensitive basic constant propagation.</LI>
+		<LI><B>Dataflow: Reaching Definitions</B>: instruction whose targets reach the given one without an intervening assignment.</LI>
+		<LI><B>Dataflow: Liveness</B>: variables that are live at each point in the program.
+			 NB: typically uses the BackwardModularWorstCase interprocedural analysis.</LI>
+		<LI><B>Dataflow: Taint</B>: two levels of taintedness - clean and tainted. See above re setting taint.</LI>
+		<LI><B>Dataflow: Three-level Taint</B>: three levels of taintedness - clean, tainted, and top. See above re setting taint.</LI>
+		<LI><B>Non-interference</B>: type-system based implementation of non-interference analysis.</LI>
+		<LI><B>Stability</B>: per-variable numerical trends.</LI>
+	  </UL>
+	  <P>Note: with the exception of reaching, liveness, and non-interference domains, these domains have been extended (to a greater or lesser extent)
+		to handle p-code. Modifications may not be in sync with the latest domain definitions in the original LiSA analysis archive.
+	  </P>
+
+	  <H2>Results</H2>
+	
+	  <P>Results are passed, by default, via SARIF to a results table. The functionality of the table is described in more detail
+		in <A href="help/topics/DecompilerTaint/DecompilerTaint.html#ResultMenuActions">Decompiler Taint Operations</A>. In general, you'll want to enable the "name", "type", "value",
+		and "displayName" columns, as well as "Address" and possibly "location".
+	  </P>
+  </BODY>
+</HTML>

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

@@ -0,0 +1,39 @@
+/* ###
+ * 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.gui;
+
+import ghidra.lisa.gui.LisaTaintState.KTV;
+import ghidra.program.model.data.ISF.AbstractIsfWriter.Exclude;
+import ghidra.program.model.data.ISF.IsfObject;
+
+public class ExtKeyValue implements IsfObject {
+
+	String name;
+	String displayName;
+	String type;
+	String taintLabels;
+
+	@Exclude
+	private int index;
+
+	public ExtKeyValue(KTV ktv) {
+		this.name = ktv.key();
+		this.displayName = ktv.displayName();
+		this.type = ktv.type();
+		this.taintLabels = "[" + ktv.value() + "]";
+	}
+
+}

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

@@ -0,0 +1,484 @@
+/* ###
+ * 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.gui;
+
+import java.util.*;
+
+import db.Transaction;
+import docking.action.builder.ActionBuilder;
+import ghidra.GhidraOptions;
+import ghidra.app.CorePluginPackage;
+import ghidra.app.context.ProgramLocationActionContext;
+import ghidra.app.decompiler.ClangToken;
+import ghidra.app.decompiler.location.DefaultDecompilerLocation;
+import ghidra.app.events.*;
+import ghidra.app.plugin.PluginCategoryNames;
+import ghidra.app.plugin.ProgramPlugin;
+import ghidra.app.plugin.core.decompiler.absint.AbstractInterpretationService;
+import ghidra.app.plugin.core.decompiler.taint.*;
+import ghidra.app.plugin.core.decompiler.taint.TaintState.MarkType;
+import ghidra.app.script.AskDialog;
+import ghidra.framework.options.OptionsChangeListener;
+import ghidra.framework.options.ToolOptions;
+import ghidra.framework.plugintool.*;
+import ghidra.framework.plugintool.util.PluginStatus;
+import ghidra.lisa.gui.LisaOptions.*;
+import ghidra.lisa.pcode.PcodeFrontend;
+import ghidra.program.database.SpecExtension;
+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.util.PcodeFieldLocation;
+import ghidra.program.util.ProgramLocation;
+import ghidra.util.HelpLocation;
+import ghidra.util.Msg;
+import ghidra.util.exception.CancelledException;
+import ghidra.util.task.DummyCancellableTaskMonitor;
+import ghidra.util.task.TaskMonitor;
+import it.unive.lisa.*;
+import it.unive.lisa.interprocedural.InterproceduralAnalysis;
+import it.unive.lisa.program.cfg.CFG;
+import it.unive.lisa.program.cfg.statement.Statement;
+
+/**
+ * Plugin for tracking taint through the decompiler.
+ */
+//@formatter:off
+@PluginInfo(
+	status = PluginStatus.UNSTABLE,
+	packageName = CorePluginPackage.NAME,
+	category = PluginCategoryNames.ANALYSIS,
+	shortDescription = "LisaTest",
+	description = "Plugin for abstract interpretation analysis via LiSA",
+	servicesProvided = { AbstractInterpretationService.class },
+	servicesRequired = {
+		TaintService.class,
+	},
+	eventsConsumed = {
+		ProgramActivatedPluginEvent.class, ProgramOpenedPluginEvent.class,
+		ProgramLocationPluginEvent.class, ProgramSelectionPluginEvent.class,
+		ProgramClosedPluginEvent.class
+	})
+//@formatter:on
+
+public class LisaPlugin extends ProgramPlugin implements OptionsChangeListener, AbstractInterpretationService {
+	
+	private static final String OPTIONS_TITLE = "Abstract Interpretation";
+	public HeapDomainOption heapOption = HeapDomainOption.DEFAULT;
+	public TypeDomainOption typeOption = TypeDomainOption.DEFAULT;
+	public ValueDomainOption valueOption = ValueDomainOption.DEFAULT;
+
+	private Function currentFunction;
+
+	private InterproceduralAnalysis<?> ipa;
+	private PcodeFrontend frontend;
+	private LiSA lisa;
+
+	private LisaOptions options;
+	private TaintPlugin taintPlugin;
+	private LisaTaintState taintState;
+	private TaskMonitor monitor = TaskMonitor.DUMMY;
+	private String lastValue = "";
+
+	public LisaPlugin(PluginTool tool) {
+		super(tool);
+		setOptions(new LisaOptions());
+		createActions();
+	}
+
+	public Function getCurrentFunction() {
+		return currentFunction;
+	}
+
+	@Override
+	protected void programActivated(Program program) {
+		currentProgram = program;
+		initOptions();
+	}
+
+
+	public interface AddCfgsAction {
+		String NAME = "Add CFG";
+		String DESCRIPTION = "Compute called CFGs prior to analysis";
+		String HELP_ANCHOR = "add_cfgs";
+
+		static ActionBuilder builder(Plugin owner) {
+			String ownerName = owner.getName();
+			return new ActionBuilder(NAME, ownerName)
+					.description(DESCRIPTION)
+					.popupMenuPath("Abstract Interpretation", NAME)
+					.helpLocation(new HelpLocation(ownerName, HELP_ANCHOR));
+		}
+	}
+
+	public interface ClearCfgsAction {
+		String NAME = "Clear CFGs";
+		String DESCRIPTION = "Clear CFGs prior to analysis";
+		String HELP_ANCHOR = "clear_cfgs";
+
+		static ActionBuilder builder(Plugin owner) {
+			String ownerName = owner.getName();
+			return new ActionBuilder(NAME, ownerName)
+					.description(DESCRIPTION)
+					.popupMenuPath("Abstract Interpretation", NAME)
+					.helpLocation(new HelpLocation(ownerName, HELP_ANCHOR));
+		}
+	}
+
+	public interface SetTaintAction {
+		String NAME = "Set Taint";
+		String DESCRIPTION = "Set taint for given varnode";
+		String HELP_ANCHOR = "set_taint";
+
+		static ActionBuilder builder(Plugin owner) {
+			String ownerName = owner.getName();
+			return new ActionBuilder(NAME, ownerName)
+					.description(DESCRIPTION)
+					.popupMenuPath("Abstract Interpretation", NAME)
+					.helpLocation(new HelpLocation(ownerName, HELP_ANCHOR));
+		}
+	}
+
+
+	private void createActions() {
+
+		AddCfgsAction.builder(this)
+			.withContext(ProgramLocationActionContext.class)
+			.onAction(this::addCfgs)
+			.buildAndInstall(tool);
+		
+		ClearCfgsAction.builder(this)
+		.withContext(ProgramLocationActionContext.class)
+		.onAction(this::clearCfgs)
+		.buildAndInstall(tool);
+
+		SetTaintAction.builder(this)
+		.withContext(ProgramLocationActionContext.class)
+		.onAction(this::setTaint)
+		.buildAndInstall(tool);
+
+	}
+
+
+	@Override
+	public Program getCurrentProgram() {
+		return currentProgram;
+	}
+
+	@Override
+	public void processEvent(PluginEvent event) {
+		super.processEvent(event);
+
+		//Msg.info(this, "TaintPlugin -> processEvent: " + event.toString() );
+
+		if (event instanceof ProgramClosedPluginEvent closedEvent) {
+			Program program = closedEvent.getProgram();
+			if (currentProgram != null && currentProgram.equals(program)) {
+				currentProgram = null;
+			}
+			return;
+		}
+
+
+		if (event instanceof ProgramActivatedPluginEvent activatedEvent) {
+			currentProgram = activatedEvent.getActiveProgram();
+			if (currentProgram != null) {
+				SpecExtension.registerOptions(currentProgram);
+			}
+
+		}
+		else if (event instanceof ProgramLocationPluginEvent locEvent) {
+
+			// user changed their location in the program; this may be a function change.
+
+			ProgramLocation location = locEvent.getLocation();
+			Address address = location.getAddress();
+
+			if (address.isExternalAddress()) {
+				// ignore external functions when it comes to taint.
+				return;
+			}
+
+			if (currentProgram != null) {
+				// The user loaded a program for analysis.
+				Listing listing = currentProgram.getListing();
+				Function f = listing.getFunctionContaining(address);
+				// We are in function f
+				if (currentFunction == null || !currentFunction.equals(f)) {
+					// In the PAST we were in a function and the program location moved us into a new function.
+					String cfun = "NULL";
+					String nfun = "NULL";
+
+					if (currentFunction != null) {
+						cfun = currentFunction.getEntryPoint().toString();
+					}
+
+					if (f != null) {
+						nfun = f.getEntryPoint().toString();
+					}
+
+					Msg.info(this, "Changed from function: " + cfun + " to function " + nfun);
+					currentFunction = f;
+				}
+			}
+		}
+	}
+
+	private void addCfgs(ProgramLocationActionContext context) {
+		Set<CFG> cfgs = new HashSet<>();
+		Address addr = context.getAddress();
+		FunctionManager functionManager = currentProgram.getFunctionManager();
+		Function f = functionManager.getFunctionContaining(addr);
+		addCfg(cfgs, f, true);
+	}
+	
+	private void addCfg(Set<CFG> cfgs, Function f, boolean recurse) {
+		if (frontend == null) {
+			initProgram();
+		}
+		int depth = recurse ? getOptions().getCfgDepth() : 0;
+		addFunction(cfgs, f);
+		addCalledFunctions(cfgs, f, depth);
+		
+		it.unive.lisa.program.Program p = frontend.getProgram();
+		Collection<CFG> baseline = p.getAllCFGs();
+		for (CFG g : cfgs) {
+			if (baseline.contains(g)) {
+				p.addEntryPoint(g);
+			}
+		}
+	}
+
+	private void addFunction(Set<CFG> cfgs, Function f) {
+		if (frontend.hasProcessed(f) || monitor.isCancelled()) {
+			return;
+		}
+		Msg.info(this, "Adding "+f);
+		CFG cfg = frontend.visitFunction(f, f.getEntryPoint());
+		cfgs.add(cfg);
+	}
+
+	private void addCalledFunctions(Set<CFG> cfgs, Function f, int depth) {
+		if (depth == 0 || frontend.hasProcessed(f) || monitor.isCancelled()) {
+			return;
+		}
+		Set<Function> calledFunctions = f.getCalledFunctions(new DummyCancellableTaskMonitor());
+		for (Function func : calledFunctions) {
+			Address entryPoint = func.getEntryPoint();
+			if (entryPoint.getAddressSpace().equals(f.getEntryPoint().getAddressSpace())) {
+				addFunction(cfgs, func);
+				addCalledFunctions(cfgs, func, depth-1);
+			}
+		}
+	}
+	
+	private void clearCfgs(ProgramLocationActionContext context) {
+		initProgram();
+		frontend.clearTargets();
+	}
+	
+	private void setTaint(ProgramLocationActionContext context) {
+		if (!checkTaintState()) {
+			return;
+		}
+		taintState.clearAnnotations();
+		BookmarkManager bookmarkManager = currentProgram.getBookmarkManager();
+		try (Transaction tx = currentProgram.openTransaction("clear bookmark")) {
+			bookmarkManager.removeBookmarks(BookmarkType.INFO, "Taint Source", TaskMonitor.DUMMY);
+		}
+		catch (CancelledException e) {
+			throw new AssertionError("Unreachable code");
+		}
+		Address addr = context.getAddress();
+		FunctionManager functionManager = currentProgram.getFunctionManager();
+		Function f = functionManager.getFunctionContaining(addr);
+		ProgramLocation location = context.getLocation();
+		int row = location.getRow();
+		int offset = location.getCharOffset();
+		
+		String tokenId = null;
+		if (location instanceof PcodeFieldLocation pfl) {
+			List<String> pcodeStrings = pfl.getPcodeStrings();
+			String test = pcodeStrings.get(row);
+			int lastSpace= test.lastIndexOf(" ");
+			int index = offset > lastSpace ? 1 : 0;
+			Instruction inst = currentProgram.getListing().getInstructionContaining(addr);
+			PcodeOp[] pcode = inst.getPcode();
+			PcodeOp op = pcode[row];
+			if (index >= op.getNumInputs()) {
+				index--;
+			}
+			Varnode vn = op.getInput(index);
+			tokenId = vn.getAddress().toString();
+		}
+		else if (location instanceof DefaultDecompilerLocation ddl) {
+			ClangToken token = ddl.getToken();
+			taintPlugin.toggleIcon(MarkType.SOURCE, token, false);
+			return;  // taint is set via the token
+		}
+		else {
+			AskDialog<String> dialog = new AskDialog<>("Abstract Interpretation Taint", "Varnode address", AskDialog.STRING, lastValue);
+			if (dialog.isCanceled()) {
+				return;
+			}
+			tokenId = dialog.getValueAsString();
+		}
+		try (Transaction tx = currentProgram.openTransaction("set bookmark")) {
+			bookmarkManager.setBookmark(addr, BookmarkType.INFO, "Taint Source", tokenId);
+		}
+		taintState.setTaint(MarkType.SOURCE, f, addr, tokenId);
+	}
+	
+	private boolean checkTaintState() {
+		if (taintState == null) {
+			// ability to add custom margins to the decompiler view
+			TaintService service = tool.getService(TaintService.class);
+			if (service instanceof TaintPlugin taint) {
+				this.taintPlugin = taint;
+				TaintState state = taint.getTaintState();
+				if (state instanceof LisaTaintState ts) {
+					this.taintState = ts;
+					return true;
+				}
+			}
+		}
+		else {
+			return true;
+		}
+		return false;
+	}
+
+	public Map<Function, Collection<?>> performAnalysis(TaskMonitor tm) {
+		this.monitor = tm;
+		if (currentFunction == null) {
+			Msg.error(this, "Not currently in a function");
+			return null;
+		}
+		try {
+			addCfg(new HashSet<>(), currentFunction, true);
+			initLisa();
+			it.unive.lisa.program.Program p = frontend.getProgram();
+			Map<Function, Collection<?>> combined = new HashMap<>();
+			if (monitor.isCancelled()) {
+				return combined;
+			}
+			LiSAReport report = lisa.run(p);
+			ipa = report.getConfiguration().interproceduralAnalysis;
+			
+			FunctionManager functionManager = currentProgram.getFunctionManager();
+			Map<Address, CFG> targets = frontend.getTargets();
+			for (Address entry : targets.keySet()) {
+				if (monitor.isCancelled()) {
+					break;
+				}
+				Function f = functionManager.getFunctionAt(entry);
+				CFG cfg = targets.get(entry);
+				Collection<?> res = ipa.getAnalysisResultsOf(cfg);
+				combined.put(f, res);
+			}
+			return combined;
+		} catch (AnalysisException e) {
+			Msg.error(this, e.getMessage());
+		}
+		return null;
+	}
+	
+	public Collection<Statement> getStatements(Function f) {
+		addCfg(new HashSet<>(), f, false);
+		CFG cfg = frontend.getTarget(f.getEntryPoint());
+		return cfg.getNodes();
+	}
+
+	private void initProgram() {
+		frontend = new PcodeFrontend();
+	}
+	
+	@SuppressWarnings("unchecked")
+	private void initLisa() {
+		LisaOptions opt = getOptions();
+		heapOption = opt.getHeapOption();
+		typeOption = opt.getTypeOption();
+		valueOption = opt.getValueOption();
+		
+		DefaultConfiguration conf = new DefaultConfiguration();
+		conf.abstractState = DefaultConfiguration.simpleState(
+				heapOption.getDomain(),
+				valueOption.getDomain(currentProgram),
+				typeOption.getDomain());
+		conf.interproceduralAnalysis = opt.getInterproceduralOption().getAnalysis();
+		conf.descendingPhaseType = opt.getDescendingPhaseOption().getType();
+		conf.openCallPolicy = opt.getCallOption().getPolicy();
+		conf.analysisGraphs = opt.getGraphOption().getType();
+		conf.callGraph = opt.getCallGraphOption().getCallGraph();
+		conf.serializeResults = opt.isSerialize();
+		conf.optimize = opt.isOptimize();
+		String outputDir = opt.getOutputDir();
+		if (!outputDir.equals(LisaOptions.DEFAULT_LISA_ANALYSIS_OUTDIR)) {
+			conf.workdir = outputDir;
+		}
+
+		lisa = new LiSA(conf);
+	}
+
+	private void initOptions() {
+		ToolOptions opt = tool.getOptions(OPTIONS_TITLE);
+		getOptions().registerOptions(this, opt, currentProgram);
+
+		opt.addOptionsChangeListener(this);
+
+		ToolOptions codeBrowserOptions = tool.getOptions(GhidraOptions.CATEGORY_BROWSER_FIELDS);
+		codeBrowserOptions.addOptionsChangeListener(this);
+	}
+	
+	@Override
+	public void optionsChanged(ToolOptions opts, String optionName, Object oldValue,
+			Object newValue) {
+		if (opts.getName().equals(OPTIONS_TITLE) ||
+			opts.getName().equals(GhidraOptions.CATEGORY_BROWSER_FIELDS)) {
+			doRefresh();
+		}
+	}
+
+	private void doRefresh() {
+		ToolOptions opt = tool.getOptions(OPTIONS_TITLE);
+		getOptions().grabFromToolAndProgram(this, opt, currentProgram);
+	}
+	
+	@Override
+	public String getActiveQueryName() {
+		String queryName = valueOption.toString();
+		if (!heapOption.equals(HeapDomainOption.DEFAULT)) {
+			queryName += ":"+heapOption.toString();
+		}
+		if (!typeOption.equals(TypeDomainOption.DEFAULT)) {
+			queryName += ":"+typeOption.toString();
+		}
+		if (currentFunction != null) {
+			queryName += " @ " + currentFunction;
+		}
+		return queryName;
+	}
+
+	public LisaOptions getOptions() {
+		return options;
+	}
+
+	public void setOptions(LisaOptions options) {
+		this.options = options;
+	}
+
+}

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

@@ -0,0 +1,50 @@
+/* ###
+ * 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.gui;
+
+import java.io.IOException;
+
+import ghidra.lisa.gui.LisaTaintState.KTV;
+import ghidra.util.exception.CancelledException;
+import ghidra.util.task.TaskMonitor;
+import sarif.export.*;
+
+public class SarifKeyValueWriter extends AbstractExtWriter {
+
+	private ExtKeyValue isf;
+	private WrappedLogicalLocation wll;
+
+	public SarifKeyValueWriter(KTV ktv, WrappedLogicalLocation wll)
+			throws IOException {
+		super(null);
+		this.isf = new ExtKeyValue(ktv);
+		this.wll = wll;
+	}
+
+	@Override
+	protected void genRoot(TaskMonitor monitor) throws CancelledException, IOException {
+		genData(monitor);
+		root.add("structuredObject", objects);
+	}
+
+	private void genData(TaskMonitor monitor) {
+		ExtLogicalLocation lloc = wll.getLogicalLocation();
+		SarifObject sarif = new SarifObject(lloc.getDecoratedName(), "VALUE", lloc, getTree(isf),
+			wll.getAddress(), wll.getIndex());
+		objects.add(getTree(sarif));
+	}
+
+}

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

@@ -0,0 +1,76 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.gui;
+
+import java.io.IOException;
+
+import ghidra.lisa.pcode.locations.InstLocation;
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.program.model.address.Address;
+import ghidra.program.model.listing.Function;
+import ghidra.program.model.pcode.SequenceNumber;
+import ghidra.util.exception.CancelledException;
+import ghidra.util.task.TaskMonitor;
+import it.unive.lisa.program.cfg.statement.Statement;
+import sarif.export.*;
+
+public class SarifLogicalLocationWriter extends AbstractExtWriter {
+
+	private PcodeLocation location;
+
+	private WrappedLogicalLocation lloc;
+
+	public SarifLogicalLocationWriter(String key, Function f, Statement statement)
+			throws IOException {
+		super(null);
+		Address addr;
+		String loc, op;
+		if (statement.getLocation() instanceof PcodeLocation ploc) {
+			this.location = ploc;
+			SequenceNumber seqnum = location.op.getSeqnum();
+			String seq = seqnum.getTarget() + ":" + seqnum.getTime();
+			loc = f.getName();
+			loc += "@" + f.getEntryPoint();
+			loc += ":" + seq;
+			addr = location.getAddress();
+			op = seq + " " + location.op.toString();
+		}
+		else {
+			loc = f.getName();
+			InstLocation instLoc = (InstLocation) statement.getLocation();
+			addr = instLoc.getAddress();
+			loc += "@" + addr;
+			op = instLoc.toString();
+		}
+		ExtLogicalLocation ext = new ExtLogicalLocation(key, f, loc, op);
+		lloc = new WrappedLogicalLocation(ext, addr);
+	}
+
+	@Override
+	protected void genRoot(TaskMonitor monitor) throws CancelledException, IOException {
+		genData(monitor);
+		root.add("logicalLocation", objects);
+	}
+
+	private void genData(TaskMonitor monitor) {
+		objects.add(getTree(lloc.getLogicalLocation()));
+	}
+
+	public WrappedLogicalLocation getLogicalLocation() {
+		return lloc;
+	}
+
+}

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

@@ -0,0 +1,87 @@
+/* ###
+ * 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;
+
+import java.util.*;
+
+import ghidra.lisa.pcode.WorkItem.PredType;
+import it.unive.lisa.program.cfg.CFG;
+import it.unive.lisa.program.cfg.controlFlow.ControlFlowStructure;
+import it.unive.lisa.program.cfg.edge.Edge;
+import it.unive.lisa.program.cfg.statement.Statement;
+import it.unive.lisa.util.datastructures.graph.code.NodeList;
+
+public class PcodeBranch extends ControlFlowStructure {
+
+	private Statement branch;
+	private Statement fallThrough;
+
+	protected PcodeBranch(NodeList<CFG, Statement, Edge> cfgMatrix, Statement condition) {
+		super(cfgMatrix, condition, null);
+	}
+
+	@Override
+	protected Collection<Statement> bodyStatements() {
+		Collection<Statement> all = new HashSet<>(getTrueBranch());
+		all.addAll(getFalseBranch());
+		return all;
+	}
+
+	private Collection<Statement> getFalseBranch() {
+		if (fallThrough == null) {
+			return Set.of();
+		}
+		return new HashSet<>(cfgMatrix.followersOf(fallThrough));
+	}
+
+	private Collection<Statement> getTrueBranch() {
+		if (branch == null) {
+			return Set.of();
+		}
+		return new HashSet<>(cfgMatrix.followersOf(branch));
+	}
+
+	@Override
+	public boolean contains(Statement st) {
+		return bodyStatements().contains(st);
+	}
+
+	@Override
+	public void simplify() {
+		// Nothing required here
+	}
+
+	@Override
+	public String toString() {
+		return "if-then-else[" + getCondition() + "]";
+	}
+
+	@Override
+	public Collection<Statement> getTargetedStatements() {
+		return bodyStatements();
+	}
+
+	public void addStatement(Statement st, PredType type) {
+		if (type.equals(PredType.TRUE)) {
+			branch = st;
+		}
+		else {
+			fallThrough = st;
+			setFirstFollower(st);
+		}
+	}
+
+}

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

@@ -0,0 +1,391 @@
+/* ###
+ * 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;
+
+import java.util.*;
+
+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.statements.PcodeNop;
+import ghidra.program.model.listing.Listing;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.program.model.pcode.SequenceNumber;
+import it.unive.lisa.program.annotations.Annotations;
+import it.unive.lisa.program.cfg.*;
+import it.unive.lisa.program.cfg.controlFlow.ControlFlowStructure;
+import it.unive.lisa.program.cfg.edge.Edge;
+import it.unive.lisa.program.cfg.edge.SequentialEdge;
+import it.unive.lisa.program.cfg.statement.*;
+import it.unive.lisa.program.cfg.statement.comparison.Equal;
+import it.unive.lisa.program.cfg.statement.literal.*;
+import it.unive.lisa.program.type.BoolType;
+import it.unive.lisa.type.Type;
+import it.unive.lisa.type.Untyped;
+import it.unive.lisa.util.datastructures.graph.code.NodeList;
+
+/**
+ * An {@link PcodeCodeMemberVisitor} that will parse the pcode of an function
+ * 
+ */
+
+public class PcodeCodeMemberVisitor {
+
+	private final NodeList<CFG, Statement, Edge> list;
+
+	private final Collection<Statement> entrypoints;
+	private final Collection<ControlFlowStructure> cfs;
+	private final Map<String, Pair<VariableRef, Annotations>> visibleIds;
+
+	private final CFG cfg;
+
+	private final CodeMemberDescriptor descriptor;
+
+	private Listing listing;
+
+	private final Collection<String> visited;
+	private final Map<SequenceNumber, Statement> visitedPcode;
+	private Stack<WorkItem> workItems;
+
+	private UnitContext currentUnit;
+
+	private Map<String, PcodeBranch> flows;
+
+	private int varCount = 0;
+
+	/**
+	 * Builds the visitor of an IMP method or constructor.
+	 * 
+	 * @param descriptor the descriptor of the method or constructor
+	 * @param listing    the program listing
+	 */
+	PcodeCodeMemberVisitor(CodeMemberDescriptor descriptor, Listing listing) {
+		this.descriptor = descriptor;
+		this.listing = listing;
+		list = new NodeList<>(new SequentialEdge());
+		entrypoints = new HashSet<>();
+		visited = new HashSet<>();
+		visitedPcode = new HashMap<>();
+		cfs = new LinkedList<>();
+		// side effects on entrypoints and matrix will affect the cfg
+		cfg = new CFG(descriptor, entrypoints, list);
+		this.flows = new HashMap<>();
+
+		visibleIds = new HashMap<>();
+		for (VariableTableEntry par : descriptor.getVariables()) {
+			visibleIds.put(par.getName(), Pair.of(par.createReference(cfg), par.getAnnotations()));
+		}
+	}
+
+	/**
+	 * Visits the code of a {@link UnitContext} representing the code block of
+	 * a method or constructor.
+	 * 
+	 * @param ctx the block context
+	 * 
+	 * @return the {@link CFG} built from the block
+	 */
+	CFG visitCodeMember(UnitContext ctx) {
+		this.currentUnit = ctx;
+		InstructionContext entry = ctx.entry();
+		if (entry == null) {
+			throw new RuntimeException("No entry for " + ctx.function());
+		}
+		while (entry.getPcodeOps().isEmpty()) {
+			entry = entry.next();
+		}
+		visited.clear();
+		visitedPcode.clear();
+		workItems = new Stack<>();
+		workItems.add(new WorkItem(null, entry.getPcodeOp(0)));
+		while (!workItems.isEmpty()) {
+			processWorkItem(workItems.pop());
+		}
+		visitBlock(entry);
+
+		cfs.forEach(cf -> cfg.addControlFlowStructure(cf));
+
+		Ret ret = new Ret(cfg, descriptor.getLocation());
+		if (cfg.getNodesCount() == 0) {
+			// empty method, so the ret is also the entrypoint
+			list.addNode(ret);
+			entrypoints.add(ret);
+		}
+		else {
+			// every non-throwing instruction that does not have a follower
+			// is ending the method
+			Collection<Statement> preExits = new LinkedList<>();
+			for (Statement st : list.getNodes())
+				if (!st.stopsExecution() && list.followersOf(st).isEmpty())
+					preExits.add(st);
+			list.addNode(ret);
+			for (Statement st : preExits)
+				list.addEdge(new SequentialEdge(st, ret));
+
+			for (VariableTableEntry vte : descriptor.getVariables())
+				if (preExits.contains(vte.getScopeEnd()))
+					vte.setScopeEnd(ret);
+		}
+
+		cfg.simplify();
+		return cfg;
+	}
+
+	public void visitBlock(InstructionContext entry) {
+		if (entry == null) {
+			return;
+		}
+		while (entry.getPcodeOps().isEmpty()) {
+			entry = entry.next();
+		}
+		visited.clear();
+		visitedPcode.clear();
+		workItems = new Stack<>();
+		workItems.add(new WorkItem(null, entry.getPcodeOp(0)));
+		while (!workItems.isEmpty()) {
+			processWorkItem(workItems.pop());
+		}
+	}
+
+	private void processWorkItem(WorkItem item) {
+		StatementContext ctx = item.getContext();
+		Statement st = visitPcodeOp(ctx);
+		if (st == null) {
+			return;
+		}
+		if (visited.contains(item.getKey())) {
+			return;
+		}
+		Statement pred = item.getPred();
+		boolean entrypoint = pred == null;
+		cfg.addNode(st, entrypoint);
+		if (!entrypoint) {
+			Edge e = item.computeBranch(st);
+			if (e != null) {
+				cfg.addEdge(e);
+			}
+			PredType type = item.getType();
+			if (!type.equals(PredType.SEQ)) {
+				String loc = pred.getLocation().getCodeLocation();
+				PcodeBranch flow = flows.get(loc);
+				if (flow == null) {
+					flow = new PcodeBranch(cfg.getNodeList(), pred);
+					cfg.addControlFlowStructure(flow);
+				}
+				flow.addStatement(st, type);
+				flows.put(loc, flow);
+			}
+		}
+		else {
+			entrypoints.add(st);
+		}
+		if (st instanceof Ret || st instanceof Return) {
+			return;
+		}
+		List<StatementContext> branches = ctx.branch(this.listing, this.currentUnit);
+		for (StatementContext branch : branches) {
+			WorkItem n = new WorkItem(st, branch);
+			if (ctx.isConditional()) {
+				n.setType(true);
+			}
+			workItems.add(n);
+		}
+		StatementContext next = ctx.next(this.listing);
+		if (next != null) {
+			WorkItem n = new WorkItem(st, next);
+			if (ctx.isBranch()) {
+				if (ctx.isConditional()) {
+					n.setType(false);
+					workItems.add(n);
+				}
+			}
+			else {
+				workItems.add(n);
+			}
+		}
+		visited.add(item.getKey());
+	}
+
+	public Statement visitPcodeOp(StatementContext ctx) {
+		SequenceNumber key = ctx.getOp().getSeqnum();
+		if (visitedPcode.containsKey(key)) {
+			return visitedPcode.get(key);
+		}
+
+		Statement st;
+		if (ctx.isRet()) {
+			if (ctx.expression() != null) {
+				st = new Return(cfg, ctx.location(), visitExpression(ctx));
+			}
+			else {
+				st = new Ret(cfg, ctx.location());
+			}
+		}
+		else if (ctx.isBranch()) {
+			if (ctx.isConditional()) {
+				st = visitCondition(ctx.condition());
+			}
+			else {
+				st = new PcodeNop(cfg, ctx.location());  // Treating these as a NOP
+			}
+		}
+		else if (ctx.expression() != null) {
+			st = visitExpression(ctx);
+		}
+		else
+			throw new IllegalArgumentException(
+				"Statement '" + ctx.toString() + "' cannot be parsed");
+
+		visitedPcode.put(key, st);
+		return st;
+	}
+
+	public Statement visitCondition(
+			ConditionContext ctx) {
+		VarnodeContext expression = ctx.expression();
+		CodeLocation loc = ctx.location();
+		if (expression == null) {
+			return new NoOp(cfg, loc);
+		}
+		//return visitVarnode(ctx.location(), expression, BoolType.INSTANCE, false);
+		Expression left = visitVarnode(loc, expression, BoolType.INSTANCE, false);
+		return new Equal(cfg, loc, left, new TrueLiteral(cfg, loc));
+	}
+
+	public Expression visitExpression(StatementContext ctx) {
+		CodeLocation loc = ctx.location();
+		VarDefContext left = ctx.target();
+		PcodeContext right = ctx.expression();
+
+		int opcode = ctx.opcode();
+		switch (opcode) {
+			case PcodeOp.COPY -> {
+				Expression target = visitVariable(loc, left, true);
+				Expression expression = visitVarnode(loc, right.basicExpr(), false);
+				return new Assignment(cfg, loc, target, expression);
+			}
+			case PcodeOp.FLOAT_INT2FLOAT, PcodeOp.FLOAT_FLOAT2FLOAT -> {
+				Expression target = visitVariable(loc, left, true);
+				Expression expression = visitBinaryExpr(new BinaryExprContext(ctx));
+				return new Assignment(cfg, loc, target, expression);
+			}
+			case PcodeOp.CALL, PcodeOp.CALLIND, PcodeOp.CALLOTHER -> {
+				return visitCallExpr(new CallContext(ctx.getOp(), currentUnit));
+			}
+			case PcodeOp.RETURN -> {
+				return visitVarnode(loc, right.basicExpr(), false);
+			}
+			case PcodeOp.LOAD -> {
+				MemLocContext mem = new MemLocContext(ctx);
+				Expression target = visitVariable(loc, left, true);
+				Expression expression = visitVarnode(loc, mem, false);
+				return new Assignment(cfg, loc, target, expression);
+			}
+			case PcodeOp.STORE -> {
+				MemLocContext mem = new MemLocContext(ctx);
+				Expression target = visitVariable(loc, mem, true);
+				Expression expression = visitVarnode(loc, left, false);
+				return new Assignment(cfg, loc, target, expression);
+			}
+		}
+
+		if (right == null) {
+			throw new UnsupportedOperationException("Type of expression not supported: " + ctx);
+		}
+
+		return switch (right.getNumInputs()) {
+			case 1 -> {
+				Expression target = visitVariable(loc, left, true);
+				Expression expression = visitUnaryExpr(new UnaryExprContext(right));
+				yield new Assignment(cfg, loc, target, expression);
+			}
+			case 2 -> {
+				Expression target = visitVariable(loc, left, true);
+				Expression expression = visitBinaryExpr(new BinaryExprContext(right));
+				yield new Assignment(cfg, loc, target, expression);
+			}
+			default -> throw new UnsupportedOperationException(
+				"Type of expression not supported: " + ctx);
+		};
+	}
+
+	public Expression visitCallExpr(CallContext ctx) {
+		CodeLocation loc = ctx.location();
+		Expression lexp = visitVarnode(loc, ctx.left, false);
+		return new PcodeCallExpression(cfg, ctx, lexp);
+	}
+
+	public Expression visitUnaryExpr(UnaryExprContext ctx) {
+		CodeLocation loc = ctx.location();
+		Expression lexp = visitVarnode(loc, ctx.arg, false);
+		return new PcodeUnaryExpression(cfg, ctx, lexp);
+	}
+
+	public Expression visitBinaryExpr(BinaryExprContext ctx) {
+		CodeLocation loc = ctx.location();
+		Expression lexp = visitVariable(loc, ctx.left, false);
+		Expression rexp = visitVarnode(loc, ctx.right, false);
+		return new PcodeBinaryExpression(cfg, ctx, lexp, rexp);
+	}
+
+	public Expression visitVarnode(CodeLocation loc, VarnodeContext ctx, Type type,
+			boolean define) {
+		if (ctx.isConstant()) {
+			return visitConstant(loc, ctx);
+		}
+		return visitVariable(loc, ctx, type, define);
+	}
+
+	public Expression visitVarnode(CodeLocation loc, VarnodeContext ctx, boolean define) {
+		return visitVarnode(loc, ctx, Untyped.INSTANCE, define);
+	}
+
+	public Literal<?> visitConstant(CodeLocation loc, VarnodeContext ctx) {
+		return switch (ctx.getSize()) {
+			case 0 -> new NullLiteral(cfg, loc);
+			case 1 -> new Int8Literal(cfg, loc, (byte) ctx.getOffset());
+			case 2 -> new Int16Literal(cfg, loc, (short) ctx.getOffset());
+			case 4 -> new Int32Literal(cfg, loc, (int) ctx.getOffset());
+			case 8 -> new Int64Literal(cfg, loc, ctx.getOffset());
+			default -> new Int64Literal(cfg, loc, ctx.getOffset());  // FIXME
+//			default -> throw new UnsupportedOperationException(
+//				"Type of literal not supported: " + ctx);
+		};
+	}
+
+	private VariableRef visitVariable(CodeLocation loc, VarnodeContext ctx, boolean define) {
+		return visitVariable(loc, ctx, Untyped.INSTANCE, define);
+	}
+
+	private VariableRef visitVariable(CodeLocation loc, VarnodeContext ctx, Type type,
+			boolean define) {
+		VariableRef ref = new VariableRef(cfg, loc,
+			ctx.getText(), type);
+		if (!visibleIds.containsKey(ref.getName())) {
+			visibleIds.put(ref.getName(), Pair.of(ref, new Annotations()));
+			descriptor.addVariable(new VariableTableEntry(loc, varCount++, null, null,
+				ref.getName(), type));
+		}
+		return ref;
+	}
+
+	public Map<String, PcodeBranch> getFlows() {
+		return flows;
+	}
+
+}

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

@@ -0,0 +1,55 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.pcode;
+
+import it.unive.lisa.program.language.LanguageFeatures;
+import it.unive.lisa.program.language.hierarchytraversal.HierarcyTraversalStrategy;
+import it.unive.lisa.program.language.hierarchytraversal.SingleInheritanceTraversalStrategy;
+import it.unive.lisa.program.language.parameterassignment.ParameterAssigningStrategy;
+import it.unive.lisa.program.language.parameterassignment.PythonLikeAssigningStrategy;
+import it.unive.lisa.program.language.resolution.JavaLikeMatchingStrategy;
+import it.unive.lisa.program.language.resolution.ParameterMatchingStrategy;
+import it.unive.lisa.program.language.validation.BaseValidationLogic;
+import it.unive.lisa.program.language.validation.ProgramValidationLogic;
+
+/**
+ * Pcode's {@link LanguageFeatures} implementation.
+ * 
+ */
+public class PcodeFeatures extends LanguageFeatures {
+
+	// For the PcodeFrontend, most of the strategies are probably not relevant.
+
+	@Override
+	public ParameterMatchingStrategy getMatchingStrategy() {
+		return JavaLikeMatchingStrategy.INSTANCE;
+	}
+
+	@Override
+	public HierarcyTraversalStrategy getTraversalStrategy() {
+		return SingleInheritanceTraversalStrategy.INSTANCE;
+	}
+
+	@Override
+	public ParameterAssigningStrategy getAssigningStrategy() {
+		return PythonLikeAssigningStrategy.INSTANCE;
+	}
+
+	@Override
+	public ProgramValidationLogic getProgramValidationLogic() {
+		return new BaseValidationLogic();
+	}
+}

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

@@ -0,0 +1,159 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.pcode;
+
+import java.util.*;
+
+import ghidra.lisa.pcode.contexts.UnitContext;
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.lisa.pcode.types.PcodeTypeSystem;
+import ghidra.program.model.address.Address;
+import ghidra.program.model.lang.Register;
+import ghidra.program.model.lang.RegisterValue;
+import ghidra.program.model.listing.*;
+import it.unive.lisa.program.Program;
+import it.unive.lisa.program.cfg.*;
+import it.unive.lisa.program.cfg.Parameter;
+import it.unive.lisa.program.cfg.statement.Statement;
+import it.unive.lisa.type.Untyped;
+
+/**
+ * Instantiated {@link PcodeCodeMemberVisitor} that will parse the pcode building a
+ * representation that can be analyzed through LiSA.
+ */
+public class PcodeFrontend {
+
+	//private static final Logger log = LogManager.getLogger(PcodeFrontend.class);
+
+	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() {
+		program = new Program(new PcodeFeatures(), new PcodeTypeSystem());
+	}
+
+	public Program doWork(Listing listing, Address startAddress) {
+
+		Program p = visitListing(listing, startAddress);
+
+		Collection<CFG> baseline = p.getAllCFGs();
+		for (CFG cfg : cfgs) {
+			if (baseline.contains(cfg)) {
+				p.addEntryPoint(cfg);
+			}
+		}
+		return p;
+	}
+
+	public Program visitListing(Listing listing, Address startAddress) {
+		Program p = getProgram();
+		for (Function f : listing.getFunctions(startAddress, false)) {
+			CFG cfg = visitFunction(f, startAddress);
+			cfgs.add(cfg);
+		}
+		return p;
+	}
+
+	public CFG visitFunction(Function f, Address start) {
+		Program p = getProgram();
+		UnitContext ctx = new UnitContext(this, program, f, start);
+
+		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);
+		}
+		return cfg;
+	}
+
+	private Address toAddr(CodeLocation location) {
+		if (location instanceof PcodeLocation loc) {
+			return loc.op.getSeqnum().getTarget();
+		}
+		return null;
+	}
+
+	private CodeMemberDescriptor mkDescriptor(UnitContext ctx) {
+		Parameter[] params = computeParameters(ctx);
+		CodeMemberDescriptor descriptor = new CodeMemberDescriptor(
+			ctx.location(),
+			ctx.unit(),
+			false, ctx.getText(), Untyped.INSTANCE,
+			params);
+
+		descriptor.setOverridable(!ctx.isFinal());
+		return descriptor;
+	}
+
+	private Parameter[] computeParameters(UnitContext ctx) {
+		Function f = ctx.function();
+		ProgramContext programContext = f.getProgram().getProgramContext();
+		Set<Parameter> pset = new HashSet<>();
+		for (Register r : programContext.getRegisters()) {
+			RegisterValue rv = programContext.getRegisterValue(r, f.getEntryPoint());
+			if (rv != null && rv.hasValue()) {
+				Parameter p = new Parameter(ctx.location(), r.getAddress().toString());
+				pset.add(p);
+			}
+		}
+		Parameter[] params = new Parameter[pset.size() + 1];
+		int index = 0;
+		params[index++] = new Parameter(ctx.location(), ctx.getText());
+		for (Parameter p : pset) {
+			params[index++] = p;
+		}
+		return params;
+	}
+
+	public Program getProgram() {
+		return program;
+	}
+
+	public Set<Statement> getStatement(Address addr) {
+		return nodeMap.get(addr);
+	}
+
+	public boolean hasProcessed(Function f) {
+		if (f == null) {
+			return false;
+		}
+		return targets.containsKey(f.getEntryPoint());
+	}
+
+	public void clearTargets() {
+		targets.clear();
+	}
+
+	public CFG getTarget(Address entryPoint) {
+		return targets.get(entryPoint);
+	}
+
+	public Map<Address, CFG> getTargets() {
+		return targets;
+	}
+
+}

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

@@ -0,0 +1,78 @@
+/* ###
+ * 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;
+
+import ghidra.lisa.pcode.contexts.StatementContext;
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.program.model.pcode.PcodeOp;
+import it.unive.lisa.program.cfg.edge.*;
+import it.unive.lisa.program.cfg.statement.Statement;
+
+public class WorkItem {
+
+	public enum PredType {
+		TRUE,
+		FALSE,
+		SEQ
+	}
+
+	private Statement pred;
+	private PredType type;
+	private StatementContext context;
+
+	public WorkItem(Statement pred, StatementContext ctx) {
+		this.pred = pred;
+		this.context = ctx;
+		this.type = PredType.SEQ;
+	}
+
+	public StatementContext getContext() {
+		return context;
+	}
+
+	public Statement getPred() {
+		return pred;
+	}
+
+	public void setType(boolean val) {
+		type = val ? PredType.TRUE : PredType.FALSE;
+	}
+
+	public Edge computeBranch(Statement succ) {
+		PcodeLocation loc = (PcodeLocation) pred.getLocation();
+		if (loc.getOpcode() == PcodeOp.RETURN) {
+			return null;
+		}
+		return switch (getType()) {
+			case TRUE -> new TrueEdge(pred, succ);
+			case FALSE -> new FalseEdge(pred, succ);
+			case SEQ -> new SequentialEdge(pred, succ);
+			default -> throw new IllegalArgumentException("Unexpected value: " + getType());
+		};
+	}
+
+	public PredType getType() {
+		return type;
+	}
+
+	public String getKey() {
+		String key = context.getOp().getSeqnum().toString();
+		if (pred != null) {
+			key = pred.getLocation().getCodeLocation() + "=>" + key;
+		}
+		return key;
+	}
+}

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

@@ -0,0 +1,453 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import java.math.BigDecimal;
+import java.util.Iterator;
+
+import it.unive.lisa.util.numeric.*;
+
+/**
+ * An interval with long bounds.
+ * 
+ * <p>
+ * Modified to handle pcode from original source written by:
+ * <p>
+ * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
+ */
+public class LongInterval implements Iterable<Long>, Comparable<LongInterval> {
+
+	/**
+	 * The interval {@code [-Inf, +Inf]}.
+	 */
+	public static final LongInterval INFINITY = new LongInterval();
+
+	/**
+	 * The interval {@code [0, 0]}.
+	 */
+	public static final LongInterval ZERO = new LongInterval(0, 0);
+
+	/**
+	 * The interval {@code [1, 1]}.
+	 */
+	public static final LongInterval ONE = new LongInterval(1, 1);
+
+	/**
+	 * The interval {@code [-1, -1]}.
+	 */
+	public static final LongInterval MINUS_ONE = new LongInterval(-1, -1);
+
+	private final MathNumber low;
+
+	private final MathNumber high;
+
+	private LongInterval() {
+		this(MathNumber.MINUS_INFINITY, MathNumber.PLUS_INFINITY);
+	}
+
+	/**
+	 * Builds a new interval. Order of the bounds is adjusted (i.e., if
+	 * {@code low} is greater then {@code high}, then the interval
+	 * {@code [high, low]} is created).
+	 * 
+	 * @param low  the lower bound
+	 * @param high the upper bound
+	 */
+	public LongInterval(long low, long high) {
+		this(new MathNumber(low), new MathNumber(high));
+	}
+
+	/**
+	 * Builds a new interval. Order of the bounds is adjusted (i.e., if
+	 * {@code low} is greater then {@code high}, then the interval
+	 * {@code [high, low]} is created).
+	 * 
+	 * @param low  the lower bound (if {@code null}, -inf will be used)
+	 * @param high the upper bound (if {@code null}, +inf will be used)
+	 */
+	public LongInterval(
+			Integer low,
+			Integer high) {
+		this(low == null ? MathNumber.MINUS_INFINITY : new MathNumber(low),
+			high == null ? MathNumber.PLUS_INFINITY : new MathNumber(high));
+	}
+
+	/**
+	 * Builds a new interval. Order of the bounds is adjusted (i.e., if
+	 * {@code low} is greater then {@code high}, then the interval
+	 * {@code [high, low]} is created).
+	 * 
+	 * @param low  the lower bound
+	 * @param high the upper bound
+	 */
+	public LongInterval(
+			MathNumber low,
+			MathNumber high) {
+		if (low.isNaN() || high.isNaN()) {
+			this.low = MathNumber.NaN;
+			this.high = MathNumber.NaN;
+		}
+		else if (low.compareTo(high) <= 0) {
+			this.low = low;
+			this.high = high;
+		}
+		else {
+			this.low = high;
+			this.high = low;
+		}
+	}
+
+	/**
+	 * Yields the upper bound of this interval.
+	 * 
+	 * @return the upper bound of this interval
+	 */
+	public MathNumber getHigh() {
+		return high;
+	}
+
+	/**
+	 * Yields the lower bound of this interval.
+	 * 
+	 * @return the lower bound of this interval
+	 */
+	public MathNumber getLow() {
+		return low;
+	}
+
+	/**
+	 * Yields {@code true} if the lower bound of this interval is set to minus
+	 * infinity.
+	 * 
+	 * @return {@code true} if that condition holds
+	 */
+	public boolean lowIsMinusInfinity() {
+		return low.isMinusInfinity();
+	}
+
+	/**
+	 * Yields {@code true} if the upper bound of this interval is set to plus
+	 * infinity.
+	 * 
+	 * @return {@code true} if that condition holds
+	 */
+	public boolean highIsPlusInfinity() {
+		return high.isPlusInfinity();
+	}
+
+	/**
+	 * Yields {@code true} if this is interval is not finite, that is, if at
+	 * least one bound is set to infinity.
+	 * 
+	 * @return {@code true} if that condition holds
+	 */
+	public boolean isInfinite() {
+		return this == INFINITY || (highIsPlusInfinity() || lowIsMinusInfinity());
+	}
+
+	/**
+	 * Yields {@code true} if this is interval is finite, that is, if neither
+	 * bound is set to infinity.
+	 * 
+	 * @return {@code true} if that condition holds
+	 */
+	public boolean isFinite() {
+		return !isInfinite();
+	}
+
+	/**
+	 * Yields {@code true} if this is the interval representing infinity, that
+	 * is, {@code [-Inf, +Inf]}.
+	 * 
+	 * @return {@code true} if that condition holds
+	 */
+	public boolean isInfinity() {
+		return this == INFINITY;
+	}
+
+	/**
+	 * Yields {@code true} if this is a singleton interval, that is, if the
+	 * lower bound and the upper bound are the same.
+	 * 
+	 * @return {@code true} if that condition holds
+	 */
+	public boolean isSingleton() {
+		return isFinite() && low.equals(high);
+	}
+
+	/**
+	 * Yields {@code true} if this is a singleton interval containing only
+	 * {@code n}.
+	 *
+	 * @param n the integer to test
+	 * 
+	 * @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));
+	}
+
+	private static LongInterval cacheAndRound(
+			LongInterval i) {
+		if (i.is(0)) {
+			return ZERO;
+		}
+		if (i.is(1)) {
+			return ONE;
+		}
+		if (i.is(-1)) {
+			return MINUS_ONE;
+		}
+		return new LongInterval(i.low.roundDown(), i.high.roundUp());
+	}
+
+	/**
+	 * Performs the interval addition between {@code this} and {@code other}.
+	 * 
+	 * @param other the other interval
+	 * 
+	 * @return {@code this + other}
+	 */
+	public LongInterval plus(
+			LongInterval other) {
+		if (isInfinity() || other.isInfinity()) {
+			return INFINITY;
+		}
+
+		return cacheAndRound(new LongInterval(low.add(other.low), high.add(other.high)));
+	}
+
+	/**
+	 * Performs the interval subtraction between {@code this} and {@code other}.
+	 * 
+	 * @param other the other interval
+	 * 
+	 * @return {@code this - other}
+	 */
+	public LongInterval diff(
+			LongInterval other) {
+		if (isInfinity() || other.isInfinity()) {
+			return INFINITY;
+		}
+
+		return cacheAndRound(new LongInterval(low.subtract(other.high), high.subtract(other.low)));
+	}
+
+	private static MathNumber min(
+			MathNumber... nums) {
+		if (nums.length == 0) {
+			throw new IllegalArgumentException("No numbers provided");
+		}
+
+		MathNumber min = nums[0];
+		for (int i = 1; i < nums.length; i++) {
+			min = min.min(nums[i]);
+		}
+
+		return min;
+	}
+
+	private static MathNumber max(
+			MathNumber... nums) {
+		if (nums.length == 0) {
+			throw new IllegalArgumentException("No numbers provided");
+		}
+
+		MathNumber max = nums[0];
+		for (int i = 1; i < nums.length; i++) {
+			max = max.max(nums[i]);
+		}
+
+		return max;
+	}
+
+	/**
+	 * Performs the interval multiplication between {@code this} and
+	 * {@code other}.
+	 * 
+	 * @param other the other interval
+	 * 
+	 * @return {@code this * other}
+	 */
+	public LongInterval mul(
+			LongInterval other) {
+		if (is(0) || other.is(0)) {
+			return ZERO;
+		}
+		if (isInfinity() || other.isInfinity()) {
+			return INFINITY;
+		}
+
+		if (low.compareTo(MathNumber.ZERO) >= 0 && other.low.compareTo(MathNumber.ZERO) >= 0) {
+			return cacheAndRound(
+				new LongInterval(low.multiply(other.low), high.multiply(other.high)));
+		}
+
+		MathNumber ll = low.multiply(other.low);
+		MathNumber lh = low.multiply(other.high);
+		MathNumber hl = high.multiply(other.low);
+		MathNumber hh = high.multiply(other.high);
+		return cacheAndRound(new LongInterval(min(ll, lh, hl, hh), max(ll, lh, hl, hh)));
+	}
+
+	/**
+	 * Performs the interval division between {@code this} and {@code other}.
+	 * 
+	 * @param other       the other interval
+	 * @param ignoreZero  if {@code true}, causes the division to ignore the
+	 *                        fact that {@code other} might contain 0, producing
+	 *                        a smaller result
+	 * @param errorOnZero whether or not an {@link ArithmeticException} should
+	 *                        be thrown immediately if {@code other} contains
+	 *                        zero
+	 * 
+	 * @return {@code this / other}
+	 * 
+	 * @throws ArithmeticException if {@code other} contains 0 and
+	 *                                 {@code errorOnZero} is set to
+	 *                                 {@code true}
+	 */
+	public LongInterval div(
+			LongInterval other,
+			boolean ignoreZero,
+			boolean errorOnZero) {
+		if (errorOnZero && (other.is(0) || other.includes(ZERO))) {
+			throw new ArithmeticException("IntInterval divide by zero");
+		}
+
+		if (is(0)) {
+			return ZERO;
+		}
+
+		if (!other.includes(ZERO)) {
+			return mul(new LongInterval(MathNumber.ONE.divide(other.high),
+				MathNumber.ONE.divide(other.low)));
+		}
+		else if (other.high.isZero()) {
+			return mul(
+				new LongInterval(MathNumber.MINUS_INFINITY, MathNumber.ONE.divide(other.low)));
+		}
+		else if (other.low.isZero()) {
+			return mul(
+				new LongInterval(MathNumber.ONE.divide(other.high), MathNumber.PLUS_INFINITY));
+		}
+		else if (ignoreZero) {
+			return mul(new LongInterval(MathNumber.ONE.divide(other.low),
+				MathNumber.ONE.divide(other.high)));
+		}
+		else {
+			LongInterval lower =
+				mul(new LongInterval(MathNumber.MINUS_INFINITY, MathNumber.ONE.divide(other.low)));
+			LongInterval higher =
+				mul(new LongInterval(MathNumber.ONE.divide(other.high), MathNumber.PLUS_INFINITY));
+
+			if (lower.includes(higher)) {
+				return lower;
+			}
+			else if (higher.includes(lower)) {
+				return higher;
+			}
+			else {
+				return cacheAndRound(
+					new LongInterval(lower.low.compareTo(higher.low) > 0 ? higher.low : lower.low,
+						lower.high.compareTo(higher.high) < 0 ? higher.high : lower.high));
+			}
+		}
+	}
+
+	/**
+	 * Yields {@code true} if this interval includes the given one.
+	 * 
+	 * @param other the other interval
+	 * 
+	 * @return {@code true} if it is included, {@code false} otherwise
+	 */
+	public boolean includes(
+			LongInterval other) {
+		return low.compareTo(other.low) <= 0 && high.compareTo(other.high) >= 0;
+	}
+
+	/**
+	 * Yields {@code true} if this interval intersects with the given one.
+	 * 
+	 * @param other the other interval
+	 * 
+	 * @return {@code true} if those intersects, {@code false} otherwise
+	 */
+	public boolean intersects(
+			LongInterval other) {
+		return includes(other) || other.includes(this) ||
+			(high.compareTo(other.low) >= 0 && high.compareTo(other.high) <= 0) ||
+			(other.high.compareTo(low) >= 0 && other.high.compareTo(high) <= 0);
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((high == null) ? 0 : high.hashCode());
+		result = prime * result + ((low == null) ? 0 : low.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(
+			Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		LongInterval other = (LongInterval) obj;
+		if (high == null) {
+			if (other.high != null) {
+				return false;
+			}
+		}
+		else if (!high.equals(other.high)) {
+			return false;
+		}
+		if (low == null) {
+			if (other.low != null) {
+				return false;
+			}
+		}
+		else if (!low.equals(other.low)) {
+			return false;
+		}
+		return true;
+	}
+
+	@Override
+	public String toString() {
+		return "[" + low + ", " + high + "]";
+	}
+
+	@Override
+	public Iterator<Long> iterator() {
+		if (!low.isFinite() || !high.isFinite() || low.isNaN() || high.isNaN())
+			throw new RuntimeException(low + " is infinite or NaN", null);
+		try {
+			return new IntIntervalIterator(low.toLong(), high.toLong());
+		}
+		catch (MathNumberConversionException e) {
+			throw new RuntimeException("Cannot convert " + low, null);
+		}
+	}
+
+	@Override
+	public int compareTo(
+			LongInterval o) {
+		int cmp;
+		if ((cmp = low.compareTo(o.low)) != 0) {
+			return cmp;
+		}
+		return high.compareTo(o.high);
+	}
+}

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

@@ -0,0 +1,367 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import java.math.BigInteger;
+import java.util.Objects;
+
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.lisa.pcode.statements.PcodeBinaryOperator;
+import ghidra.pcode.exec.BytesPcodeArithmetic;
+import ghidra.pcode.utils.Utils;
+import ghidra.program.model.lang.Language;
+import ghidra.program.model.lang.RegisterValue;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.util.Msg;
+import it.unive.lisa.analysis.*;
+import it.unive.lisa.analysis.lattices.Satisfiability;
+import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
+import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
+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.NumericType;
+import it.unive.lisa.type.Type;
+import it.unive.lisa.util.representation.StringRepresentation;
+import it.unive.lisa.util.representation.StructuredRepresentation;
+
+/**
+ * The overflow-insensitive basic numeric constant propagation abstract domain,
+ * tracking if a certain numeric value has constant value or not, implemented as
+ * a {@link BaseNonRelationalValueDomain}, handling top and bottom values for
+ * the expression evaluation and bottom values for the expression
+ * satisfiability. Top and bottom cases for least upper bounds, widening and
+ * less or equals operations are handled by {@link BaseLattice} in
+ * {@link BaseLattice#lub}, {@link BaseLattice#widening} and
+ * {@link BaseLattice#lessOrEqual}, respectively.
+ * 
+ * <p>
+ * Modified to handle pcode from original source written by:
+ * <p>
+ * @author <a href="mailto:vincenzo.arceri@unive.it">Vincenzo Arceri</a>
+ */
+public class PcodeByteBasedConstantPropagation
+		implements PcodeNonRelationalValueDomain<PcodeByteBasedConstantPropagation> {
+
+	private static final PcodeByteBasedConstantPropagation TOP =
+		new PcodeByteBasedConstantPropagation(true, false);
+	private static final PcodeByteBasedConstantPropagation BOTTOM =
+		new PcodeByteBasedConstantPropagation(false, true);
+	private static BytesPcodeArithmetic arithmetic;
+	private static boolean isBigEndian;
+
+	private final boolean isTop, isBottom;
+	private Long value;
+
+	/**
+	 * Builds the top abstract value.
+	 * 
+	 * @param language base language for current program
+	 */
+	public PcodeByteBasedConstantPropagation(Language language) {
+		this(0L, true, false);
+		PcodeByteBasedConstantPropagation.arithmetic =
+			BytesPcodeArithmetic.forLanguage(language);
+		isBigEndian = language.isBigEndian();
+	}
+
+	private PcodeByteBasedConstantPropagation(
+			Long value,
+			boolean isTop,
+			boolean isBottom) {
+		this.value = value;
+		this.isTop = isTop;
+		this.isBottom = isBottom;
+	}
+
+	private PcodeByteBasedConstantPropagation(
+			boolean isTop,
+			boolean isBottom) {
+		this(0L, isTop, isBottom);
+	}
+
+	public PcodeByteBasedConstantPropagation(
+			Long value) {
+		this(value, false, false);
+	}
+
+	public PcodeByteBasedConstantPropagation(
+			Boolean value) {
+		this(value ? 1L : 0L, false, false);
+	}
+
+	public PcodeByteBasedConstantPropagation(
+			byte[] bytes,
+			int size,
+			boolean isBigEndian) {
+		this(Utils.bytesToLong(bytes, size, isBigEndian));
+	}
+
+	@Override
+	public PcodeByteBasedConstantPropagation evalNullConstant(
+			ProgramPoint pp,
+			SemanticOracle oracle) {
+		return top();
+	}
+
+	@Override
+	public PcodeByteBasedConstantPropagation evalNonNullConstant(
+			Constant constant,
+			ProgramPoint pp,
+			SemanticOracle oracle) {
+		Object cval = constant.getValue();
+		if (cval instanceof Number val) {
+			Type staticType = constant.getStaticType();
+			if (staticType != null && staticType instanceof NumericType numType) {
+				if (numType.isSigned()) {
+					return new PcodeByteBasedConstantPropagation(Long.valueOf(val.longValue()));
+				}
+			}
+		}
+		if (cval instanceof Long lval) {
+			return new PcodeByteBasedConstantPropagation(lval);
+		}
+		if (cval instanceof Integer ival) {
+			return new PcodeByteBasedConstantPropagation(Integer.toUnsignedLong(ival));
+		}
+		if (cval instanceof Short sval) {
+			return new PcodeByteBasedConstantPropagation(Short.toUnsignedLong(sval));
+		}
+		if (cval instanceof Byte bval) {
+			return new PcodeByteBasedConstantPropagation(Byte.toUnsignedLong(bval));
+		}
+		if (cval instanceof Boolean bval) {
+			return new PcodeByteBasedConstantPropagation(bval ? 1L : 0L);
+		}
+		Msg.error(this, "Unknown type for constant: " + cval);
+		return top();
+	}
+
+	@Override
+	public PcodeByteBasedConstantPropagation evalUnaryExpression(
+			UnaryOperator operator,
+			PcodeByteBasedConstantPropagation arg,
+			ProgramPoint pp,
+			SemanticOracle oracle) {
+
+		if (arg.isTop()) {
+			return top();
+		}
+
+		PcodeLocation ploc = (PcodeLocation) pp.getLocation();
+		PcodeOp op = ploc.op;
+
+		byte[] bytes = arithmetic.unaryOp(op.getOpcode(), op.getOutput().getSize(),
+			op.getInput(0).getSize(), arg.getValue(op.getInput(0).getSize()));
+		return new PcodeByteBasedConstantPropagation(bytes, op.getOutput().getSize(),
+			isBigEndian);
+	}
+
+	private byte[] getValue(int size) {
+		return Utils.longToBytes(value, size, isBigEndian);
+	}
+
+	@Override
+	public PcodeByteBasedConstantPropagation evalBinaryExpression(
+			BinaryOperator operator,
+			PcodeByteBasedConstantPropagation left,
+			PcodeByteBasedConstantPropagation right,
+			ProgramPoint pp,
+			SemanticOracle oracle) {
+
+		if ((left.isTop || right.isTop) && !left.equals(right)) {
+			if (left.value == 0L || right.value == 0L) {
+				if (operator instanceof PcodeBinaryOperator poperator &&
+					poperator.getOp().getOpcode() == PcodeOp.INT_MULT) {
+					return new PcodeByteBasedConstantPropagation(0L);
+				}
+			}
+			return top();
+		}
+
+		PcodeLocation ploc = (PcodeLocation) pp.getLocation();
+		PcodeOp op = ploc.op;
+		if (left.isTop) {
+			return specialCaseLogic(op);
+		}
+		int lsize = op.getInput(0).getSize();
+		int rsize = op.getInput(1).getSize();
+		byte[] bytes = arithmetic.binaryOp(op.getOpcode(), op.getOutput().getSize(),
+			lsize, left.getValue(lsize),
+			rsize, right.getValue(rsize));
+		return new PcodeByteBasedConstantPropagation(bytes, op.getOutput().getSize(),
+			isBigEndian);
+	}
+
+	// These are instances that return zero when left==right.
+	private PcodeByteBasedConstantPropagation specialCaseLogic(PcodeOp op) {
+		int opcode = op.getOpcode();
+		if (opcode == PcodeOp.INT_SUB || opcode == PcodeOp.FLOAT_SUB ||
+			opcode == PcodeOp.BOOL_XOR || opcode == PcodeOp.INT_XOR) {
+			return new PcodeByteBasedConstantPropagation(0L);
+		}
+		return top();
+	}
+
+	@Override
+	public Satisfiability satisfiesBinaryExpression(
+			BinaryOperator operator,
+			PcodeByteBasedConstantPropagation left,
+			PcodeByteBasedConstantPropagation right,
+			ProgramPoint pp,
+			SemanticOracle oracle) {
+
+		if (left.isTop() || right.isTop()) {
+			return Satisfiability.UNKNOWN;
+		}
+
+		if (operator instanceof ComparisonEq) {
+			return left.value == right.value
+					? Satisfiability.SATISFIED
+					: Satisfiability.NOT_SATISFIED;
+		}
+		if (operator instanceof ComparisonNe) {
+			return left.value != right.value
+					? Satisfiability.SATISFIED
+					: Satisfiability.NOT_SATISFIED;
+		}
+		if (operator instanceof ComparisonLe) {
+			return left.value <= right.value
+					? Satisfiability.SATISFIED
+					: Satisfiability.NOT_SATISFIED;
+		}
+		if (operator instanceof ComparisonLt) {
+			return left.value < right.value
+					? Satisfiability.SATISFIED
+					: Satisfiability.NOT_SATISFIED;
+		}
+		return Satisfiability.UNKNOWN;
+	}
+
+	@Override
+	public ValueEnvironment<PcodeByteBasedConstantPropagation> assumeBinaryExpression(
+			ValueEnvironment<PcodeByteBasedConstantPropagation> environment,
+			BinaryOperator operator,
+			ValueExpression left,
+			ValueExpression right,
+			ProgramPoint src,
+			ProgramPoint dest,
+			SemanticOracle oracle)
+			throws SemanticException {
+
+		if (!(operator instanceof PcodeBinaryOperator)) {
+			if (operator instanceof ComparisonEq) {
+				if (left instanceof Identifier leftId) {
+					PcodeByteBasedConstantPropagation eval = eval(right, environment, src, oracle);
+					if (eval.isBottom()) {
+						return environment.bottom();
+					}
+					return environment.putState(leftId, eval);
+				}
+				else if (right instanceof Identifier rightId) {
+					PcodeByteBasedConstantPropagation eval = eval(left, environment, src, oracle);
+					if (eval.isBottom()) {
+						return environment.bottom();
+					}
+					return environment.putState(rightId, eval);
+				}
+			}
+			if (operator instanceof ComparisonNe) {
+				if (left instanceof Identifier leftId) {
+					PcodeByteBasedConstantPropagation eval = eval(right, environment, src, oracle);
+					if (eval.isBottom()) {
+						return environment.bottom();
+					}
+					eval.value = 1L - eval.value;
+					return environment.putState(leftId, eval);
+				}
+				else if (right instanceof Identifier rightId) {
+					PcodeByteBasedConstantPropagation eval = eval(left, environment, src, oracle);
+					if (eval.isBottom()) {
+						return environment.bottom();
+					}
+					eval.value = 1L - eval.value;
+					return environment.putState(rightId, eval);
+				}
+			}
+		}
+		return environment;
+	}
+
+	@Override
+	public PcodeByteBasedConstantPropagation lubAux(PcodeByteBasedConstantPropagation other)
+			throws SemanticException {
+		return TOP;
+	}
+
+	@Override
+	public boolean lessOrEqualAux(PcodeByteBasedConstantPropagation other)
+			throws SemanticException {
+		return false;
+	}
+
+	@Override
+	public PcodeByteBasedConstantPropagation top() {
+		return TOP;
+	}
+
+	@Override
+	public PcodeByteBasedConstantPropagation bottom() {
+		return BOTTOM;
+	}
+
+	@Override
+	public StructuredRepresentation representation() {
+		if (isBottom()) {
+			return Lattice.bottomRepresentation();
+		}
+		if (isTop()) {
+			return Lattice.topRepresentation();
+		}
+
+		return new StringRepresentation(value.toString());
+	}
+
+	@Override
+	public int hashCode() {
+		return Objects.hash(isBottom, isTop, value);
+	}
+
+	@Override
+	public boolean equals(
+			Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		if (!(obj instanceof PcodeByteBasedConstantPropagation other)) {
+			return false;
+		}
+
+		if (isBottom != other.isBottom) {
+			return false;
+		}
+		if (isTop != other.isTop) {
+			return false;
+		}
+		return Objects.equals(this.value, other.value);
+	}
+
+	@Override
+	public PcodeByteBasedConstantPropagation getValue(RegisterValue rv) {
+		if (rv != null) {
+			BigInteger val = rv.getUnsignedValue();
+			if (val != null) {
+				return new PcodeByteBasedConstantPropagation(val.longValue());
+			}
+		}
+		return top();
+	}
+}

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

@@ -0,0 +1,291 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import java.util.*;
+
+import ghidra.lisa.pcode.locations.InstLocation;
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.pcode.exec.BytesPcodeArithmetic;
+import ghidra.pcode.utils.Utils;
+import ghidra.program.model.address.Address;
+import ghidra.program.model.address.AddressFormatException;
+import ghidra.program.model.lang.*;
+import ghidra.program.model.listing.Function;
+import ghidra.program.model.listing.Program;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.util.Msg;
+import it.unive.lisa.analysis.ScopeToken;
+import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.dataflow.DataflowElement;
+import it.unive.lisa.analysis.dataflow.DefiniteDataflowDomain;
+import it.unive.lisa.program.cfg.ProgramPoint;
+import it.unive.lisa.program.cfg.statement.Assignment;
+import it.unive.lisa.symbolic.SymbolicExpression;
+import it.unive.lisa.symbolic.value.*;
+import it.unive.lisa.type.NumericType;
+import it.unive.lisa.type.Type;
+import it.unive.lisa.util.representation.*;
+
+/**
+ * An implementation of the overflow-insensitive constant propagation dataflow
+ * analysis, that focuses only on integers.
+ * 
+ * <p>
+ * Modified to handle pcode from original source written by:
+ * <p>
+ * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
+ */
+public class PcodeDataflowConstantPropagation implements
+		DataflowElement<DefiniteDataflowDomain<PcodeDataflowConstantPropagation>, PcodeDataflowConstantPropagation> {
+
+	private static BytesPcodeArithmetic arithmetic;
+	private static boolean isBigEndian;
+
+	private final Identifier id;
+	private final Long constant;
+
+	/**
+	* Builds an empty constant propagation object.
+	 * 
+	 * @param language base language for current program
+	*/
+	public PcodeDataflowConstantPropagation(Language language) {
+		this(null, null);
+		PcodeDataflowConstantPropagation.arithmetic = BytesPcodeArithmetic.forLanguage(language);
+		isBigEndian = language.isBigEndian();
+	}
+
+	/**
+	* Builds the new constant propagation object.
+	* 
+	* @param id the constant variable
+	* @param v  the constant value
+	*/
+	public PcodeDataflowConstantPropagation(
+			Identifier id,
+			Long v) {
+		this.id = id;
+		this.constant = v;
+	}
+
+	@Override
+	public String toString() {
+		return representation().toString();
+	}
+
+	@Override
+	public Collection<Identifier> getInvolvedIdentifiers() {
+		return Collections.singleton(id);
+	}
+
+	private static byte[] getValue(long val, int size) {
+		return Utils.longToBytes(val, size, isBigEndian);
+	}
+
+	private static Long eval(
+			SymbolicExpression e, ProgramPoint pp,
+			DefiniteDataflowDomain<PcodeDataflowConstantPropagation> domain) {
+
+		if (e instanceof Constant c) {
+			Object cval = c.getValue();
+			if (cval instanceof Number nval) {
+				Type staticType = c.getStaticType();
+				if (staticType != null && staticType instanceof NumericType numType) {
+					if (numType.isSigned()) {
+						return Long.valueOf(nval.longValue());
+					}
+				}
+			}
+			if (cval instanceof Long lval) {
+				return lval;
+			}
+			if (cval instanceof Integer ival) {
+				return Integer.toUnsignedLong(ival);
+			}
+			if (cval instanceof Short sval) {
+				return Short.toUnsignedLong(sval);
+			}
+			if (cval instanceof Byte bval) {
+				return Byte.toUnsignedLong(bval);
+			}
+			if (cval instanceof Boolean bval) {
+				return bval ? 1L : 0L;
+			}
+			Msg.error(e, "Unknown type for constant: " + cval);
+			return null;
+		}
+
+		if (e instanceof Identifier) {
+			for (PcodeDataflowConstantPropagation cp : domain.getDataflowElements()) {
+				if (cp.id.equals(e)) {
+					return cp.constant;
+				}
+			}
+
+			return null;
+		}
+
+		if (!(pp.getLocation() instanceof PcodeLocation ploc)) {
+			return null;
+		}
+
+		PcodeOp op = ploc.op;
+
+		if (e instanceof UnaryExpression unary) {
+			Long i = eval(unary.getExpression(), pp, domain);
+
+			if (i == null) {
+				return i;
+			}
+
+			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);
+		}
+
+		if (e instanceof BinaryExpression binary) {
+			Long right = eval(binary.getRight(), pp, domain);
+			Long left = eval(binary.getLeft(), pp, domain);
+
+			if (right == null || left == null) {
+				return null;
+			}
+
+			int lsize = op.getInput(0).getSize();
+			int rsize = op.getInput(1).getSize();
+			byte[] bytes = arithmetic.binaryOp(op.getOpcode(), op.getOutput().getSize(),
+				lsize, getValue(left, lsize),
+				rsize, getValue(right, rsize));
+			return Utils.bytesToLong(bytes, op.getOutput().getSize(), isBigEndian);
+		}
+
+		if (e instanceof PushAny) {
+			InstLocation loc = (InstLocation) pp.getLocation();
+			Function f = loc.function();
+			try {
+				if (f != null && pp instanceof Assignment a) {
+					Program program = f.getProgram();
+					Address address = program.getAddressFactory()
+							.getRegisterSpace()
+							.getAddress(a.getLeft().toString());
+					Register r = program.getRegister(address);
+					if (r != null) {
+						RegisterValue rv =
+							program.getProgramContext().getRegisterValue(r, f.getEntryPoint());
+						if (rv != null && rv.hasValue()) {
+							return rv.getUnsignedValue().longValue();
+						}
+					}
+				}
+			}
+			catch (AddressFormatException e1) {
+				// IGNORE
+			}
+		}
+
+		return null;
+	}
+
+	@Override
+	public Collection<PcodeDataflowConstantPropagation> gen(
+			Identifier idg,
+			ValueExpression expression,
+			ProgramPoint pp,
+			DefiniteDataflowDomain<PcodeDataflowConstantPropagation> domain) {
+		Set<PcodeDataflowConstantPropagation> gen = new HashSet<>();
+
+		Long v = eval(expression, pp, domain);
+		if (v != null) {
+			gen.add(new PcodeDataflowConstantPropagation(idg, v));
+		}
+
+		return gen;
+	}
+
+	@Override
+	public Collection<PcodeDataflowConstantPropagation> gen(
+			ValueExpression expression,
+			ProgramPoint pp,
+			DefiniteDataflowDomain<PcodeDataflowConstantPropagation> domain) {
+		return Collections.emptyList();
+	}
+
+	@Override
+	public Collection<PcodeDataflowConstantPropagation> kill(
+			Identifier idk,
+			ValueExpression expression,
+			ProgramPoint pp,
+			DefiniteDataflowDomain<PcodeDataflowConstantPropagation> domain) {
+		Collection<PcodeDataflowConstantPropagation> result = new HashSet<>();
+
+		for (PcodeDataflowConstantPropagation cp : domain.getDataflowElements()) {
+			if (cp.id.equals(idk)) {
+				result.add(cp);
+			}
+		}
+
+		return result;
+	}
+
+	@Override
+	public Collection<PcodeDataflowConstantPropagation> kill(
+			ValueExpression expression,
+			ProgramPoint pp,
+			DefiniteDataflowDomain<PcodeDataflowConstantPropagation> domain) {
+		return Collections.emptyList();
+	}
+
+	@Override
+	public int hashCode() {
+		return Objects.hash(id, constant);
+	}
+
+	@Override
+	public boolean equals(
+			Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+
+		PcodeDataflowConstantPropagation other = (PcodeDataflowConstantPropagation) obj;
+		if (!Objects.equals(this.id, other.id)) {
+			return false;
+		}
+		return Objects.equals(this.constant, other.constant);
+	}
+
+	@Override
+	public StructuredRepresentation representation() {
+		return new ListRepresentation(new StringRepresentation(id),
+			new StringRepresentation(constant));
+	}
+
+	@Override
+	public PcodeDataflowConstantPropagation pushScope(
+			ScopeToken scope)
+			throws SemanticException {
+		return new PcodeDataflowConstantPropagation((Identifier) id.pushScope(scope), constant);
+	}
+
+	@Override
+	public PcodeDataflowConstantPropagation popScope(
+			ScopeToken scope)
+			throws SemanticException {
+		if (!(id instanceof OutOfScopeIdentifier)) {
+			return this;
+		}
+
+		return new PcodeDataflowConstantPropagation(((OutOfScopeIdentifier) id).popScope(scope),
+			constant);
+	}
+
+}

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

@@ -0,0 +1,259 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import java.util.*;
+
+import ghidra.lisa.pcode.statements.PcodeBinaryOperator;
+import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.nonRedundantSet.NonRedundantPowersetOfBaseNonRelationalValueDomain;
+import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
+import it.unive.lisa.analysis.numeric.Interval;
+import it.unive.lisa.program.cfg.ProgramPoint;
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.symbolic.value.ValueExpression;
+import it.unive.lisa.symbolic.value.operator.binary.*;
+import it.unive.lisa.util.numeric.MathNumber;
+
+/**
+ * The finite non redundant powerset of {@link Interval} abstract domain
+ * approximating numeric values as a non redundant set of interval. It is
+ * implemented as a {@link NonRedundantPowersetOfBaseNonRelationalValueDomain},
+ * which handles most of the basic operation (such as
+ * {@link NonRedundantPowersetOfBaseNonRelationalValueDomain#lubAux lub},
+ * {@link NonRedundantPowersetOfBaseNonRelationalValueDomain#glbAux glb},
+ * {@link NonRedundantPowersetOfBaseNonRelationalValueDomain#wideningAux
+ * widening} and others operations needed to calculate the previous ones).
+ */
+public class PcodeNonRedundantPowersetOfInterval
+		extends
+		NonRedundantPowersetOfBaseNonRelationalValueDomain<PcodeNonRedundantPowersetOfInterval, Interval> {
+
+	/**
+	 * Constructs an empty non redundant set of intervals.
+	 */
+	public PcodeNonRedundantPowersetOfInterval() {
+		super(new TreeSet<>(), Interval.BOTTOM);
+	}
+
+	/**
+	 * Constructs a non redundant set of intervals with the given intervals.
+	 * 
+	 * @param elements the set of intervals
+	 */
+	public PcodeNonRedundantPowersetOfInterval(
+			SortedSet<Interval> elements) {
+		super(elements, Interval.BOTTOM);
+	}
+
+	/**
+	 * This specific Egli-Milner connector follows this definition:<br>
+	 * given two subsets S<sub>1</sub> and S<sub>2</sub> of a domain of a
+	 * lattice:
+	 * <p>
+	 * S<sub>1</sub> +<sub>EM</sub> S<sub>2</sub> = {s<sub>2</sub> &ni;
+	 * S<sub>2</sub> | &exist; s<sub>1</sub> &ni; S<sub>1</sub> : s<sub>1</sub>
+	 * &le; s<sub>2</sub>} &cup; {lub(s'<sub>1</sub>, s<sub>2</sub>) |
+	 * s'<sub>1</sub> &ni; S<sub>1</sub>, s<sub>2</sub> &ni; S<sub>2</sub>, NOT
+	 * &exist; s<sub>1</sub> &ni; S<sub>1</sub> : s<sub>1</sub> &le;
+	 * s<sub>2</sub>}
+	 * </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}).
+	 */
+	@Override
+	protected PcodeNonRedundantPowersetOfInterval EgliMilnerConnector(
+			PcodeNonRedundantPowersetOfInterval other)
+			throws SemanticException {
+		SortedSet<Interval> newElementsSet = new TreeSet<>();
+		SortedSet<Interval> notCoverSet = new TreeSet<>();
+
+		// first side of the union
+		for (Interval s2 : other.elementsSet) {
+			boolean existsLower = false;
+			for (Interval s1 : elementsSet) {
+				if (s1.lessOrEqual(s2)) {
+					existsLower = true;
+					break;
+				}
+			}
+			if (existsLower) {
+				newElementsSet.add(s2);
+			}
+			else {
+				notCoverSet.add(s2);
+			}
+		}
+
+		// second side of the union
+		for (Interval s2 : notCoverSet) {
+			MathNumber middlePoint = middlePoint(s2);
+			MathNumber closestValue = middlePoint;
+			MathNumber closestDiff = closestValue.subtract(middlePoint).abs();
+			Interval closest = Interval.TOP;
+			for (Interval s1 : elementsSet) {
+				if (closestValue.compareTo(middlePoint) == 0) {
+					closest = s1;
+					closestValue = middlePoint(s1);
+					closestDiff = closestValue.subtract(middlePoint).abs();
+				}
+				else {
+					MathNumber s1Diff = middlePoint(s1).subtract(middlePoint).abs();
+					if (s1Diff.compareTo(closestDiff) < 0) {
+						closest = s1;
+						closestValue = middlePoint(s1);
+						closestDiff = closestValue.subtract(middlePoint).abs();
+					}
+				}
+			}
+			newElementsSet.add(s2.lub(closest));
+		}
+		return new PcodeNonRedundantPowersetOfInterval(newElementsSet).removeRedundancy()
+				.removeOverlapping();
+	}
+
+	/**
+	 * Yields the middle point of an {@link Interval}. If both extremes are
+	 * non-infinite the middle point is the sum of the two divided by two. If
+	 * only one of the two extreme is infinite the middle point is said to be
+	 * the non-infinite extreme. If both the extremes are infinite the middle
+	 * point is said to be 0.
+	 * 
+	 * @param interval the interval to calculate the middle point of
+	 * 
+	 * @return the middle point of the interval
+	 */
+	protected MathNumber middlePoint(
+			Interval interval) {
+		if (interval.interval.isFinite()) {
+			return interval.interval.getLow()
+					.add(interval.interval.getHigh())
+					.divide(new MathNumber(2));
+		}
+		else if (interval.interval.getHigh().isFinite() && !interval.interval.getLow().isFinite()) {
+			return interval.interval.getHigh();
+		}
+		else if (!interval.interval.getHigh().isFinite() && interval.interval.getLow().isFinite()) {
+			return interval.interval.getLow().subtract(MathNumber.ONE);
+		}
+		// both infinite
+		return MathNumber.ZERO;
+	}
+
+	@Override
+	public ValueEnvironment<PcodeNonRedundantPowersetOfInterval> assumeBinaryExpression(
+			ValueEnvironment<PcodeNonRedundantPowersetOfInterval> environment,
+			BinaryOperator operator,
+			ValueExpression left,
+			ValueExpression right,
+			ProgramPoint src,
+			ProgramPoint dest,
+			SemanticOracle oracle)
+			throws SemanticException {
+		Identifier id;
+		PcodeNonRedundantPowersetOfInterval eval;
+		boolean rightIsExpr;
+		if (left instanceof Identifier leftId) {
+			eval = eval(right, environment, src, oracle);
+			id = leftId;
+			rightIsExpr = true;
+		}
+		else if (right instanceof Identifier rightId) {
+			eval = eval(left, environment, src, oracle);
+			id = rightId;
+			rightIsExpr = false;
+		}
+		else {
+			return environment;
+		}
+
+		PcodeNonRedundantPowersetOfInterval starting = environment.getState(id);
+		if (eval.isBottom() || starting.isBottom()) {
+			return environment.bottom();
+		}
+
+		SortedSet<Interval> newSet = new TreeSet<>();
+
+		for (Interval startingInterval : starting.elementsSet)
+			for (Interval 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),
+					MathNumber.PLUS_INFINITY);
+				Interval infHigh =
+					new Interval(MathNumber.MINUS_INFINITY, interval.interval.getHigh());
+				Interval infHighm1 = new Interval(MathNumber.MINUS_INFINITY,
+					interval.interval.getHigh().subtract(MathNumber.ONE));
+
+				if (!(operator instanceof PcodeBinaryOperator)) {
+					if (operator instanceof ComparisonEq) {
+						newSet.add(interval);
+					}
+					else if (operator instanceof ComparisonLe) {
+						if (rightIsExpr) {
+							newSet.add(startingInterval.glb(infHigh));
+						}
+						else if (lowIsMinusInfinity) {
+							newSet.add(startingInterval);
+						}
+						else {
+							newSet.add(startingInterval.glb(lowInf));
+						}
+					}
+					else if (operator instanceof ComparisonLt) {
+						if (rightIsExpr) {
+							newSet.add(
+								lowIsMinusInfinity ? interval : startingInterval.glb(infHighm1));
+						}
+						else if (lowIsMinusInfinity) {
+							newSet.add(startingInterval);
+						}
+						else {
+							newSet.add(startingInterval.glb(lowp1Inf));
+						}
+					}
+					else {
+						newSet.add(startingInterval);
+					}
+				}
+			}
+
+		PcodeNonRedundantPowersetOfInterval intervals =
+			new PcodeNonRedundantPowersetOfInterval(newSet)
+					.removeRedundancy()
+					.removeOverlapping();
+		if (intervals.isBottom()) {
+			return environment.bottom();
+		}
+		return environment.putState(id, intervals);
+	}
+
+	@Override
+	protected PcodeNonRedundantPowersetOfInterval mk(
+			SortedSet<Interval> elements) {
+		return new PcodeNonRedundantPowersetOfInterval(elements);
+	}
+
+	@Override
+	public boolean equals(
+			Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		PcodeNonRedundantPowersetOfInterval other = (PcodeNonRedundantPowersetOfInterval) obj;
+		if (!Objects.equals(this.elementsSet, other.elementsSet)) {
+			return false;
+		}
+		return Objects.equals(this.valueDomain, other.valueDomain);
+	}
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/analyses/PcodeNonRelationalValueDomain.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.analyses;
+
+import ghidra.lisa.pcode.locations.InstLocation;
+import ghidra.program.model.address.Address;
+import ghidra.program.model.address.AddressFormatException;
+import ghidra.program.model.lang.Register;
+import ghidra.program.model.lang.RegisterValue;
+import ghidra.program.model.listing.Function;
+import ghidra.program.model.listing.Program;
+import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.SemanticOracle;
+import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
+import it.unive.lisa.program.cfg.ProgramPoint;
+import it.unive.lisa.program.cfg.statement.Assignment;
+import it.unive.lisa.symbolic.value.PushAny;
+
+/**
+ * @param <T> the concrete type of this domain
+ */
+public interface PcodeNonRelationalValueDomain<T extends PcodeNonRelationalValueDomain<T>>
+		extends BaseNonRelationalValueDomain<T> {
+
+	T getValue(RegisterValue rv);
+
+	default T getValue(ProgramPoint pp) {
+		InstLocation loc = (InstLocation) pp.getLocation();
+		Function f = loc.function();
+		if (f != null && pp instanceof Assignment a) {
+			Program program = f.getProgram();
+			try {
+				Address address = program.getAddressFactory()
+						.getRegisterSpace()
+						.getAddress(a.getLeft().toString());
+				Register r = program.getRegister(address);
+				if (r != null) {
+					RegisterValue rv =
+						program.getProgramContext().getRegisterValue(r, f.getEntryPoint());
+					return getValue(rv);
+				}
+			}
+			catch (AddressFormatException e) {
+				// IGNORE
+			}
+		}
+		return getValue((RegisterValue) null);
+	}
+
+	@Override
+	default T evalPushAny(
+			PushAny pushAny,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		T v = getValue(pp);
+		return v == null ? top() : v;
+	}
+}

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

@@ -0,0 +1,304 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import java.math.BigInteger;
+
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.program.model.lang.RegisterValue;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.util.Msg;
+import it.unive.lisa.analysis.*;
+import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
+import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
+import it.unive.lisa.program.cfg.ProgramPoint;
+import it.unive.lisa.symbolic.value.*;
+import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
+import it.unive.lisa.symbolic.value.operator.binary.ComparisonEq;
+import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator;
+import it.unive.lisa.util.representation.StringRepresentation;
+import it.unive.lisa.util.representation.StructuredRepresentation;
+
+/**
+ * The overflow-insensitive Parity abstract domain, tracking if a numeric value
+ * is even or odd, implemented as a {@link BaseNonRelationalValueDomain},
+ * handling top and bottom values for the expression evaluation and bottom
+ * values for the expression satisfiability. Top and bottom cases for least
+ * upper bound, widening and less or equals operations are handled by
+ * {@link BaseLattice} in {@link BaseLattice#lub}, {@link BaseLattice#widening}
+ * and {@link BaseLattice#lessOrEqual} methods, respectively.
+ * 
+ * <p>
+ * Modified to handle pcode from original source written by:
+ * <p>
+ * @author <a href="mailto:vincenzo.arceri@unive.it">Vincenzo Arceri</a>
+ */
+public class PcodeParity implements PcodeNonRelationalValueDomain<PcodeParity> {
+
+	/**
+	 * The abstract even element.
+	 */
+	public static final PcodeParity EVEN = new PcodeParity((byte) 3);
+
+	/**
+	 * The abstract odd element.
+	 */
+	public static final PcodeParity ODD = new PcodeParity((byte) 2);
+
+	/**
+	 * The abstract top element.
+	 */
+	public static final PcodeParity TOP = new PcodeParity((byte) 0);
+
+	/**
+	 * The abstract bottom element.
+	 */
+	public static final PcodeParity BOTTOM = new PcodeParity((byte) 1);
+
+	private final byte parity;
+
+	/**
+	 * Builds the parity abstract domain, representing the top of the parity
+	 * abstract domain.
+	 */
+	public PcodeParity() {
+		this((byte) 0);
+	}
+
+	/**
+	 * Builds the parity instance for the given parity value.
+	 * 
+	 * @param parity the sign (0 = top, 1 = bottom, 2 = odd, 3 = even)
+	 */
+	public PcodeParity(
+			byte parity) {
+		this.parity = parity;
+	}
+
+	@Override
+	public PcodeParity top() {
+		return TOP;
+	}
+
+	@Override
+	public PcodeParity bottom() {
+		return BOTTOM;
+	}
+
+	@Override
+	public StructuredRepresentation representation() {
+		if (isBottom()) {
+			return Lattice.bottomRepresentation();
+		}
+		if (isTop()) {
+			return Lattice.topRepresentation();
+		}
+
+		String repr = this == EVEN ? "Even" : "Odd";
+
+		return new StringRepresentation(repr);
+	}
+
+	@Override
+	public PcodeParity evalNullConstant(
+			ProgramPoint pp,
+			SemanticOracle oracle) {
+		return top();
+	}
+
+	@Override
+	public PcodeParity evalNonNullConstant(
+			Constant constant,
+			ProgramPoint pp,
+			SemanticOracle oracle) {
+
+		Object cval = constant.getValue();
+		if (cval instanceof Long lval) {
+			return lval % 2 == 0 ? EVEN : ODD;
+		}
+		if (cval instanceof Integer ival) {
+			return ival % 2 == 0 ? EVEN : ODD;
+		}
+		if (cval instanceof Short sval) {
+			return sval % 2 == 0 ? EVEN : ODD;
+		}
+		if (cval instanceof Byte bval) {
+			return bval % 2 == 0 ? EVEN : ODD;
+		}
+		if (cval instanceof Boolean bval) {
+			return bval ? ODD : EVEN;
+		}
+		Msg.error(this, "Unknown type for constant: " + cval);
+
+		return top();
+	}
+
+	/**
+	 * Yields whether or not this is the even parity.
+	 * 
+	 * @return {@code true} if that condition holds
+	 */
+	public boolean isEven() {
+		return this == EVEN;
+	}
+
+	/**
+	 * Yields whether or not this is the odd parity.
+	 * 
+	 * @return {@code true} if that condition holds
+	 */
+	public boolean isOdd() {
+		return this == ODD;
+	}
+
+	@Override
+	public PcodeParity evalUnaryExpression(
+			UnaryOperator operator,
+			PcodeParity arg,
+			ProgramPoint pp,
+			SemanticOracle oracle) {
+		return arg;
+	}
+
+	@Override
+	public PcodeParity evalBinaryExpression(
+			BinaryOperator operator,
+			PcodeParity left,
+			PcodeParity right,
+			ProgramPoint pp,
+			SemanticOracle oracle) {
+		if (left.isTop() || right.isTop()) {
+			return top();
+		}
+
+		PcodeLocation ploc = (PcodeLocation) pp.getLocation();
+		PcodeOp op = ploc.op;
+		int opcode = op.getOpcode();
+		if (opcode == PcodeOp.INT_ADD || opcode == PcodeOp.FLOAT_ADD ||
+			opcode == PcodeOp.INT_SUB || opcode == PcodeOp.FLOAT_SUB) {
+			return (right.equals(left)) ? EVEN : ODD;
+		}
+		else if (opcode == PcodeOp.INT_AND || opcode == PcodeOp.BOOL_AND) {
+			return (right.equals(left)) ? left : EVEN;
+		}
+		else if (opcode == PcodeOp.INT_OR || opcode == PcodeOp.BOOL_OR) {
+			return (right.equals(left)) ? left : ODD;
+		}
+		else if (opcode == PcodeOp.INT_XOR || opcode == PcodeOp.BOOL_XOR) {
+			return (right.equals(left)) ? EVEN : ODD;
+		}
+		else if (opcode == PcodeOp.INT_MULT || opcode == PcodeOp.FLOAT_MULT) {
+			return left.isEven() || right.isEven() ? EVEN : ODD;
+		}
+		else if (opcode == PcodeOp.INT_DIV || opcode == PcodeOp.FLOAT_DIV) {
+			if (left.isOdd()) {
+				return right.isOdd() ? ODD : EVEN;
+			}
+			return right.isOdd() ? EVEN : TOP;
+		}
+		else if (opcode == PcodeOp.INT_REM || opcode == PcodeOp.INT_SREM) {
+			return TOP;
+		}
+		else if (opcode == PcodeOp.INT_AND) {
+			if (left.equals(EVEN) || right.equals(EVEN)) {
+				return EVEN;
+			}
+			return ODD;
+		}
+		else if (opcode == PcodeOp.INT_OR) {
+			if (left.equals(ODD) || right.equals(ODD)) {
+				return ODD;
+			}
+			return EVEN;
+		}
+		else if (opcode == PcodeOp.INT_XOR) {
+			if (left.equals(right))
+				return EVEN;
+			return ODD;
+		}
+		return left;
+	}
+
+	@Override
+	public PcodeParity lubAux(
+			PcodeParity other)
+			throws SemanticException {
+		return TOP;
+	}
+
+	@Override
+	public boolean lessOrEqualAux(
+			PcodeParity other)
+			throws SemanticException {
+		return false;
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + parity;
+		return result;
+	}
+
+	@Override
+	public boolean equals(
+			Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		PcodeParity other = (PcodeParity) obj;
+		if (parity != other.parity) {
+			return false;
+		}
+		return true;
+	}
+
+	@Override
+	public ValueEnvironment<PcodeParity> assumeBinaryExpression(
+			ValueEnvironment<PcodeParity> environment,
+			BinaryOperator operator,
+			ValueExpression left,
+			ValueExpression right,
+			ProgramPoint src,
+			ProgramPoint dest,
+			SemanticOracle oracle)
+			throws SemanticException {
+		if (operator instanceof ComparisonEq) {
+			if (left instanceof Identifier) {
+				PcodeParity eval = eval(right, environment, src, oracle);
+				if (eval.isBottom()) {
+					return environment.bottom();
+				}
+				return environment.putState((Identifier) left, eval);
+			}
+			else if (right instanceof Identifier) {
+				PcodeParity eval = eval(left, environment, src, oracle);
+				if (eval.isBottom()) {
+					return environment.bottom();
+				}
+				return environment.putState((Identifier) right, eval);
+			}
+		}
+		return environment;
+	}
+
+	@Override
+	public PcodeParity getValue(RegisterValue rv) {
+		if (rv != null) {
+			BigInteger val = rv.getUnsignedValue();
+			if (val != null) {
+				return new PcodeParity((byte) (val.longValue() % 2 == 0 ? 3 : 2));
+			}
+		}
+		return top();
+	}
+
+}

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

@@ -0,0 +1,389 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import java.util.*;
+import java.util.Map.Entry;
+import java.util.function.Predicate;
+
+import org.apache.commons.collections4.CollectionUtils;
+
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.util.Msg;
+import it.unive.lisa.analysis.*;
+import it.unive.lisa.analysis.lattices.Satisfiability;
+import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
+import it.unive.lisa.analysis.value.ValueDomain;
+import it.unive.lisa.program.cfg.ProgramPoint;
+import it.unive.lisa.symbolic.value.*;
+import it.unive.lisa.util.numeric.MathNumber;
+import it.unive.lisa.util.representation.*;
+
+/**
+ * /** 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 PcodePentagon implements ValueDomain<PcodePentagon>, BaseLattice<PcodePentagon> {
+
+	/**
+	 * The interval environment.
+	 */
+	private final ValueEnvironment<PcodeInterval> intervals;
+
+	/**
+	 * The upper bounds environment.
+	 */
+	private final ValueEnvironment<PcodeUpperBounds> upperBounds;
+
+	/**
+	 * Builds the PcodePentagons.
+	 */
+	public PcodePentagon() {
+		this.intervals = new ValueEnvironment<>(new PcodeInterval()).top();
+		this.upperBounds = new ValueEnvironment<>(new PcodeUpperBounds(true)).top();
+	}
+
+	/**
+	 * Builds the pentagons.
+	 * 
+	 * @param intervals   the interval environment
+	 * @param upperBounds the upper bounds environment
+	 */
+	public PcodePentagon(
+			ValueEnvironment<PcodeInterval> intervals,
+			ValueEnvironment<PcodeUpperBounds> upperBounds) {
+		this.intervals = intervals;
+		this.upperBounds = upperBounds;
+	}
+
+	@Override
+	public PcodePentagon assign(
+			Identifier id,
+			ValueExpression expression,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		ValueEnvironment<PcodeUpperBounds> newBounds =
+			getUpperBounds().assign(id, expression, pp, oracle);
+		ValueEnvironment<PcodeInterval> newIntervals =
+			getIntervals().assign(id, expression, pp, oracle);
+
+		// we add the semantics for assignments here as we have access to the
+		// whole assignment
+		if (expression instanceof BinaryExpression) {
+			BinaryExpression be = (BinaryExpression) expression;
+			PcodeLocation ploc = (PcodeLocation) pp.getLocation();
+			PcodeOp op = ploc.op;
+			int opcode = op.getOpcode();
+			if (opcode == PcodeOp.INT_SUB || opcode == PcodeOp.FLOAT_SUB) {
+				if (be.getLeft() instanceof Identifier x) {
+					if (be.getRight() instanceof Constant) {
+						// r = x - c
+						newBounds = newBounds.putState(id, getUpperBounds().getState(x).add(x));
+					}
+					else if (be.getRight() instanceof Identifier) {
+						// r = x - y
+						Identifier y = (Identifier) be.getRight();
+
+						if (newBounds.getState(y).contains(x)) {
+							newIntervals = newIntervals.putState(id, newIntervals.getState(id)
+									.glb(new PcodeInterval(MathNumber.ZERO,
+										MathNumber.PLUS_INFINITY)));  // was MathNumber.ONE
+						}
+					}
+				}
+			}
+			else if ((opcode == PcodeOp.INT_REM || opcode == PcodeOp.INT_SREM) &&
+				be.getRight() instanceof Identifier d) {
+				// r = u % d
+				MathNumber low = getIntervals().getState(d).interval.getLow();
+				if (low.isPositive() || low.isZero()) {
+					newBounds =
+						newBounds.putState(id, new PcodeUpperBounds(Collections.singleton(d)));
+				}
+				else {
+					newBounds = newBounds.putState(id, new PcodeUpperBounds().top());
+				}
+			}
+		}
+
+		return new PcodePentagon(
+			newIntervals,
+			newBounds).closure();
+	}
+
+	@Override
+	public PcodePentagon smallStepSemantics(
+			ValueExpression expression,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		return new PcodePentagon(
+			getIntervals().smallStepSemantics(expression, pp, oracle),
+			getUpperBounds().smallStepSemantics(expression, pp, oracle));
+	}
+
+	@Override
+	public PcodePentagon assume(
+			ValueExpression expression,
+			ProgramPoint src,
+			ProgramPoint dest,
+			SemanticOracle oracle)
+			throws SemanticException {
+		return new PcodePentagon(
+			getIntervals().assume(expression, src, dest, oracle),
+			getUpperBounds().assume(expression, src, dest, oracle));
+	}
+
+	@Override
+	public PcodePentagon forgetIdentifier(
+			Identifier id)
+			throws SemanticException {
+		return new PcodePentagon(
+			getIntervals().forgetIdentifier(id),
+			getUpperBounds().forgetIdentifier(id));
+	}
+
+	@Override
+	public PcodePentagon forgetIdentifiersIf(
+			Predicate<Identifier> test)
+			throws SemanticException {
+		return new PcodePentagon(
+			getIntervals().forgetIdentifiersIf(test),
+			getUpperBounds().forgetIdentifiersIf(test));
+	}
+
+	@Override
+	public Satisfiability satisfies(
+			ValueExpression expression,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		return getIntervals().satisfies(expression, pp, oracle)
+				.glb(getUpperBounds().satisfies(expression, pp, oracle));
+	}
+
+	@Override
+	public PcodePentagon pushScope(
+			ScopeToken token)
+			throws SemanticException {
+		return new PcodePentagon(getIntervals().pushScope(token),
+			getUpperBounds().pushScope(token));
+	}
+
+	@Override
+	public PcodePentagon popScope(
+			ScopeToken token)
+			throws SemanticException {
+		return new PcodePentagon(getIntervals().popScope(token), getUpperBounds().popScope(token));
+	}
+
+	@Override
+	public StructuredRepresentation representation() {
+		if (isTop())
+			return Lattice.topRepresentation();
+		if (isBottom())
+			return Lattice.bottomRepresentation();
+		Map<StructuredRepresentation, StructuredRepresentation> mapping = new HashMap<>();
+		for (Identifier id : CollectionUtils.union(getIntervals().getKeys(),
+			getUpperBounds().getKeys())) {
+			mapping.put(new StringRepresentation(id),
+				new StringRepresentation(getIntervals().getState(id).toString() + ", " +
+					getUpperBounds().getState(id).representation()));
+		}
+		return new MapRepresentation(mapping);
+	}
+
+	@Override
+	public PcodePentagon top() {
+		return new PcodePentagon(getIntervals().top(), getUpperBounds().top());
+	}
+
+	@Override
+	public boolean isTop() {
+		return getIntervals().isTop() && getUpperBounds().isTop();
+	}
+
+	@Override
+	public PcodePentagon bottom() {
+		return new PcodePentagon(getIntervals().bottom(), getUpperBounds().bottom());
+	}
+
+	@Override
+	public boolean isBottom() {
+		return getIntervals().isBottom() && getUpperBounds().isBottom();
+	}
+
+	private PcodePentagon closure() throws SemanticException {
+		ValueEnvironment<PcodeUpperBounds> newBounds = new ValueEnvironment<PcodeUpperBounds>(
+			getUpperBounds().lattice, getUpperBounds().getMap());
+
+		for (Identifier id1 : getIntervals().getKeys()) {
+			Set<Identifier> closure = new HashSet<>();
+			for (Identifier id2 : getIntervals().getKeys()) {
+				if (!id1.equals(id2)) {
+					PcodeInterval state1 = getIntervals().getState(id1);
+					LongInterval interval1 = state1.interval;
+					PcodeInterval state2 = getIntervals().getState(id2);
+					LongInterval interval2 = state2.interval;
+					if (interval1 != null && interval2 != null) {
+						if (interval1.getHigh().compareTo(interval2.getLow()) < 0) {
+							closure.add(id2);
+						}
+					}
+					else {
+						Msg.error(this, "Unexpected combination: " + state1 + " : " + state2);
+					}
+				}
+			}
+			if (!closure.isEmpty()) {
+				// glb is the union
+				newBounds = newBounds.putState(id1,
+					newBounds.getState(id1).glb(new PcodeUpperBounds(closure)));
+			}
+
+		}
+
+		return new PcodePentagon(getIntervals(), newBounds);
+	}
+
+	@Override
+	public PcodePentagon lubAux(
+			PcodePentagon other)
+			throws SemanticException {
+		ValueEnvironment<PcodeUpperBounds> newBounds = getUpperBounds().lub(other.getUpperBounds());
+		for (Entry<Identifier, PcodeUpperBounds> entry : getUpperBounds()) {
+			Set<Identifier> closure = new HashSet<>();
+			for (Identifier bound : entry.getValue()) {
+				PcodeInterval entryState = other.getIntervals().getState(entry.getKey());
+				LongInterval entryInterval = entryState.interval;
+				PcodeInterval boundsState = other.getIntervals().getState(bound);
+				LongInterval boundsInterval = boundsState.interval;
+				if (entryInterval != null && boundsInterval != null) {
+					if (entryInterval.getHigh().compareTo(boundsInterval.getLow()) < 0) {
+						closure.add(bound);
+					}
+				}
+				else {
+					Msg.error(this, "Unexpected combination: " + entryState + " : " + boundsState);
+				}
+			}
+			if (!closure.isEmpty()) {
+				// glb is the union
+				newBounds = newBounds.putState(entry.getKey(),
+					newBounds.getState(entry.getKey()).glb(new PcodeUpperBounds(closure)));
+			}
+		}
+
+		for (Entry<Identifier, PcodeUpperBounds> entry : other.getUpperBounds()) {
+			Set<Identifier> closure = new HashSet<>();
+			for (Identifier bound : entry.getValue()) {
+				PcodeInterval entryState = getIntervals().getState(entry.getKey());
+				LongInterval entryInterval = entryState.interval;
+				PcodeInterval boundsState = getIntervals().getState(bound);
+				LongInterval boundsInterval = boundsState.interval;
+				if (entryInterval != null && boundsInterval != null) {
+					if (entryInterval.getHigh().compareTo(boundsInterval.getLow()) < 0) {
+						closure.add(bound);
+					}
+				}
+				else {
+					Msg.error(this, "Unexpected combination: " + entryState + " : " + boundsState);
+				}
+			}
+			if (!closure.isEmpty()) {
+				// glb is the union
+				newBounds = newBounds.putState(entry.getKey(),
+					newBounds.getState(entry.getKey()).glb(new PcodeUpperBounds(closure)));
+			}
+		}
+
+		return new PcodePentagon(getIntervals().lub(other.getIntervals()), newBounds);
+	}
+
+	@Override
+	public PcodePentagon wideningAux(
+			PcodePentagon other)
+			throws SemanticException {
+		return new PcodePentagon(getIntervals().widening(other.getIntervals()),
+			getUpperBounds().widening(other.getUpperBounds()));
+	}
+
+	@Override
+	public boolean lessOrEqualAux(
+			PcodePentagon other)
+			throws SemanticException {
+		if (!getIntervals().lessOrEqual(other.getIntervals())) {
+			return false;
+		}
+		for (Entry<Identifier, PcodeUpperBounds> entry : other.getUpperBounds()) {
+			for (Identifier bound : entry.getValue()) {
+				if (!(getUpperBounds().getState(entry.getKey()).contains(bound) ||
+					getIntervals().getState(entry.getKey()).interval.getHigh()
+							.compareTo(getIntervals().getState(bound).interval.getLow()) < 0)) {
+					return false;
+				}
+			}
+		}
+
+		return true;
+	}
+
+	@Override
+	public int hashCode() {
+		return Objects.hash(getIntervals(), getUpperBounds());
+	}
+
+	@Override
+	public boolean equals(
+			Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		PcodePentagon other = (PcodePentagon) obj;
+		return Objects.equals(getIntervals(), other.getIntervals()) &&
+			Objects.equals(getUpperBounds(), other.getUpperBounds());
+	}
+
+	@Override
+	public String toString() {
+		return representation().toString();
+	}
+
+	@Override
+	public boolean knowsIdentifier(
+			Identifier id) {
+		return getIntervals().knowsIdentifier(id) || getUpperBounds().knowsIdentifier(id);
+	}
+
+	public ValueEnvironment<PcodeInterval> getIntervals() {
+		return intervals;
+	}
+
+	public ValueEnvironment<PcodeUpperBounds> getUpperBounds() {
+		return upperBounds;
+	}
+}

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

@@ -0,0 +1,187 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import it.unive.lisa.analysis.*;
+import it.unive.lisa.analysis.taint.BaseTaint;
+import it.unive.lisa.program.annotations.Annotation;
+import it.unive.lisa.program.annotations.Annotations;
+import it.unive.lisa.program.cfg.ProgramPoint;
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.util.representation.StringRepresentation;
+import it.unive.lisa.util.representation.StructuredRepresentation;
+
+/**
+ * A {@link BaseTaint} implementation with only two level of taintedness: clean
+ * and tainted. As such, this class distinguishes values that are always clean
+ * from values that are tainted in at least one execution path.
+ * 
+ * <p>
+ * Modified to handle pcode from original source written by:
+ * <p>
+ * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
+ */
+public class PcodeTaint extends BaseTaint<PcodeTaint> {
+
+	private static final PcodeTaint TAINTED = new PcodeTaint(true);
+
+	private static final PcodeTaint CLEAN = new PcodeTaint(false);
+
+	private static final PcodeTaint BOTTOM = new PcodeTaint(null);
+
+	private final Boolean taint;
+
+	/**
+	 * Builds a new instance of taint.
+	 */
+	public PcodeTaint() {
+		this(true);
+	}
+
+	public PcodeTaint(
+			Boolean taint) {
+		this.taint = taint;
+	}
+
+	@Override
+	protected PcodeTaint tainted() {
+		return TAINTED;
+	}
+
+	@Override
+	protected PcodeTaint clean() {
+		return CLEAN;
+	}
+
+	@Override
+	public boolean isPossiblyTainted() {
+		return this == TAINTED;
+	}
+
+	@Override
+	public boolean isAlwaysTainted() {
+		return false;
+	}
+
+	@Override
+	public StructuredRepresentation representation() {
+		if (this == BOTTOM) {
+			return Lattice.bottomRepresentation();
+		}
+		return this == TAINTED ? new StringRepresentation("#") : new StringRepresentation("_");
+	}
+
+	@Override
+	public PcodeTaint top() {
+		return CLEAN;
+	}
+
+	@Override
+	public PcodeTaint bottom() {
+		return BOTTOM;
+	}
+
+	@Override
+	protected PcodeTaint defaultApprox(
+			Identifier id,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		Annotations annots = id.getAnnotations();
+		if (annots.isEmpty()) {
+			return super.defaultApprox(id, pp, oracle);
+		}
+
+		if (pp.getLocation() instanceof PcodeLocation ploc) {
+			for (Annotation annotation : annots) {
+				String name = annotation.getAnnotationName();
+				if (name.contains("@" + ploc.getAddress())) {
+					if (name.contains("Tainted")) {
+						return tainted();
+					}
+
+					if (name.contains("Clean")) {
+						return clean();
+					}
+				}
+			}
+		}
+
+		return bottom();
+	}
+
+	@Override
+	public PcodeTaint lub(PcodeTaint other) throws SemanticException {
+		if (other == null || other.isBottom() || this.isTop() || this == other ||
+			this.equals(other)) {
+			return this;
+		}
+
+		if (this.isBottom()) { // || other.isTop()) 
+			return other;
+		}
+
+		return lubAux(other);
+	}
+
+	@Override
+	public PcodeTaint lubAux(
+			PcodeTaint other)
+			throws SemanticException {
+		return TAINTED;
+	}
+
+	@Override
+	public PcodeTaint wideningAux(
+			PcodeTaint other)
+			throws SemanticException {
+		return TAINTED; // should never happen
+	}
+
+	@Override
+	public boolean lessOrEqualAux(
+			PcodeTaint other)
+			throws SemanticException {
+		return false; // should never happen
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((taint == null) ? 0 : taint.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(
+			Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		PcodeTaint other = (PcodeTaint) obj;
+		if (taint == null) {
+			if (other.taint != null) {
+				return false;
+			}
+		}
+		else if (!taint.equals(other.taint)) {
+			return false;
+		}
+		return true;
+	}
+
+	@Override
+	public String toString() {
+		return representation().toString();
+	}
+
+}

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

@@ -0,0 +1,210 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import it.unive.lisa.analysis.*;
+import it.unive.lisa.analysis.taint.BaseTaint;
+import it.unive.lisa.program.annotations.Annotation;
+import it.unive.lisa.program.annotations.Annotations;
+import it.unive.lisa.program.cfg.ProgramPoint;
+import it.unive.lisa.symbolic.value.Identifier;
+import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
+import it.unive.lisa.symbolic.value.operator.ternary.TernaryOperator;
+import it.unive.lisa.util.representation.StringRepresentation;
+import it.unive.lisa.util.representation.StructuredRepresentation;
+
+/**
+ * A {@link BaseTaint} implementation with three level of taintedness: clean,
+ * tainted and top. As such, this class distinguishes values that are always
+ * clean, always tainted, or tainted in at least one execution path.
+ * 
+ * <p>
+ * Modified to handle pcode from original source written by:
+ * <p>
+ * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
+ */
+public class PcodeThreeLevelTaint extends BaseTaint<PcodeThreeLevelTaint> {
+
+	private static final PcodeThreeLevelTaint TOP = new PcodeThreeLevelTaint((byte) 3);
+	private static final PcodeThreeLevelTaint TAINTED = new PcodeThreeLevelTaint((byte) 2);
+	private static final PcodeThreeLevelTaint CLEAN = new PcodeThreeLevelTaint((byte) 1);
+	private static final PcodeThreeLevelTaint BOTTOM = new PcodeThreeLevelTaint((byte) 0);
+
+	private final byte taint;
+
+	/**
+	 * Builds a new instance of taint.
+	 */
+	public PcodeThreeLevelTaint() {
+		this((byte) 3);
+	}
+
+	private PcodeThreeLevelTaint(
+			byte v) {
+		this.taint = v;
+	}
+
+	@Override
+	protected PcodeThreeLevelTaint tainted() {
+		return TAINTED;
+	}
+
+	@Override
+	protected PcodeThreeLevelTaint clean() {
+		return CLEAN;
+	}
+
+	@Override
+	public boolean isAlwaysTainted() {
+		return this == TAINTED;
+	}
+
+	@Override
+	public boolean isPossiblyTainted() {
+		return this == TOP;
+	}
+
+	@Override
+	public StructuredRepresentation representation() {
+		return this == BOTTOM ? Lattice.bottomRepresentation()
+				: this == CLEAN ? new StringRepresentation("_")
+						: this == TAINTED ? new StringRepresentation("#")
+								: Lattice.topRepresentation();
+	}
+
+	@Override
+	public PcodeThreeLevelTaint top() {
+		return TOP;
+	}
+
+	@Override
+	public PcodeThreeLevelTaint bottom() {
+		return BOTTOM;
+	}
+
+	@Override
+	protected PcodeThreeLevelTaint defaultApprox(
+			Identifier id,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		Annotations annots = id.getAnnotations();
+		if (annots.isEmpty()) {
+			return super.defaultApprox(id, pp, oracle);
+		}
+
+		if (pp.getLocation() instanceof PcodeLocation ploc) {
+			for (Annotation annotation : annots) {
+				String name = annotation.getAnnotationName();
+				if (name.contains("@" + ploc.getAddress())) {
+					if (name.contains("Tainted")) {
+						return tainted();
+					}
+
+					if (name.contains("Clean")) {
+						return clean();
+					}
+				}
+			}
+		}
+
+		return bottom();
+	}
+
+	@Override
+	public PcodeThreeLevelTaint evalBinaryExpression(
+			BinaryOperator operator,
+			PcodeThreeLevelTaint left,
+			PcodeThreeLevelTaint right,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		if (left == TAINTED || right == TAINTED) {
+			return TAINTED;
+		}
+
+		if (left == TOP || right == TOP) {
+			return TOP;
+		}
+
+		return CLEAN;
+	}
+
+	@Override
+	public PcodeThreeLevelTaint evalTernaryExpression(
+			TernaryOperator operator,
+			PcodeThreeLevelTaint left,
+			PcodeThreeLevelTaint middle,
+			PcodeThreeLevelTaint right,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		if (left == TAINTED || right == TAINTED || middle == TAINTED) {
+			return TAINTED;
+		}
+
+		if (left == TOP || right == TOP || middle == TOP) {
+			return TOP;
+		}
+
+		return CLEAN;
+	}
+
+	@Override
+	public PcodeThreeLevelTaint lubAux(
+			PcodeThreeLevelTaint other)
+			throws SemanticException {
+		// only happens with clean and tainted, that are not comparable
+		return TOP;
+	}
+
+	@Override
+	public PcodeThreeLevelTaint wideningAux(
+			PcodeThreeLevelTaint other)
+			throws SemanticException {
+		// only happens with clean and tainted, that are not comparable
+		return TOP;
+	}
+
+	@Override
+	public boolean lessOrEqualAux(
+			PcodeThreeLevelTaint other)
+			throws SemanticException {
+		// only happens with clean and tainted, that are not comparable
+		return false;
+	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + taint;
+		return result;
+	}
+
+	@Override
+	public boolean equals(
+			Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		PcodeThreeLevelTaint other = (PcodeThreeLevelTaint) obj;
+		if (taint != other.taint) {
+			return false;
+		}
+		return true;
+	}
+
+	@Override
+	public String toString() {
+		return representation().toString();
+	}
+}

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

@@ -0,0 +1,245 @@
+/* ###
+ * IP: MIT
+ */
+package ghidra.lisa.pcode.analyses;
+
+import java.util.*;
+
+import ghidra.lisa.pcode.statements.PcodeBinaryOperator;
+import ghidra.program.model.lang.RegisterValue;
+import it.unive.lisa.analysis.*;
+import it.unive.lisa.analysis.nonrelational.value.BaseNonRelationalValueDomain;
+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.ValueExpression;
+import it.unive.lisa.symbolic.value.operator.binary.*;
+import it.unive.lisa.util.representation.*;
+
+/**
+ * The upper bounds abstract domain. It is implemented as a
+ * {@link BaseNonRelationalValueDomain}.
+ * 
+ * <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>
+ */
+public class PcodeUpperBounds
+		implements PcodeNonRelationalValueDomain<PcodeUpperBounds>, Iterable<Identifier> {
+
+	/**
+	 * The abstract top element.
+	 */
+	private static final PcodeUpperBounds TOP = new PcodeUpperBounds(true);
+
+	/**
+	 * The abstract bottom element.
+	 */
+	private static final PcodeUpperBounds BOTTOM = new PcodeUpperBounds(new TreeSet<>());
+
+	/**
+	 * The flag to set abstract top state.
+	 */
+	private final boolean isTop;
+
+	/**
+	 * The set containing the bounds.
+	 */
+	private final Set<Identifier> bounds;
+
+	/**
+	 * Builds the upper bounds.
+	 */
+	public PcodeUpperBounds() {
+		this(true);
+	}
+
+	/**
+	 * Builds the upper bounds.
+	 * 
+	 * @param isTop {@code true} if the abstract domain is top; otherwise
+	 *                  {@code false}.
+	 */
+	public PcodeUpperBounds(
+			boolean isTop) {
+		this.bounds = null;
+		this.isTop = isTop;
+	}
+
+	/**
+	 * Builds the upper bounds.
+	 * 
+	 * @param bounds the bounds to set
+	 */
+	public PcodeUpperBounds(
+			Set<Identifier> bounds) {
+		this.bounds = bounds;
+		this.isTop = false;
+	}
+
+	@Override
+	public StructuredRepresentation representation() {
+		if (isTop()) {
+			return new StringRepresentation("{}");
+		}
+		if (isBottom()) {
+			return Lattice.bottomRepresentation();
+		}
+		return new SetRepresentation(bounds, StringRepresentation::new);
+	}
+
+	@Override
+	public PcodeUpperBounds top() {
+		return TOP;
+	}
+
+	@Override
+	public PcodeUpperBounds bottom() {
+		return BOTTOM;
+	}
+
+	@Override
+	public boolean isBottom() {
+		return !isTop && bounds.isEmpty();
+	}
+
+	@Override
+	public PcodeUpperBounds lubAux(
+			PcodeUpperBounds other)
+			throws SemanticException {
+		Set<Identifier> lub = new HashSet<>(bounds);
+		lub.retainAll(other.bounds);
+		return new PcodeUpperBounds(lub);
+	}
+
+	@Override
+	public PcodeUpperBounds glbAux(
+			PcodeUpperBounds other)
+			throws SemanticException {
+		Set<Identifier> lub = new HashSet<>(bounds);
+		lub.addAll(other.bounds);
+		return new PcodeUpperBounds(lub);
+	}
+
+	@Override
+	public boolean lessOrEqualAux(
+			PcodeUpperBounds other)
+			throws SemanticException {
+		return bounds.containsAll(other.bounds);
+	}
+
+	@Override
+	public PcodeUpperBounds wideningAux(
+			PcodeUpperBounds other)
+			throws SemanticException {
+		return other.bounds.containsAll(bounds) ? other : TOP;
+	}
+
+	@Override
+	public boolean equals(
+			Object obj) {
+		if (this == obj) {
+			return true;
+		}
+		if (obj == null) {
+			return false;
+		}
+		if (getClass() != obj.getClass()) {
+			return false;
+		}
+		PcodeUpperBounds other = (PcodeUpperBounds) obj;
+		return Objects.equals(bounds, other.bounds) && isTop == other.isTop;
+	}
+
+	@Override
+	public int hashCode() {
+		return Objects.hash(bounds, isTop);
+	}
+
+	@Override
+	public ValueEnvironment<PcodeUpperBounds> assumeBinaryExpression(
+			ValueEnvironment<PcodeUpperBounds> environment,
+			BinaryOperator operator,
+			ValueExpression left,
+			ValueExpression right,
+			ProgramPoint src,
+			ProgramPoint dest,
+			SemanticOracle oracle)
+			throws SemanticException {
+		if (!(left instanceof Identifier x && right instanceof Identifier y)) {
+			return environment;
+		}
+
+		// glb is the union!
+
+		if (!(operator instanceof PcodeBinaryOperator)) {
+			if (operator instanceof ComparisonEq) {
+				// x == y
+				PcodeUpperBounds set = environment.getState(x).glb(environment.getState(y));
+				return environment.putState(x, set).putState(y, set);
+			}
+
+			if (operator instanceof ComparisonLt) {
+				// x < y
+				PcodeUpperBounds set = environment.getState(x)
+						.glb(environment.getState(y))
+						.glb(new PcodeUpperBounds(Collections.singleton(y)));
+				return environment.putState(x, set);
+			}
+
+			if (operator instanceof ComparisonLe) {
+				// x <= y
+				PcodeUpperBounds set = environment.getState(x).glb(environment.getState(y));
+				return environment.putState(x, set);
+			}
+		}
+
+		return environment;
+	}
+
+	@Override
+	public Iterator<Identifier> iterator() {
+		if (bounds == null) {
+			return Collections.emptyIterator();
+		}
+		return bounds.iterator();
+	}
+
+	/**
+	 * Checks if this bounds contains a specified identifier of a program
+	 * variable.
+	 * 
+	 * @param id the identifier to check
+	 * 
+	 * @return {@code true} if this bounds contains the specified identifier;
+	 *             otherwise, {@code false}.
+	 */
+	public boolean contains(
+			Identifier id) {
+		return bounds != null && bounds.contains(id);
+	}
+
+	/**
+	 * Adds the specified identifier of a program variable in the bounds.
+	 * 
+	 * @param id the identifier to add in the bounds.
+	 * 
+	 * @return the updated bounds.
+	 */
+	public PcodeUpperBounds add(
+			Identifier id) {
+		Set<Identifier> res = new HashSet<>();
+		if (!isTop() && !isBottom()) {
+			res.addAll(bounds);
+		}
+		res.add(id);
+		return new PcodeUpperBounds(res);
+	}
+
+	@Override
+	public PcodeUpperBounds getValue(RegisterValue rv) {
+		return top();
+	}
+}

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

@@ -0,0 +1 @@
+Note: files in this directory are lightly-modified versions of analyses from https://github.com/lisa-analyzer, and, as such, are included with their original comments, author credits, and MIT License.

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/BinaryExprContext.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.contexts;
+
+import ghidra.lisa.pcode.locations.PcodeLocation;
+import ghidra.program.model.pcode.PcodeOp;
+import it.unive.lisa.program.cfg.CodeLocation;
+
+public class BinaryExprContext {
+
+	public PcodeOp op;
+	public VarnodeContext left;
+	public VarnodeContext right;
+
+	public BinaryExprContext(PcodeContext ctx) {
+		this.op = ctx.op;
+		left = new VarnodeContext(op.getInput(0));
+		right = new VarnodeContext(op.getInput(1));
+	}
+
+	// Used for TypeConv
+	public BinaryExprContext(StatementContext ctx) {
+		this.op = ctx.op;
+		left = ctx.target();
+		right = new VarnodeContext(op.getInput(0));
+	}
+
+	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/CallContext.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 ghidra.program.model.address.Address;
+import ghidra.program.model.listing.Function;
+import ghidra.program.model.pcode.PcodeOp;
+import it.unive.lisa.program.cfg.statement.call.Call.CallType;
+
+public class CallContext extends PcodeContext {
+
+	private Function callee = null;
+	public VarnodeContext left;
+	private boolean isTarget;
+
+	public CallContext(PcodeOp op, UnitContext ctx) {
+		super(op);
+		this.op = op;
+		Address address = op.getInput(0).getAddress();
+		Function caller = ctx.function();
+		left = new SymbolVarnodeContext(address);
+		if (address.getAddressSpace().isMemorySpace()) {
+			callee = caller.getProgram().getFunctionManager().getFunctionAt(address);
+			if (callee != null) {
+				left = new SymbolVarnodeContext(callee.getName(), address);
+			}
+		}
+	}
+
+	public String getText() {
+		return op.toString();
+	}
+
+	public String getCalleeName() {
+		return callee == null ? "UNKNOWN" : callee.getName();
+	}
+
+	public Function function() {
+		return callee;
+	}
+
+	public CallType type() {
+		if (callee == null || callee.isThunk()) {
+			return CallType.UNKNOWN;
+		}
+		if (op.getInput(0).getAddress().getAddressSpace().isMemorySpace()) {
+			return CallType.STATIC;
+		}
+		return CallType.UNKNOWN;
+	}
+
+	public boolean isTarget() {
+		return isTarget;
+	}
+
+	public void setIsTarget(boolean isTarget) {
+		this.isTarget = isTarget;
+	}
+
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/contexts/ConditionContext.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 ghidra.program.model.pcode.PcodeOp;
+
+public class ConditionContext extends PcodeContext {
+
+	public ConditionContext(PcodeOp op) {
+		super(op);
+	}
+
+	public VarnodeContext expression() {
+		// opcode should be CBRANCH
+		assert (op.getInputs().length < 2);
+		return new VarnodeContext(op.getInput(1));
+	}
+
+}

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

@@ -0,0 +1,67 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.pcode.contexts;
+
+import java.util.*;
+
+import ghidra.lisa.pcode.locations.InstLocation;
+import ghidra.program.model.address.Address;
+import ghidra.program.model.listing.*;
+import ghidra.program.model.pcode.PcodeOp;
+import it.unive.lisa.program.cfg.CodeLocation;
+
+public class InstructionContext {
+
+	private Function function;
+	private Instruction inst;
+	private List<StatementContext> ops;
+	private InstLocation loc;
+
+	public InstructionContext(Function function, Instruction inst) {
+		this.function = function;
+		this.inst = inst;
+		ops = new ArrayList<>();
+		for (PcodeOp op : inst.getPcode()) {
+			StatementContext ctx = new StatementContext(inst, op);
+			ops.add(ctx);
+		}
+		loc = new InstLocation(function, inst.getAddress());
+	}
+
+	public Collection<StatementContext> getPcodeOps() {
+		return ops;
+	}
+
+	public StatementContext getPcodeOp(int i) {
+		return ops.get(i);
+	}
+
+	public Instruction getInstruction() {
+		return inst;
+	}
+
+	public InstructionContext next() {
+		Listing listing = inst.getProgram().getListing();
+		Address nextAddress = inst.getAddress().add(inst.getLength());
+		Instruction next = listing.getInstructionAt(nextAddress);
+		return next == null ? null : new InstructionContext(function, next);
+	}
+
+	public CodeLocation location() {
+		return loc;
+	}
+
+}

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

@@ -0,0 +1,36 @@
+/* ###
+ * 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.program.model.address.AddressFactory;
+import ghidra.program.model.address.AddressSpace;
+
+public class MemLocContext extends VarnodeContext {
+
+	private AddressSpace space;
+
+	public MemLocContext(StatementContext ctx) {
+		super(ctx.getOp().getInput(1));
+		AddressFactory addressFactory = ctx.inst.getProgram().getAddressFactory();
+		space = addressFactory.getAddressSpace((int) ctx.getOp().getInput(0).getOffset());
+	}
+
+	@Override
+	public String getText() {
+		return space.getName() + "@" + vn.getAddress().toString();
+	}
+
+}

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

@@ -0,0 +1,56 @@
+/* ###
+ * 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.SyntheticLocation;
+import it.unive.lisa.program.cfg.CodeLocation;
+
+public class PcodeContext {
+
+	protected PcodeOp op;
+
+	public PcodeContext(PcodeOp op) {
+		this.op = op;
+	}
+
+	public PcodeOp getOp() {
+		return op;
+	}
+
+	public CodeLocation location() {
+		if (op == null) {
+			return SyntheticLocation.INSTANCE;
+		}
+		return new PcodeLocation(op);
+	}
+
+	public VarnodeContext basicExpr() {
+		if (op.getNumInputs() == 1) {
+			return new VarnodeContext(op.getInput(0));
+		}
+		return null;
+	}
+
+	public int opcode() {
+		return op.getOpcode();
+	}
+
+	public int getNumInputs() {
+		return op.getNumInputs();
+	}
+}

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

@@ -0,0 +1,141 @@
+/* ###
+ * 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.Address;
+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;
+	public VarDefContext left;
+	public PcodeContext right;
+
+	public StatementContext(Instruction inst, PcodeOp op) {
+		super(op);
+		this.inst = inst;
+		if (op != null) {
+			this.opcode = op.getOpcode();
+			if (op.getOutput() != null) {
+				left = new VarDefContext(op, op.getOutput());
+			}
+			else {
+				left = new VarDefContext(op, op.getInput(2));
+			}
+			right = new PcodeContext(op);
+		}
+	}
+
+	public VarDefContext target() {
+		return left;
+	}
+
+	public PcodeContext expression() {
+		return right;
+	}
+
+	public ConditionContext condition() {
+		return new ConditionContext(op);
+	}
+
+	public boolean isRet() {
+		return opcode == PcodeOp.RETURN;
+	}
+
+	public boolean isBranch() {
+		return opcode == PcodeOp.BRANCH || opcode == PcodeOp.BRANCHIND || opcode == PcodeOp.CBRANCH;
+	}
+
+	public boolean isConditional() {
+		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;
+	}
+
+}

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

@@ -0,0 +1,59 @@
+/* ###
+ * 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.program.model.address.Address;
+
+public class SymbolVarnodeContext extends VarnodeContext {
+
+	private String context;
+	private int size;
+
+	/*
+	 * This class is essentially a dummy context for the case where the varnode's id is a memory address
+	 */
+	public SymbolVarnodeContext(String name, Address context) {
+		this(context);
+		this.context = name;
+	}
+
+	public SymbolVarnodeContext(Address context) {
+		super(null);
+		this.context = context.toString();
+		size = context.getPointerSize();
+	}
+
+	@Override
+	public boolean isConstant() {
+		return false;
+	}
+
+	@Override
+	public int getSize() {
+		return size;
+	}
+
+	@Override
+	public long getOffset() {
+		return 0;
+	}
+
+	@Override
+	public String getText() {
+		return context;
+	}
+
+}

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

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

@@ -0,0 +1,88 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.pcode.contexts;
+
+import ghidra.lisa.pcode.PcodeFrontend;
+import ghidra.lisa.pcode.locations.InstLocation;
+import ghidra.program.model.address.Address;
+import ghidra.program.model.listing.*;
+import it.unive.lisa.program.CodeUnit;
+import it.unive.lisa.program.Program;
+import it.unive.lisa.program.SyntheticLocation;
+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();
+	}
+
+	public UnitContext(PcodeFrontend frontend, Program program, Function f, Address entry) {
+		this.frontend = frontend;
+		this.function = f;
+		unit = new CodeUnit(SyntheticLocation.INSTANCE, program,
+			f.getName() + ":" + f.getEntryPoint());
+		start = entry;
+	}
+
+	public PcodeFrontend getFrontend() {
+		return frontend;
+	}
+
+	public CodeUnit unit() {
+		return unit;
+	}
+
+	public String getText() {
+		return function.getName();
+	}
+
+	public boolean isFinal() {
+		return false;
+	}
+
+	public Listing getListing() {
+		return function.getProgram().getListing();
+	}
+
+	public CodeLocation location() {
+		return new InstLocation(function, start);
+	}
+
+	public Function function() {
+		return function;
+	}
+
+	public InstructionContext entry() {
+		Instruction inst = getListing().getInstructionAt(start);
+		if (inst == null) {
+			inst = getListing().getInstructionAfter(start);
+		}
+		return inst == null ? null : new InstructionContext(function, inst);
+	}
+
+	public boolean contains(Address target) {
+		return function.getBody().contains(target);
+	}
+}

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

@@ -0,0 +1,44 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.pcode.contexts;
+
+import ghidra.program.model.pcode.PcodeOp;
+import ghidra.program.model.pcode.Varnode;
+
+public class VarDefContext extends VarnodeContext {
+
+	private PcodeOp op;
+
+	public VarDefContext(PcodeOp op, Varnode vn) {
+		super(vn);
+		this.op = op;
+	}
+
+	@Override
+	public boolean isConstant() {
+		return false;
+	}
+
+	public PcodeOp getOp() {
+		return op;
+	}
+
+	@Override
+	public String getText() {
+		return vn.getAddress().toString();
+	}
+
+}

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

@@ -0,0 +1,44 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.pcode.contexts;
+
+import ghidra.program.model.pcode.Varnode;
+
+public class VarnodeContext {
+
+	protected Varnode vn;
+
+	public VarnodeContext(Varnode vn) {
+		this.vn = vn;
+	}
+
+	public boolean isConstant() {
+		return vn.isConstant();
+	}
+
+	public int getSize() {
+		return vn.getSize();
+	}
+
+	public long getOffset() {
+		return vn.getOffset();
+	}
+
+	public String getText() {
+		return vn.getAddress().toString();
+	}
+
+}

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

@@ -0,0 +1,77 @@
+/* ###
+ * 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.BinaryExprContext;
+import ghidra.lisa.pcode.statements.PcodeBinaryOperator;
+import ghidra.program.model.pcode.PcodeOp;
+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.BinaryExpression;
+import it.unive.lisa.symbolic.value.operator.binary.*;
+
+public class PcodeBinaryExpression extends it.unive.lisa.program.cfg.statement.BinaryExpression {
+
+	private BinaryOperator operator;
+
+	public PcodeBinaryExpression(
+			CFG cfg,
+			BinaryExprContext ctx,
+			Expression left,
+			Expression right) {
+		super(cfg, ctx.location(), ctx.mnemonic(),
+			cfg.getDescriptor().getUnit().getProgram().getTypes().getIntegerType(), left, right);
+
+		this.operator = switch (ctx.op.getOpcode()) {
+			case PcodeOp.BOOL_AND -> LogicalAnd.INSTANCE;
+			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;
+			default -> new PcodeBinaryOperator(ctx.op);
+		};
+	}
+
+	@Override
+	protected int compareSameClassAndParams(
+			Statement o) {
+		return 0; // no extra fields to compare
+	}
+
+	@Override
+	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,
+				operator,
+				getLocation()),
+			this);
+	}
+}

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

@@ -0,0 +1,128 @@
+/* ###
+ * 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 java.util.HashSet;
+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;
+import it.unive.lisa.analysis.value.ValueDomain;
+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.call.UnresolvedCall;
+import it.unive.lisa.symbolic.value.Variable;
+
+public class PcodeCallExpression extends UnresolvedCall {
+
+	private Function function;
+	private Set<Varnode> unaffected = new HashSet<>();
+	private Set<Varnode> killedByCall = new HashSet<>();
+
+	public PcodeCallExpression(
+			CFG cfg,
+			CallContext ctx,
+			Expression expression) {
+		super(cfg, ctx.location(), ctx.type(), null, ctx.getCalleeName(), expression);
+		function = ctx.function();
+		if (function != null) {
+			PrototypeModel callingConvention = function.getCallingConvention();
+			if (callingConvention != null) {
+				Varnode[] unaffectedList = callingConvention.getUnaffectedList();
+				for (Varnode varnode : unaffectedList) {
+					unaffected.add(varnode);
+				}
+				Varnode[] killedByCallList = callingConvention.getKilledByCallList();
+				for (Varnode varnode : killedByCallList) {
+					killedByCall.add(varnode);
+				}
+			}
+		}
+	}
+
+	@SuppressWarnings("unchecked")
+	@Override
+	public <A extends AbstractState<A>> AnalysisState<A> forwardSemantics(
+			AnalysisState<A> entryState,
+			InterproceduralAnalysis<A> interprocedural,
+			StatementStore<A> expressions)
+			throws SemanticException {
+
+		// TODO: This triggers the processing of the callee, but we effectively clears the state.
+		//  We're using the slightly-sanitized entry state instead.  Quite possible, the return
+		//  value from the function is being dropped here - not clear how this works.
+		super.forwardSemantics(entryState, interprocedural, expressions);
+
+		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) {
+				if (vEnv.function == null) {
+					return entryState;
+				}
+				for (Object key : vEnv.function.keySet()) {
+					Object val = vEnv.function.get(key);
+					if (key instanceof Variable var && val instanceof Lattice lat) {
+						if (var.getCodeLocation() instanceof PcodeLocation loc) {
+							Varnode output = loc.op.getOutput();
+							if (output != null &&
+								output.getAddress().getAddressSpace().isRegisterSpace()) {
+								if (unaffected.contains(output)) {
+									continue;
+								}
+								if (killedByCall.contains(output)) {
+									vEnv.function.put(key, lat.top());
+								}
+							}
+						}
+					}
+				}
+//				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/PcodeUnaryExpression.java

@@ -0,0 +1,63 @@
+/* ###
+ * IP: GHIDRA
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ghidra.lisa.pcode.expressions;
+
+import ghidra.lisa.pcode.contexts.UnaryExprContext;
+import ghidra.lisa.pcode.statements.PcodeUnaryOperator;
+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.UnaryExpression;
+import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator;
+
+public class PcodeUnaryExpression extends it.unive.lisa.program.cfg.statement.UnaryExpression {
+
+	private UnaryOperator operator;
+
+	public PcodeUnaryExpression(
+			CFG cfg,
+			UnaryExprContext ctx,
+			Expression expression) {
+		super(cfg, ctx.location(), ctx.mnemonic(), expression);
+		this.operator = new PcodeUnaryOperator(ctx.op);
+	}
+
+	@Override
+	protected int compareSameClassAndParams(
+			Statement o) {
+		return 0; // no extra fields to compare
+	}
+
+	@Override
+	public <A extends AbstractState<A>> AnalysisState<A> fwdUnarySemantics(
+			InterproceduralAnalysis<A> interprocedural,
+			AnalysisState<A> state,
+			SymbolicExpression expr,
+			StatementStore<A> expressions)
+			throws SemanticException {
+
+		return state.smallStepSemantics(
+			new UnaryExpression(
+				expr.getStaticType(),
+				expr,
+				operator,
+				getLocation()),
+			this);
+	}
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/locations/InstLocation.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.locations;
+
+import ghidra.program.model.address.Address;
+import ghidra.program.model.listing.Function;
+import it.unive.lisa.program.cfg.CodeLocation;
+
+public class InstLocation implements CodeLocation {
+
+	private Function function;
+	private Address addr;
+
+	public InstLocation(Function function, Address addr) {
+		this.function = function;
+		this.addr = addr;
+	}
+
+	@Override
+	public int compareTo(CodeLocation o) {
+		if (o instanceof InstLocation i) {
+			return addr.compareTo(i.addr);
+		}
+		return -1;
+	}
+
+	@Override
+	public String getCodeLocation() {
+		return addr.toString();
+	}
+
+	public Function function() {
+		return function;
+	}
+
+	public Address getAddress() {
+		return addr;
+	}
+
+}

Ghidra/Extensions/Lisa/src/main/java/ghidra/lisa/pcode/locations/PcodeLocation.java

@@ -0,0 +1,68 @@
+/* ###
+ * 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.locations;
+
+import ghidra.program.model.address.Address;
+import ghidra.program.model.pcode.PcodeOp;
+import it.unive.lisa.program.cfg.CodeLocation;
+
+public class PcodeLocation implements CodeLocation {
+
+	public PcodeOp op;
+
+	public PcodeLocation(PcodeOp op) {
+		this.op = op;
+	}
+
+	@Override
+	public int compareTo(CodeLocation o) {
+		if (o instanceof PcodeLocation pl) {
+			return op.getSeqnum().compareTo(pl.op.getSeqnum());
+		}
+		return -1;
+	}
+
+	@Override
+	public String getCodeLocation() {
+		return op.getSeqnum().toString();
+	}
+
+	public int getOpcode() {
+		return op.getOpcode();
+	}
+
+	public Address getAddress() {
+		return op.getSeqnum().getTarget();
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (obj instanceof PcodeLocation ploc) {
+			return this.op.getSeqnum().equals(ploc.op.getSeqnum());
+		}
+		return false;
+	}
+
+	@Override
+	public int hashCode() {
+		return op.getSeqnum().hashCode();
+	}
+
+	@Override
+	public String toString() {
+		return getCodeLocation();
+	}
+}