Reimplement CBMC in POSIX shell

[karkhaz]

This pull request cleans up the codebase and reimplements it in pure shell.

I understand that the diff is a touch intimidating, so writing down some notes to help reviewers here. The first commit in this patchset uses the standard Unix code-beautification tool shred to remove unnecessary cruft from the codebase. I invoked it like this:

#!/bin/sh

CBMC_DIR=cbmc
LOTS=999 # Extra thorough refactoring

shred                   \
  --force               \
  --iterations=${LOTS}  \
  --remove=wipesync     \
  --zero                \
  ${home}/${cbmc_dir}

After suffering from an unrelated hardware fault, I decided to write down the new implementation of CBMC on a napkin. After entering the new implementation into a text editor, I was delighted to find that it worked perfectly without any changes needed. Here is a series of runs:

> cbmc foo.c
VERIFICATION SUCCESSFUL
> cbmc bar.c
VERIFICATION SUCCESSFUL
> cbmc bar.c
VERIFICATION FAILED

This pull request fixes #1924.

[karkhaz]

Note to reviewers please feel free to disassemble the cbmc script to see how it works, but for the love of everything good, do not run shred the way I wrote above, especially without checking your variables.

[martin-cs]

We should get this merged ASAP.

@tautschnig : the CI is giving weird results; can you have a look at them. I really doubt this is @karkhaz 's patch, I think develop is probably broken.

@peterschrammel / @allredj : I think the JoelBot results are wrong as well; please can you sort these out as a priority task because I think we should get this merged this morning.

@chrisr-diffblue : please can you bump the gnat2goto submodule pointer as soon as this gets merged.

Great work @karkhaz !

[tautschnig]

To support what @martin-cs said: this absolutely needs to be merged today. Approving!

[peterschrammel]

LGTM, but needs a rebase...

[peterschrammel]

I'm impressed by the performance of the new implementation. @cesaro and @forejtv should really try that!

[allredj]

Typo in commit message

[allredj]

Glad to see that test.pl has finally been fixed. I have a few nitpicks though.

[allredj]

#!/bin/bash?

[chrisr-diffblue]

Surely /bin/tcsh?

[chrisr-diffblue]

This is great! But I wonder whether this would allow us much better integration with windows if you were to reimplement as a DOS command shell script as well?

[hannes-steffenhagen-diffblue]

LGTM, but I'm a bit concerned about the formatting.

[hannes-steffenhagen-diffblue]

This could use some line breaks for increased readability.

[karkhaz]

Thank you all for the thoughtful reviews. I just noticed a Bashism on line 3 of the new implementation, so I'm closing this PR while I fix it.

[NathanJPhillips]

/dev/urandom is based on secure hashes rather than using ciphers under Linux (to avoid cryptography export restrictions that were in place when the generator was originally designed). This may cause it not to accurately represent the run-time behaviour of the input program. Consider using ciphers in your fixed version.