Atc-symbolic-execution-rules
Symbolic execution rules for ATC.
Currently, the generated proofs of function correctness
are carried out via symbolic execution of the C code.
The C code is a constant value,
because we are generating proofs over specific C functions;
this makes symbolic execution possible.
In order to make these generated proofs more robust,
we carry them out in a theory that consists exactly of
(what we believe to be) all and only the needed rules.
This file defines that theory.
This set of rules has been defined by
not only thinking of what is needed for symbolic execution,
but also experimenting with several symbolic execution proofs,
starting with the empty theory and adding rules
as needed to advance the symbolic execution,
and also by looking at the C dynamic semantics.
There is no guarantee (meta proof) that
these rules will suffice for every use of ATC;
there is also no guarantee that
the proof will not be defeated by some ACL2 heuristic in some cases.
Nonetheless, the proof strategy seems sound and robust,
and if a generated proof fails
it should be possible to (prove and) use additional rules.
Some of the rules that are used in the symbolic execution
rewrite calls of functions used in the deeply embedded dynamic semantics
into their shallowly embedded counterparts,
under hypothesis on the types of the arguments.
For instance, (exec-unary op x compst)
is rewritten to (<op>-<type> x)
when op is the unary operation corresponding to <op>
(unary plus, unary minus, bitwise complement, or logical complement),
and x has type <type>.
These shallowly embedded counterparts are used
in the ACL2 functions from which C code is represented:
thus, the rewrite rules serve to turn (the execution of) the C code
into the ACL2 terms from which the C code is generated,
which is at the core of proving the correctness of the generated C code.
For recursive ACL2 functions that model C execution
(e.g. exec-expr-pure),
we introduce opener rules,
which include syntaxp hypotheses requiring that
the C abstract syntax being executed is a quoted constant.
Some of these opener rules include binding hypotheses,
which avoid symbolically executing the same pieces of C abstract syntax
multiple times in some situations.
We collect the rules in lists,
each of which serves a particular symbolic execution purpose.
Certain rules may appear in multiple lists,
when they serve multiple symbolic execution purposes.
The current organization and subdivision of the rules in these lists
is reasonable, but can (and will) certainly be improved
Subtopics
- Atc-exec-expr-pure-rules
- Rules for exec-expr-pure.
- Atc-exec-expr-asg-arrsub-rules-generation
- Code to generate the rules for executing
assignments to array subscripting expressions.
- Integer-value-disjoint-rules
- Rules about disjointness of integer values.
- Atc-uaconvert-values-rules
- Rules about uaconvert-values
on values of given types.
- Atc-exec-unary-nonpointer-rules
- Rules for executing unary operations
that do not involve pointers.
- Atc-exec-expr-asg-indir-rules
- Rules for executing assignment expressions
to integers by pointer.
- Atc-exec-expr-asg-arrsub-rules
- Rules for executing assignment expressions to
array subscript expressions.
- Atc-exec-cast-rules-generation
- Code to generate the rules for executing cast operations.
- Atc-exec-cast-rules
- Rules for executing casts.
- Atc-exec-binary-strict-pure-rules-generation
- Code to generate the rules for executing
strict pure binary operations.
- Atc-exec-arrsub-rules
- Rules for executing array subscript expressions.
- Atc-convert-integer-value-rules
- Rules about convert-integer-value.
- Atc-array-read-rules
- Rules about array reads.
- Array-value-disjoint-rules
- Rules about disjointness of array values.
- Atc-exec-arrsub-rules-generation
- Code to generate the rules for executing array subscript expressions.
- Atc-exec-unary-nonpointer-rules-generation
- Code to generate the rules for executing
unary operations that do not involve pointers.
- Atc-identifier-rules
- Rules related to C identifiers.
- Atc-flexible-array-member-rules
- Rules about flexible array members.
- Atc-exec-indir-rules
- Rules for executing the indirection unary operation.
- Atc-uaconvert-values-rules-generation
- Code to generate the rules for uaconvert-values.
- Atc-exec-expr-asg-indir-rule-generation
- Code to generate the rules for executing
assignments to integers by pointer.
- Atc-exec-stmt-rules
- Rules for exec-stmt.
- Value-bridge-theorems
- Bridge theorems between
the deeply embedded integer values
and the shallowly embedded integer values.
- Atc-test-value-rules
- Rules for executing tests on values.
- Atc-exec-const-rules
- Rules for executing constants.
- *atc-integer-ops-2-return-rewrite-rules*
- List of rewrite rules for the return types of
models of C integer operations that involve two C integer types.
- *atc-integer-ops-2-type-prescription-rules*
- List of type prescription rules for the
models of C integer operations that involve two C integer types.
- Atc-integer-conv-rules
- Rules about the composition of integer conversions.
- Atc-adjust-type-rules
- Rules for adjust-type.
- Atc-static-variable-pointer-rules
- Rules about pointers to variables in static storage.
- Atc-exec-indir-rules-generation
- Code to generate the rules for executing
the indirection unary operation.
- Atc-exec-binary-strict-pure-rules
- Rules for executing strict pure binary operations.
- Atc-array-write-rules
- Rules about array writes.
- Array-value-rules
- Some rules about array values.
- Atc-pointed-integer-rules
- Rules about pointed-to integers.
- Atc-array-length-rules
- Rules for array length operations.
- *atc-exec-cast-rules*
- Atc-value-array->elemtype-rules
- Rules about value-array->elemtype.
- *atc-exec-expr-asg-arrsub-rules-deprecated*
- Atc-limit-rules
- Rules about limits not being 0.
- Atc-exec-fun-rules
- Rules for exec-fun.
- Type-of-value-under-array-predicates
- Rules that rewrite type-of-value to specific types
under hypotheses on different array types of values.
- Atc-value-integer->get-rules
- Rules about value-integer->get
assuming the various integer types.
- Atc-distributivity-over-if-rewrite-rules
- Rewrite rules about certain functions distributing over if.
- *atc-array-write-return-rewrite-rules*
- List of rewrite rules for the return types of
models of C array write operations.
- *atc-array-read-return-rewrite-rules*
- List of rewrite rules for the return types of
models of C array read operations.
- *atc-integer-convs-type-prescription-rules*
- List of type prescription rules for the
models of C integer conversions.
- *atc-exec-arrsub-rules-deprecated*
- *atc-array-write-type-prescription-rules*
- List of type prescription rules for the
models of C array write operations.
- *atc-array-read-type-prescription-rules*
- List of type prescription rules for the
models of C array read operations.
- Atc-value-array->elements-rules
- Rules about value-array->elements.
- Atc-syntaxp-hyp-for-expr-pure
- Construct a syntaxp hypothesis for
a symbolic execution rule for pure expressions.
- *atc-uaconvert-values-rules*
- *atc-integer-ops-1-return-rewrite-rules*
- List of rewrite rules for the return types of
models of C integer operations that involve one C integer type.
- *atc-integer-convs-return-rewrite-rules*
- List of rewrite rules for the return types of
models of C integer conversions.
- Valuepred-when-value-kind
- Theorems saying that specific value-kinds
imply corresponding value predicates.
- Valuepred-to-type-of-value-equalities
- Rules that rewrite predicates for values
to equalities of the types of the values.
- Atc-promote-value-rules
- Rules about promote-value on values of given types.
- Atc-array-length-write-rules
- Rules for array lengths and array write operations.
- *atc-integer-ops-1-type-prescription-rules*
- List of type prescription rules for the
models of C integer operations that involve one C integer type.
- *atc-all-rules*
- List of all the (generic) rules for the proofs generated by ATC.
- Atc-integer-ifix-rules
- Rules to simplify ifix applied to accessors of C integers.
- *atc-type-prescription-rules*
- List of type prescription rules for the proofs generated by ATC.
- Atc-hide-rules
- Rules about hide.
- Type-of-value-when-valuepred
- Rules that rewrite type-of-value to specific types
under hypotheses on different types of values.
- Atc-value-integerp-rules
- Rules about value-integerp holding
when the predicates for the integer types hold.
- Atc-not-error-rules
- Rules about things of certain types not being errors.
- Value-listp-when-valuepred-listp
- Theorems saying that
the value list recognizers imply value-listp.
- Value-kind-when-valuepred
- Theorem providing the kind of value for different types.
- Atc-value-arithmeticp-rules
- Rules about value-arithmeticp holding
when the predicates for the integer types hold.
- Atc-type-kind-rules
- Rules for resolving type-kind on given types.
- *atc-compound-recognizer-rules*
- List of compound recognizer rules for the proofs generated by ATC.
- Atc-value-pointer-rules
- Rules about value-pointer not satisfying
the predicates for the integer types.
- Atc-boolean-equality-rules
- Rules about boolean equalities.
- Atc-tyname-to-type-rules
- Rules for turning type names into types.
- Atc-integer-size-rules
- Rules related to integer sizes.
- *atc-all-rules-deprecated*
- Variant of *atc-all-rules*
that has rules about deprecated array operations
instead of rules about new array operations.
- Atc-init-scope-rules
- Rules for init-scope.
- Atc-boolean-from-sint
- Rules about boolean-from-sint.
- Valuep-when-valuepred
- Theorem saying that the value recognizers imply valuep.
- Atc-if*-rules
- Rules about if*.
- Atc-exec-ident-rules
- Rules for executing identifiers.
- Atc-integer-const-rules
- Definition rules of the <type>-<base>-const.
- Atc-sint-get-rules
- Rules about the composition of integer-from-sint
with sint-from-<type> functions.
- Atc-type-of-value-option-rules
- Rules about type-of-value-option.
- Atc-identifier-other-rules
- Other rules related to C identifiers.
- Atc-exec-block-item-rules
- Rules for exec-block-item.
- Atc-boolean-from-integer-return-rules
- Rules about the return types of boolean-from-<type>.
- *atc-exec-unary-nonpointer-rules*
- Atc-lognot-sint-rules
- Rules about lognot applied to the signed integer 0 or 1.
- Atc-sint-from-boolean-rules
- Rules about sint-from-boolean.
- *atc-convert-integer-value-rules*
- Atc-value-optionp-rules
- Rules for discharging value-optionp hypotheses.
- Atc-exec-expr-call-or-pure-rules
- Rules for exec-expr-call-or-pure.
- Atc-exec-expr-call-or-asg-rules
- Rules for exec-expr-call-or-asg.
- Atc-exec-block-item-list-rules
- Rules for exec-block-item-list.
- Value-tau-rules
- Some tau rules about values.
- Atc-valuep-rules
- Rules for discharging valuep hypotheses.
- Atc-exec-expr-pure-list-rules
- Rules for exec-expr-pure-list.
- Atc-exec-expr-asg-ident-rules
- Rules for executing assignment expressions to identifier expressions.
- Atc-boolean-fron/to-sint-rules
- Rules about the interaction of
boolean-from-sint and sint-from-boolean.
- *atc-other-executable-counterpart-rules*
- List of other executable counterpart rules
for the proofs generated by ATC.
- Value-promoted-arithmeticp-alt-def
- Alternative definition of value-promoted-arithmeticp,
in terms of the shallow embedding's integer value recognizers.
- Atc-type-of-value-rules
- Rules about type-of-value.
- *atc-type-of-value-rules*
- *atc-identifier-rules*
- List of rules related to C identifiers.
- *atc-flexible-array-member-rules*
- *atc-exec-expr-pure-rules*
- *atc-boolean-from-integer-return-rules*
- *atc-array-read-rules*
- Valuep-possibilities
- Possible integer and other predicates for values.
- Value-unsigned-integerp-alt-def
- Alternative definition of value-unsigned-integerp,
in terms of the shallow embedding's integer value recognizers.
- Value-signed-integerp-alt-def
- Alternative definition of value-signed-integerp,
in terms of the shallow embedding's integer value recognizers.
- Atc-value-listp-rules
- Rules for discharging value-listp hypotheses.
- *atc-pointed-integers-type-prescription-rules*
- List of type prescription rules for the
readers and writers of integers by pointer.
- *atc-pointed-integer-rules*
- *atc-exec-expr-asg-indir-rules*
- Atc-exec-initer-rules
- Rules for exec-initer.
- Array-tau-rules
- Some tau rules about arrays.
- *atc-not-error-rules*
- *atc-integer-conv-rules*
- *atc-array-length-rules*
- *atc-adjust-type-rules*
- Atc-sint-from-boolean
- Rules about sint-from-boolean.
- Atc-init-value-to-value-rules
- Rules for init-value-to-value.
- Atc-exec-expr-call-rules
- Rules for exec-expr-call.
- *atc-value-integer->get-rules*
- *atc-static-variable-pointer-rules*
- *atc-integer-size-rules*
- List of rules related to integer sizes.
- *atc-integer-constructors-return-rules*
- *atc-exec-stmt-rules*
- *atc-exec-expr-asg-arrsub-rules*
- *atc-exec-const-rules*
- *atc-distributivity-over-if-rewrite-rules*
- List of rewrite rules about
certain functions distributing over if.
- *atc-array-length-write-rules*
- Atc-wrapper-rules
- Rules about wrappers.
- Atc-value-result-fix-rules
- Rules for simplifying away value-result-fix.
- Atc-value-kind-rules
- Rules to resolve value-kind for various kinds of values.
- *atc-value-kind-rules*
- *atc-value-array->elemtype-rules*
- *atc-type-kind-rules*
- *atc-test-value-rules*
- *atc-promote-value-rules*
- *atc-integer-ifix-rules*
- *atc-integer-fix-rules*
- *atc-integer-const-rules*
- *atc-exec-indir-rules*
- *atc-exec-arrsub-rules*
- *atc-computation-state-return-rules*
- Atc-misc-rewrite-rules
- Some miscellaneous rewrite rules.
- *atc-valuep-rules*
- *atc-tyname-to-type-rules*
- *atc-init-scope-rules*
- *atc-exec-expr-call-or-pure-rules*
- *atc-exec-expr-call-or-asg-rules*
- *atc-exec-expr-asg-rules-deprecated*
- *atc-exec-expr-asg-ident-rules*
- *atc-exec-block-item-rules*
- Atc-computation-state-return-rules
- Rules about return types of
functions related to the computation state.
- *atc-wrapper-rules*
- *atc-value-result-fix-rules*
- *atc-value-optionp-rules*
- *atc-value-listp-rules*
- *atc-value-fix-rules*
- *atc-type-of-value-option-rules*
- *atc-sint-get-rules*
- *atc-sint-from-boolean*
- *atc-misc-rewrite-rules*
- *atc-lognot-sint-rules*
- *atc-limit-rules*
- *atc-init-value-to-value-rules*
- *atc-exec-initer-rules*
- *atc-exec-ident-rules*
- *atc-exec-fun-rules*
- *atc-exec-expr-pure-list-rules*
- *atc-exec-expr-call-rules*
- *atc-exec-expr-asg-rules*
- *atc-exec-block-item-list-rules*
- *atc-boolean-from-sint*
- Atc-value-fix-rules
- Rules for simplifying away value-fix.
- Atc-integer-fix-rules
- Rules to simplify <type>-fix applies to C integers.
- Atc-integer-constructors-return-rules
- Rules about the return types of the integer constructors.
- Atc-exec-expr-asg-rules
- Rules for executing assignment expressions.
