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 <[email protected]>
Sent: Thursday, June 19, 2025 4:57:53 AM
To: Matthew Schmitt <[email protected]>
Cc: Nowack, Martin <[email protected]>; klee-dev <[email protected]>
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 <[email protected]> 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
> [email protected]
> 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>


_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to