views:

732

answers:

23

Whilst working on a recent project, I was visited by a customer QA representitive, who asked me a question that I hadn't really considered before:

How do you know that the compiler you are using generates machine code that matches the c code's functionality exactly and that the compiler is fully deterministic?

To this question I had absolutely no reply as I have always taken the compiler for granted. It takes in code and spews out machine code. How can I go about and test that the compiler isn't actually adding functionality that I haven't asked it for? or even more dangerously implementing code in a slightly different manner to that which I expect?

I am aware that this is perhapse not really an issue for everyone, and indeed the answer might just be... "you're over a barrel and deal with it". However, when working in an embedded environment, you trust your compiler implicitly. How can I prove to myself and QA that I am right in doing so?

+1  A: 

Try unit testing.

If that's not enough, use different compilers and compare the results of your unit tests. Compare strace outputs, run your tests in a VM, keep a log of disk and network I/O, then compare those.

Or propose to write your own compiler and tell them what it's going to cost.

+3  A: 

It all boils down to trust. Does your customer trust any compiler? Use that, or at least compare output code between yours and theirs.

If they don't trust any, is there a reference implementation for the language? Could you convince them to trust it? Then compare yours against the reference or use the reference.

This all assuming you actually verify the actual code you get from the vendor/provider and that you check the compiler has not been tampered with, which should be the first step.

Anyhow this still leaves the question about how would you verify, without having references, a compiler, from scratch. That certainly looks like a ton of work and requires a definition of the language, which not always is available, sometimes the definition is the compiler.

Vinko Vrsalovic
+11  A: 

You can apply that argument at any level: do you trust the third party libraries? do you trust the OS? do you trust the processor?

A good example of why this may be a valid concern of course, is how Ken Thompson put a backdoor into the original 'login' program ... and modified the C compiler so that even if you recompiled login you still got the backdoor. See this posting for more details.

Similar questions have been raised about encryption algorithms -- how do we know there isn't a backdoor in DES for the NSA to snoop through?

At the end of the you have to decide if you trust the infrastructure you are building on enough to not worry about it, otherwise you have to start developing your own silicon chips!

Rob Walker
Exactly. I'm assuming that if the guy asked is because the thing is sensitive and they have reasons to, not because they are paranoid wankers...
Vinko Vrsalovic
No, Ken didn't, and quoting some blogger doesn't make it so. Read Ken's real paper (Reflections on Trusting Trust) to see what he really did: he suggested that he could do it. Neither the alleged compiler nor the alleged login binary has ever been seen.
MSalters
Answer does not actually address the question.
Tim Williscroft
A: 

It all boils down to trust.

I couldn't agree more! The trouble is that all Ive always seen customer technical reps do is to try and 'trip you up' in such that you say that you hadn't thought of something, or overlooked a minor point and use this to impose more stringent requirements. I guess that I was lucky and that I could say that many other companies and projects use the MS c compiler, but there are really obscure langueages being used and integrated into mainstream languages upon which, there is little relevant information. I suppose Im asking ... is there a generally agreed procedure on 'certifying' a compiler?

TK
A: 
  1. Changing the optimization level of the compiler will change the output.
  2. Slight changes to a function may make the compiler inline or no longer inline a function.
  3. Changes to the compiler (gcc versions for example) may change the output
  4. Certain library functions may be instrinic (i.e., emit optimized assembly) while others most are not.

The good news is that for most things it really doesn't matter that much. Where it does, you may want to consider assembly if it really matters (e.g., in an ISR).

dpp
+1  A: 

The most you can easily certify is that you are using an untampered compiler from provider X. If they do not trust provider X, it's their problem (if X is reasonably trustworthy). If they do not trust any compiler provider, then they are totally unreasonable.

Answering their question: I make sure I'm using an untampered compiler from X through these means. X is well reputed, plus I have a nice set of tests that show our application behaves as expected.

Everything else is starting to open the can of worms. You have to stop somewhere, as Rob says.

Vinko Vrsalovic
A: 

If you are concerned about unexpected machine code which doesn't produce visible results, the only way is probably to contact compiler vendor for certification of some sort which will satisfy your customer.

Otherwise you'll know it the same you know about bugs in your code - testing.

Machine code from modern compilers can be vastly different and totally incomprehensible for puny humans.

ima
A: 

Sometimes you do get behavioural changes when you request aggressive levels of optimisation.

And optimisation and floating point numbers? Forget it!

Rob Wells
A: 

I think it's possible to reduce this problem to the Halting Problem somehow.

