Hacker News new | ask | show | jobs
by philzook 868 days ago
ooooooh. link?

What do you mean by standardizing on hardware and toolchain? I am currently choosing ghidra and cbmc, and it seems like the approach is applicable to any compiler or arch that ghidra supports without too much change. I have only been doing x86-64 and gcc so far though
2 comments
nanolith 868 days ago
Sadly, I don't have a link for this yet. My goal is to write this up once I have a compelling example.

In the meantime, check out my github. https://github.com/nanolith

Currently, I'm feeding commits into libcparse, which is the start of this effort. That stream is currently about 180 days out of phase with what's in my local repositories, but it is slowly trickling in. The first step of this second phase will be to use libcparse to verify itself via constructive proofs in Lean. Currently, and by that I mean what hits in March or April, libcparse has a mostly C18 compliant lexical scanner for the C preprocessor. The goal is to have a SAX-like C18 parser that can detect all C declarations and definitions. Tooling will include a utility that imports C declarations and definitions into both Lean 4 and Coq. This is a moonlighting effort for an upcoming book I intend to write.

link
nanolith 868 days ago
As for standardizing on hardware and toolchain, what I mean is that I try to get projects to commit to using specific hardware and a specific toolchain. The goal is to limit variables for automated testing and analysis.

OpenBSD, in particular, is adamant about testing their OS on real hardware for platforms that they support. Their definition of "working" is on real hardware. I think that's a reasonable goal.

It helps with analysis like this, as you don't have to worry about different compilers or different hardware. GCC, in particular, can produce different output depending on which hardware it was compiled on, unless a specific configuration is locked down. If there is a flaw in how it does vector operations on a particular Xeon processor, this won't be caught if testing locally on a Core i5 processor that produces different code.

link