[klee-dev] Using LLVM cost modeling in KLEE
Matthew Schmitt
mschmit1 at stevens.edu
Tue Jun 24 19:21:17 BST 2025
Perhaps error was not the best use of language, as we are not receiving a specific error message from KLEE or LLVM, rather LLVM is not assigning the correct TTIImpl to our TargetMachine, from what I understand. This seems to occur because some exception or check fails during the construction of the TargetTransformInfo object, which causes a fallback to the generic TTI implementation, which causes an incorrect cost to be supplied for any instruction that is an arithmetic operator or load/store operation.
As per the recommendation, we have implemented a pass that is based upon the CostModel (https://github.com/llvm-mirror/llvm/blob/master/lib/Analysis/CostModel.cpp) analysis pass that is accessible in the LLVM opt utility. This adaptation adds a metadata node to each LLVM instruction so that we can then read a cost value in the ExecuteInstruction function in Executor.cpp. This pass is added to the pass manager instance in klee::instrument as suggested.
We face the same issues with this approach, as we did when extracting the TTI from the TargetMachine and using TTI.getInstructionCost in the ExecuteInstruction function, where the generic TTI is constructed and incorrect costs are generated.
We have used a debugger to verify that the target triple, CPU string, and CPU feature list are reflective of the current host, so there does not appear to be a reason why TTI would fall back to the generic implementation.
Further assistance would be appreciated, and please let us know if this question is worth posting to the LLVM mailing list as well.
________________________________
From: Nowack, Martin <m.nowack at imperial.ac.uk>
Sent: Thursday, June 19, 2025 4:57:53 AM
To: Matthew Schmitt <mschmit1 at stevens.edu>
Cc: Nowack, Martin <m.nowack at imperial.ac.uk>; klee-dev <klee-dev at imperial.ac.uk>
Subject: Re: [klee-dev] Using LLVM cost modeling in KLEE
CAUTION: This email originated from outside of Stevens. Please do not click links or open attachments unless you recognize the sender and know the content is safe.
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://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fklee%2Fklee%2Fblob%2Fmaster%2Finclude%2Fklee%2FModule%2FKInstruction.h&data=05%7C02%7Cmschmit1%40stevens.edu%7Ca944d8c5541a44dff6f608ddaf0f5cc1%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C638859202734908404%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=wtvQwjQ1cinCjHsqaOaIri3LppzXUaNpPB0o6PBS3cE%3D&reserved=0<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://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fklee%2Fklee%2Fblob%2F492800921e47141d509736f97731f2985c09704d%2Flib%2FModule%2FInstrumentLegacy.cpp%23L35&data=05%7C02%7Cmschmit1%40stevens.edu%7Ca944d8c5541a44dff6f608ddaf0f5cc1%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C638859202734929330%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=RXemJIb2urtRgxa8c3qvOmN%2BPLIzyULwkiAsz19IEX8%3D&reserved=0)<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://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmailman.ic.ac.uk%2Fmailman%2Flistinfo%2Fklee-dev&data=05%7C02%7Cmschmit1%40stevens.edu%7Ca944d8c5541a44dff6f608ddaf0f5cc1%7C8d1a69ec03b54345ae21dad112f5fb4f%7C0%7C0%7C638859202734943079%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=5iIGX1w2cmneLKoItC7bPzl2kbESY1KTeL5JaUEFMXk%3D&reserved=0<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list