Mutually recursive ACL2 functions to generate pure C expressions from ACL2 terms.
These are for pure expression terms and for expression terms returning booleans (which are always pure).
We also generate correctness theorems for the generated expressions. The theorems relate (the semantics of) the expressions to the ACL2 terms from which they are generated. Fow now we only generate theorems for some expressions, but eventually we plan to extend this to all the expressions.
As we generate the code, we ensure that the ACL2 terms
are well-typed according to the C types.
This is subsumed by guard verification for all the code,
except for any code that is dead (i.e. unreachable) under the guard:
the dead code passes guard verification
(under a hypothesis of
Function:
(defun atc-gen-expr-pure (term gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp term) (expr-ginp gin)))) (let ((__function__ 'atc-gen-expr-pure)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) ((expr-gin gin) gin) ((when (pseudo-term-case term :var)) (retok (atc-gen-expr-var (pseudo-term-var->name term) gin state))) ((erp okp type-base-const type const) (atc-check-iconst term)) ((when okp) (retok (atc-gen-expr-const term const type type-base-const gin state))) ((erp okp fn arg-term in-type out-type op) (atc-check-unop term)) ((when okp) (b* (((erp (expr-gout arg)) (atc-gen-expr-pure arg-term gin state)) (gin (change-expr-gin gin :thm-index arg.thm-index :names-to-avoid arg.names-to-avoid))) (atc-gen-expr-unary fn arg.term arg.expr arg.type arg.events arg.thm-name in-type out-type op gin state))) ((erp okp fn arg1-term arg2-term in-type1 in-type2 out-type op) (atc-check-binop term)) ((when okp) (b* (((erp (expr-gout arg1)) (atc-gen-expr-pure arg1-term gin state)) (gin (change-expr-gin gin :thm-index arg1.thm-index :names-to-avoid arg1.names-to-avoid)) ((erp (expr-gout arg2)) (atc-gen-expr-pure arg2-term gin state)) (gin (change-expr-gin gin :thm-index arg2.thm-index :names-to-avoid arg2.names-to-avoid))) (atc-gen-expr-binary fn arg1.term arg2.term arg1.expr arg2.expr arg1.type arg2.type arg1.events arg2.events arg1.thm-name arg2.thm-name in-type1 in-type2 out-type op gin state))) ((erp okp fn arg-term in-type out-type tyname) (atc-check-conv term)) ((when okp) (b* (((erp (expr-gout arg)) (atc-gen-expr-pure arg-term gin state)) (gin (change-expr-gin gin :thm-index arg.thm-index :names-to-avoid arg.names-to-avoid))) (atc-gen-expr-conv fn arg.term arg.expr arg.type arg.events arg.thm-name in-type out-type tyname gin state))) ((erp okp fn arg-term type) (atc-check-integer-read term)) ((when okp) (b* (((erp (expr-gout arg)) (atc-gen-expr-pure arg-term gin state)) (gin (change-expr-gin gin :thm-index arg.thm-index :names-to-avoid arg.names-to-avoid))) (atc-gen-expr-integer-read fn arg.term arg.expr arg.type arg.events arg.thm-name type gin state))) ((erp okp fn arr-term sub-term elem-type) (atc-check-array-read term)) ((when okp) (b* (((erp (expr-gout arr)) (atc-gen-expr-pure arr-term gin state)) ((erp (expr-gout sub)) (atc-gen-expr-pure sub-term (change-expr-gin gin :thm-index arr.thm-index :names-to-avoid arr.names-to-avoid) state)) (gin (change-expr-gin gin :thm-index sub.thm-index :names-to-avoid sub.names-to-avoid))) (atc-gen-expr-array-read fn arr.term arr.expr arr.type arr.events arr.thm-name sub.term sub.expr sub.type sub.events sub.thm-name elem-type gin state))) ((erp okp fn arg-term tag member mem-type) (atc-check-struct-read-scalar term gin.prec-tags)) ((when okp) (b* (((erp (expr-gout arg)) (atc-gen-expr-pure arg-term gin state)) (gin (change-expr-gin gin :thm-index arg.thm-index :names-to-avoid arg.names-to-avoid))) (atc-gen-expr-struct-read-scalar fn arg-term arg.expr arg.type arg.events arg.thm-name tag member mem-type gin state))) ((erp okp fn index-term struct-term tag member elem-type flexiblep) (atc-check-struct-read-array term gin.prec-tags)) ((when okp) (b* (((erp (expr-gout index)) (atc-gen-expr-pure index-term gin state)) ((erp (expr-gout struct)) (atc-gen-expr-pure struct-term (change-expr-gin gin :thm-index index.thm-index :names-to-avoid index.names-to-avoid) state)) (gin (change-expr-gin gin :thm-index struct.thm-index :names-to-avoid struct.names-to-avoid))) (atc-gen-expr-struct-read-array fn index.term index.expr index.type index.events index.thm-name struct.term struct.expr struct.type struct.events struct.thm-name tag member elem-type flexiblep gin state))) ((erp okp arg-term) (atc-check-sint-from-boolean term)) ((when okp) (b* (((erp (expr-gout arg)) (atc-gen-expr-bool arg-term gin state))) (atc-gen-expr-sint-from-bool arg.term arg.expr arg.events arg.thm-name (change-expr-gin gin :thm-index arg.thm-index :names-to-avoid arg.names-to-avoid) state))) ((erp okp test-term then-term else-term) (atc-check-condexpr term)) ((when okp) (b* (((erp (expr-gout test)) (atc-gen-expr-bool test-term gin state)) ((erp (expr-gout then)) (b* ((then-cond (untranslate$ test.term t state)) (then-premise (atc-premise-test then-cond)) (then-context (atc-context-extend gin.context (list then-premise)))) (atc-gen-expr-pure then-term (change-expr-gin gin :context then-context :thm-index test.thm-index :names-to-avoid test.names-to-avoid) state))) ((erp (expr-gout else)) (b* ((not-test-term (cons 'not (cons test.term 'nil))) (else-cond (untranslate$ not-test-term nil state)) (else-premise (atc-premise-test else-cond)) (else-context (atc-context-extend gin.context (list else-premise)))) (atc-gen-expr-pure else-term (change-expr-gin gin :context else-context :thm-index then.thm-index :names-to-avoid then.names-to-avoid) state)))) (atc-gen-expr-cond term test.term then.term else.term test.expr then.expr else.expr test.type then.type else.type test.thm-name then.thm-name else.thm-name test.events then.events else.events (change-expr-gin gin :thm-index else.thm-index :names-to-avoid else.names-to-avoid) state)))) (reterr (msg "When generating C code for the function ~x0, ~ at a point where ~ a pure expression term returning a C type is expected, ~ the term ~x1 is encountered instead, ~ which is not a C expression term returning a C type; ~ see the ATC user documentation." gin.fn term)))))
Function:
(defun atc-gen-expr-bool (term gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp term) (expr-ginp gin)))) (let ((__function__ 'atc-gen-expr-bool)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) ((expr-gin gin) gin) ((mv okp arg1-term arg2-term) (fty-check-and-call term)) ((when okp) (b* (((erp (expr-gout arg1)) (atc-gen-expr-bool arg1-term gin state)) (cond (untranslate$ arg1.term t state)) (premise (atc-premise-test cond)) (context (atc-context-extend gin.context (list premise))) ((erp (expr-gout arg2)) (atc-gen-expr-bool arg2-term (change-expr-gin gin :context context :thm-index arg1.thm-index :names-to-avoid arg1.names-to-avoid) state))) (retok (atc-gen-expr-and arg1.term arg2.term arg1.expr arg2.expr arg1.type arg2.type arg1.thm-name arg2.thm-name arg1.events arg2.events (change-expr-gin gin :thm-index arg2.thm-index :names-to-avoid arg2.names-to-avoid) state)))) ((mv okp arg1-term arg2-term) (fty-check-or-call term)) ((when okp) (b* (((erp (expr-gout arg1)) (atc-gen-expr-bool arg1-term gin state)) (cond (untranslate$ (cons 'not (cons arg1.term 'nil)) t state)) (premise (atc-premise-test cond)) (context (atc-context-extend gin.context (list premise))) ((erp (expr-gout arg2)) (atc-gen-expr-bool arg2-term (change-expr-gin gin :context context :thm-index arg1.thm-index :names-to-avoid arg1.names-to-avoid) state))) (retok (atc-gen-expr-or arg1.term arg2.term arg1.expr arg2.expr arg1.type arg2.type arg1.thm-name arg2.thm-name arg1.events arg2.events (change-expr-gin gin :thm-index arg2.thm-index :names-to-avoid arg2.names-to-avoid) state)))) ((erp okp fn arg-term in-type) (atc-check-boolean-from-type term)) ((when okp) (b* (((erp (expr-gout arg)) (atc-gen-expr-pure arg-term gin state)) (gin (change-expr-gin gin :thm-index arg.thm-index :names-to-avoid arg.names-to-avoid))) (atc-gen-expr-bool-from-type fn arg.term arg.expr arg.type arg.events arg.thm-name in-type gin state)))) (reterr (msg "When generating C code for the function ~x0, ~ at a point where ~ an expression term returning boolean is expected, ~ the term ~x1 is encountered instead, ~ which is not a C epxression term returning boolean; ~ see the ATC user documentation." gin.fn term)))))
Theorem:
(defthm return-type-of-atc-gen-expr-pure.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-pure term gin state))) (expr-goutp gout)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atc-gen-expr-bool.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-bool term gin state))) (expr-goutp gout)) :rule-classes :rewrite)