The most obvious problem is that if you use some kind of program to analyze the compiler and its determinism, how do you know that your program gets compiled correctly, and produces the correct result?

If you're using another, "safe" compiler though, I'm not sure. What I'm sure is writing a compiler from scratch would probably be an easier job.

aib
No, it's quite possible to write a provably correct compiler, and to ground the proving ultimately in the correctness of a small hand-checked proof-checker. What's uncomputable is to take an arbitrary program and tell for sure whether it's the correct compiler you want.
Darius Bacon
+2  A: 

You don't know for sure that the compiler will do exactly what you expect. The reason is, of course, that a compiler is a peice of software, and is therefore susceptible to bugs.

Compiler writers have the advantage of working from a high quality spec, while the rest of us have to figure out what we're making as we go along. However, compiler specs also have bugs, and complex parts with subtle interactions. So, it's not exactly trivial to figure out what the compiler should be doing.

Still, once you decide what you think the language spec means, you can write a good, fast, automated test for every nuance. This is where compiler writing has a huge advantage over writing other kinds of software: in testing. Every bug becomes an automated test case, and the test suite can very thorough. Compiler vendors have a lot more budget to invest in verifying the correctness of the compiler than you do (you already have a day job, right?).

What does this mean for you? It means that you need to be open to the possibilities of bugs in your compiler, but chances are you won't find any yourself.

I would pick a compiler vendor that is not likely to go out of business any time soon, that has a history of high quality in their compilers, and that has demonstrated their ability to service (patch) their products. Compilers seem to get more correct over time, so I'd choose one that's been around a decade or two.

Focus your attention on getting your code right. If it's clear and simple, then when you do hit a compiler bug, you won't have to think really hard to decide where the problem lies. Write good unit tests, which will ensure that your code does what you expect it to do.

Jay Bazuzi
+8  A: 

For safety critical embedded application certifying agencies require to satisfy the "proven-in-use" requirement for the compiler. There are typically certain requirements (kind of like "hours of operation") that need to be met and proven by detailed documentation. However, most people either cannot or don't want to meet these requirements because it can be very difficult especially on your first project with a new target/compiler.

One other approach is basically to NOT trust the compiler's output at all. Any compiler and even language-dependent (Appendix G of the C-90 standard, anyone?) deficiencies need to be covered by a strict set of static analysis, unit- and coverage testing in addition to the later functional testing.

A standard like MISRA-C can help to restrict the input to the compiler to a "safe" subset of the C language. Another approach is to restrict the input to a compiler to a subset of a language and test what the output for the entire subset is. If our application is only built of components from the subset it is assumed to be known what the output of the compiler will be. The usually goes by "qualification of the compiler".

The goal of all of this is to be able to answer the QA representative's question with "We don't just rely on determinism of the compiler but this is the way we prove it...".

cschol
Right on. Use unit tests, static testing and integration testing to verify systems behavior. The customer's QQ guy wanted to know if you know how to test software to assure quality. Validate your unit and integration test data set using either a test oracle or some validated independent means. (E.g. Hand generated unit test results, validated by several engineers.)
Tim Williscroft
+7  A: 

You know by testing. When you test, you're testing your both code and the compiler.

You will find that the odds that you or the compiler writer have made an error are much smaller than the odds that you would make an error if you wrote the program in question in some assembly language.

jfm3
Make sure you use sufficient tests. If the application domain has little requirement for correctness, testing is easy. To do this rigorously, the formal requirements have to be represented by the software, and tested by the unit and integration tests. If the formal correctness requirements are not defined, then any answer is right. The customer will pick whichever one you didn't choose.
Tim Williscroft
+1  A: 

For most software development (think desktop applications) the answer is probably that you don't know and don't care.

In safety-critical systems (think nuclear power plants and commercial avionics) you do care and regulatory agencies will require you to prove it. In my experience, you can do this one of two ways:

  1. Use a qualified compiler, where "qualified" means that it has been verified according to the standards set out by the regulatory agency.
  2. Perform object code analysis. Essentially, you compile a piece of reference code and then manually analyze the output to demonstrate that the compiler has not inserted any instructions that can't be traced back to your source code.
Michael Carman
+4  A: 

There are compiler validation suits available.
The one I remember is "Perennial".

When I worked on a C compiler for a embedded SOC processor we had to validate the compiler against this and two other validation suits (that I forget the name of). Validating the compiler to a certain level of conformance to these test suits was part of the contract.

Martin York
A: 

