|
|
|---|
|
|
|
|---|
A simple transformation to simplify
This is a very simple proof-of-concept transformation,
which replaces expressions of the form
(simpadd0 const-old const-new :proofs ... ; default nil )
Specifies the code to the transformed.
This must be a symbol that names an existing ACL2 constant that contains a validated translation unit ensemble, i.e. a value of type transunit-ensemble resulting from validation, and in particular containing validation information. This constant could result from c$::input-files, or from some other transformation.
In the rest of this documentation page, we refer to this constant as
*old* .
Specifies the name of the constant for the transformed code.
This must be a symbol that is valid name for a new ACL2 constant.
In the rest of this documentation page,
we refer to this constant as
Specifies whether proofs of correctness should be generated or not.
This is a very preliminary proof-of-concept capability. It works only on very restricted forms of the code. This is why, for now, it is turned off by default.
The named constant containing the result of the transformation. This is a translation unit ensemble that is the same as the one in
*old* , except that:
- Every occurrence of an expression of the form
<x> + 0 , where<x> is a variable and0 is the octal constant for zero without other leading zeros and without suffixes, into just the expression<x> .- Each file path
<file>.<ext> in*old* is turned into<file>.simpadd0.<ext> , if the path has a dot, and where<ext> had no dots; if the path is<file> without dots, it is turned into<file>.simpadd .
Equivalence theorems.
These are generated only if
:proofs ist .One theorem is generated for every function definition in
*old* .If
<f> is the name of a defined function in*old* , the generated theorem has the form(defruled |<f>|-equivalence (equal (c::exec-fun (c::ident "<f>") nil compst (c::init-fun-env (mv-nth 1 (c$::ldm-transunit (omap::lookup <path> (transunit-ensemble->unwrap *old*))))) 1000) (c::exec-fun (c::ident ,string) nil compst (c::init-fun-env (mv-nth 1 (c$::ldm-transunit (omap::lookup <path> (transunit-ensemble->unwrap *new*))))) 1000)))where:
- c::exec-fun is part of our dynamic semantics for C.
- The
nil passed as second argument to c::exec-fun signifies that we only generate proofs for C functions that take no arguments. (As noted above, this proof generation capability is very preliminary.<path> is the path of the translation unit that defines<f> .- c$::ldm-transunit is part of the mapping from our abstract syntax for tools to the the abstract syntax of our C formalization. This is a partial mapping, because our C formalization only covers a subset of C. If any of the translation units in
*old* falls outside the domain of the mapping, thesimpadd0 transformation fails, because proofs cannot be generated; in this case, the transformation must be run with:proofs nil .- The
1000 passed to c::exec-fun is just an arbitrary limit, for this very preliminary proof generation capability.Any of these generated theorems may actually fail to prove. Currently
simpadd0 does not generate robust proofs, and does not make thorough checks to provide user-friendly error messages if proof generation is not possible.