Japheth's recent change (6f7c660cb) to error-reporting for the latter
broke the former. Refactor code so that old and new code can coexist.
Would just use Japheth's code in the purely SML version too, but it uses
Isabelle/ML libraries that I can't be bothered to recreate in SML.
The handling of local static variables is now part of a general
improvement in the handling of all the "munging" that the parser does.
*Munging* is the process of renaming variables so that Isabelle can cope
with them. There are at least three different forms of munging at the
moment:
- static locals get munged so that multiple static locals (which have to
be treated as globals) can co-exist with the same source name.
- local variables of the same source name but different types have to be
able to co-exist
- variables with legitimate C names but illegal Isabelle names have to
be allowed
The new structure MString implements an opaque version of string
designed to make it clear to the typechecker that certain strings are
"munged".
They are now treated as globals with a specially munged name, derived
from the given name and the name of the function where they occur. The
function NameGeneration.mk_localstatic generates the "munged" name.
As with other globals, initialisation is not handled very well (i.e., at
the moment the initialisation is completely ignored).
Close JIRA VER-439
This extra proof was to validate that the existing word 32 proof generalises to
other, arbitrarily complex, types. The proof script is more or less identical,
which strongly suggests that we can now trivially lift the generic memcpy proof
into a proof for copying any mem_type. It would be nice to generalise the
required properties on is_valid_* into some kind of locale construction, but the
way lifted_globals and friends are constructed make this a little tricky.
Note that the memcpy implementation we're currently reasoning about should
actually work correctly even if the memory regions overlap, as long as the
destination pointer is less than or equal to the source. That is, the
precondition of the Hoare triple for memcpy could be weakened. However, this
does not seem sensible to do as the memcpy spec requires that the input
pointers do not overlap and we don't want users proving properties that they
think will also hold on other memcpy implementations.
In particular, don't reveal the internal references used during
yacc-ing to the user-level. Instead, add a referentially transparent
repair of the AST after its been parsed.
JIRA VER-432
This commit adds a proof over a call to (the non-heap-abstracted) memcpy from
a heap-abstracted context. As a result, our pre- and post-conditions are
expressed on the abstract heap and need to be transfered to the concrete heap
during the proof. Altogether the proof is not so complex and most of the heavy
lifting remains in the original proof of memcpy.
As per example, syntax is
declare [[cpp_path="path to file"]]
If the empty string is used as the value, then no preprocessor will be
called.
The standalone parser has also been adjusted so that you can it with
--cpp=path
or
--nocpp
options.
Closes JIRA issue VER-337
Reasoning about heap equivalence involving mixed types (~= writing to memory
through two differently typed pointers) is very awkward. The enclosed proof
leans heavily on the fact that we know the concrete size of the type of the
memory we're copying, and it still requires a fair bit of sledgehammering. This
is fine for an example, but certainly won't translate to proof generation on
arbitrary types. We may need to take a slightly different tack.
Functions that are declared in the C file, called by other C functions,
but are never actually _defined_ are translated simply into a "fail"
monadic statement. This sometimes causes confusion to new users.
We update AutoCorres to instead emit a new constant:
FUNCTION_BODY_NOT_IN_INPUT_C_FILE
defined simply as "fail" for such functions.