Even a qualified or certified compiler can produce undesirable results. Keep your code simple and test, test, test. That or walk through the machine code by hand while not allowing any human error. PLus the operating system or whatever environment you are running on (preferably no operating system, just your program).

This problem has been solved in mission critical environments since software and compilers began. As many of the others who have responded also know. Each industry has its own rules from certified compilers to programming style (you must always program this way, never use this or that or the other), lots of testing and peer review. Verifying every execution path, etc.

If you are not in one of those industries, then you get what you get. A commercial program on a COTS operating system on COTS hardware. It will fail, that is a guarantee.

dwelch
+1  A: 

...you trust your compiler implicitly

You'll stop doing that the first time you come across a compiler bug. ;-)

But ultimately this is what testing is for. It doesn't matter to your test regime how the bug got in to your product in the first place, all that matters is that it didn't pass your extensive testing regime.

Andrew Edgecombe
+1  A: 

How do you know that the compiler you are using generates machine code that matches the c code's functionality exactly and that the compiler is fully deterministic?

You don't, that's why you test the resultant binary, and why you make sure to ship the same binary you tested with. And why when you make 'minor' software changes, you regression test to make sure none of the old functionality broke.

The only software I've certified is avionics. FAA certification isn't rigorous enough to prove the software works correctly, while at the same time it does force you to jump through a certain amount of hoops. The trick is to structure your 'process' so it improves quality as much as possible, with as little extraneous hoop-jumping as you can get away with. So anything that you know is worthless and won't actually find bugs, you can probably weasel out of. And anything you know you should do because it will find bugs that isn't explicitly asked for by the FAA, your best bet is to twist words until it sounds like you're giving the FAA/your QA people what they asked for.

This actually isn't as dishonest as I've made it sound, in general the FAA cares more about you being conscientious and confident that you're trying to do a good job, than about what exactly you do.

KeyserSoze
+2  A: 

Some intellectual ammunition might be found in Crosstalk, a magazine for defense software engineers. This question is the kind of thing they spend many waking hours on. http://www.stsc.hill.af.mil/crosstalk/2006/08/index.html (If i can find my old notes from an old project, i'll be back here...)

DarenW
+2  A: 

You can never fully trust the compiler, even highly recommended ones. They could release an update that has a bug, and your code compiles the same. This problem is compounded when updating old code with the buggy compiler, doing testing and shipping out the goods only to have the customer ring you 3 months later with a problem.

It all comes back to testing, and if there is one thing I have learnt it is to thouroughly test after any non-trivial change. If the problem seems impossible to find have a look at the compiled assembler and check it's doing what it should be doing.

On several occasions I have found bugs in the compiler. One time there was a bug where 16 bit variables would get incremented but without carry and only if the 16 bit variable was part of an extern struct defined in a header file.

geometrikal
A: 

You get the one Dijkstra wrote.

Watson Ladd
+1  A: 

Select a formally verified compiler, like Compcert C compiler.

abc
But how do you know the verifier(Coq) is correct? How do you know that the C specification was transcribed into Coq's language correctly?
Mike
A: 

If your worried about malicious bugs in the compiler, one recommendation (IIRC, an NSA requirement for some projects) is that the compiler binary predate the writing of the code. At least then you know that no one has added bugs targeted at your program.

BCS
+1  A: 

Well.. you can't simply say that you trust your compiler's output - particularly if you work with embedded code. It is not hard to find discrepancies between the code generated when compiling the very same code with different compilers. This is the case because the C standard itself is too loose. Many details can be implemented differently by different compilers without breaking the standard. How do we deal with this stuff? We avoid compiler dependent constructs whenever possible. We may deal with it by choosing a safer subset of C like Misra-C as previously mentioned by the user cschol. I seldom have to inspect the code generated by the compiler but that has also happened to me at times. But, ultimately, you are relying on your tests in order to make sure that the code behaves as intended.

Is there a better option out there? Some people claim that there is. The other option is to write your code in SPARK/Ada. I have never written code in SPARK but my understanding is that you would still have to link it against routines written in C that would deal with the "bare metal" stuff. The beauty of SPARK/Ada is that you are absolutely guaranteed that the code generated by any compiler is always going to be the same. No ambiguity whatsoever. On top of that, the language allows you to annotate the code with explanations as to how the code is intended to behave. The SPARK toolset will use these annotations to formally prove that the code written does indeed do what the annotations have described. So I have been told that for critical systems, SPARK/Ada is a pretty good bet. I have never tried it myself though.

figurassa