[klee-dev] Using LLVM cost modeling in KLEE

[Nowack, Martin]

Hi Matthew,

Sounds like an interesting project.

I would try first to distinguish if that problem is caused by KLEE or LLVM.
KLEE does some code generation and optimisations of the software under test, that might have an impact.
Does the issue show for all functions or just some? If just for some, which are those functions?
And what is the error message?


For your implementation, as you’re interested in the per-instruction cost, hook into the KModule generation and attach this information as additional meta data in KInstruction (https://github.com/klee/klee/blob/master/include/klee/Module/KInstruction.h)

The instrumentation functionality should give you an idea how to run your required pass and generate the data (`klee::instrument` in https://github.com/klee/klee/blob/492800921e47141d509736f97731f2985c09704d/lib/Module/InstrumentLegacy.cpp#L35)

While developing such an extension, use a debug and assertion enabled version of LLVM that should help with the process.

Best,
Martin



> On 18 Jun 2025, at 20:01, Matthew Schmitt <mschmit1 at stevens.edu> wrote:
> 
> We are currently attempting to explore methods that would add a provision to KLEE so that a cost metric can be produced for each path that KLEE explores within a program. The instruction cost metrics provided by the LLVM optimizers appear to be sufficient for our purposes, as they provide values that are reflective of the latency of each LLVM bytecode instruction on the particular CPU architecture that the program in question is being targeted for. We would like to replicate the functionality provided by passes like the one located at llvm/Analysis/CostModel.h.
> 
> Unfortunately, we have encountered some issues with this when it comes to returning the true latency-aware costs for instructions such as floating-point division (fdiv). It is my understanding that costs such as this are highly architecture specific, though will always be more expensive than multiplication, addition, or subtraction, hence why LLVM must collect information about the current target. In our case, even after this is completed successfully, LLVM encounters some error, and handles it by reverting to a generic cost model that returns costs that are simply unstable for the purposes of this extension, such as returning the same costs for all floating-point operations.
> 
> We are currently attempting to implement this feature as presented below:
> 
> std::unique_ptr<raw_fd_ostream> InstructionStats = interpreterHandler->openOutputFile("stats.csv");
> 
> bindModuleConstants();
> InitializeNativeTarget();
> InitializeNativeTargetAsmPrinter();
> InitializeNativeTargetAsmParser();
> 
> Expected<llvm::orc::JITTargetMachineBuilder> JITBE = llvm::orc::JITTargetMachineBuilder::detectHost();
> 
> if (!JITBE) klee_error("Failed to detect host target machine");
> 
> llvm::orc::JITTargetMachineBuilder JITB = std::move(*JITBE);
> 
> Expected<std::unique_ptr<TargetMachine>> TME = JITB.createTargetMachine();
> 
> if (!TME) klee_error("Failed to create target machine");
> 
> TMown = std::move(*TME);
> TargetMachine *TM = TMown.get();
> 
> if (InstructionStats) {
>   *InstructionStats << "Target Triple: " << TM->getTargetTriple().str() << "\n";
>   *InstructionStats << "CPU: " << TM->getTargetCPU() << "\n";
>   *InstructionStats << "Features: " << TM->getTargetFeatureString() << "\n";
>   *InstructionStats << "Instruction/Call, Cost" << "\n";
> }
> else {
>   klee_error("Error: could not access file");
> }
> 
> /* The target machine seems to be constructed correctly. All values appear to reflect the CPU architecture of the current machine. */
> Instruction *i = ki->inst;
> Function *f = state.stack.back().kf->function;
> TargetIRAnalysis TIRA = (TM ? TM->getTargetIRAnalysis() : TargetIRAnalysis());
> Module *M = f->getParent();
> 
> M->setDataLayout(TM->createDataLayout());
> M->setTargetTriple(TM->getTargetTriple().getTriple());
> 
> TargetTransformInfo TTI = TM->getTargetTransformInfo(*f);
> InstructionCost Cost = TTI.getInstructionCost(i, TargetTransformInfo::TCK_Latency);
> /* This cost value is wrong and appears to reflect costs of the generic TTI implementation, not the x86 implementation */
> 
> We would appreciate any assistance in this regard, particularly concerning advice as to how getInstructionCost can be effectively utilized outside of an LLVM optimizer pass.
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev