martin-cs
commented
1 year ago I have talked to some of the people involved in these kinds of projects before (there is also an Intel internal project doing something like this) and yes, it could work and yes it could give us models for lots of intrinsics. There are some performance questions about level of detail (CBMC probably doesn't need to reason about TLB state or cache misses) and some missing information (if an intrinsic alters a particular register, how do we know which variable to alter) but these are probably resolvable.
The big challenge was who was going to do it or, who was going to pay for someone to do it. Sadly, this is the barrier for 99% of "It would be great for CBMC to ...".
If you are volunteering to do it then this is a whole different question! I think the simplest route to get something working would be to take the structured form of the instructions and generate C or C with CBMC's extensions. If you generated a function per instruction, matched the names with the compiler intrinsics and dropped them in ansi-c/library I suspect you could get a proof of concept together in a very short amount of time.
kroening
rod-chapman
I came across a post the other day discussing a project that extracts working SAT models for x86 intrinsics from the pseudocode contained in the Intel documentation. They also linked the SAIL project that also has models for ARM and RISC-V (it also has x86 but I believe those are hand-written).
It would be great for CBMC to support as many of these intrinsics as possible, possibly through the linked projects. Awhile back, I was working on an optimized internet checksum implementation that would be really nice to have a proof for.