Generate a C expression from an ACL2 term that represents an indirection of a pointer to integer.
(atc-gen-expr-integer-read fn arg-term arg-expr arg-type arg-events arg-thm type gin state) → (mv erp gout)
The expression and theorem for the argument are generated in the caller, and passed here.
Currently, the argument term must be an ACL2 variable.
We defensively check that it is the case.
The generated theorem needs not only the theorem about the argument,
but also the theorem about the variable in the symbol table.
The reason is that the theorem about the argument
just says that the execution of the C variable
yields the ACL2
Function:
(defun atc-gen-expr-integer-read (fn arg-term arg-expr arg-type arg-events arg-thm type gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (pseudo-termp arg-term) (exprp arg-expr) (typep arg-type) (pseudo-event-form-listp arg-events) (symbolp arg-thm) (typep type) (expr-ginp gin)))) (declare (xargs :guard (type-nonchar-integerp type))) (let ((__function__ 'atc-gen-expr-integer-read)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr-gout)) ((expr-gin gin) gin) ((unless (equal arg-type (type-pointer type))) (reterr (msg "The indirection operator representation for integer type ~x0 ~ is applied to an expression term ~x1 returning ~x2, ~ but a ~x3 operand is expected. ~ This is indicative of provably dead code, ~ given that the code is guard-verified." type arg-term arg-type (type-pointer type)))) (expr (make-expr-unary :op (unop-indir) :arg arg-expr)) (term (cons fn (cons arg-term 'nil))) ((when (not gin.proofs)) (retok (make-expr-gout :expr expr :type type :term term :events arg-events :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid))) ((unless (symbolp arg-term)) (reterr (raise "Interal error: indirection applied to non-variable ~x0." arg-term))) (info (atc-get-var arg-term gin.inscope)) ((unless info) (reterr (raise "Internal error: variable ~x0 not found in scope." arg-term))) (var-thm (atc-var-info->thm info)) (hints (b* ((type-pred (atc-type-to-recognizer type gin.prec-tags)) (exec-indir-when-type-pred (pack 'exec-indir-when- type-pred)) (type-read (pack (type-kind type) '-read)) (type-read-when-type-pred (pack type-read '-when- type-pred))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-pure-when-unary (cons '(:e expr-kind) (cons '(:e expr-unary->arg) (cons '(:e expr-unary->op) (cons arg-thm (cons 'expr-valuep-of-expr-value (cons exec-indir-when-type-pred (cons '(:e unop-kind) (cons var-thm (cons type-read-when-type-pred 'nil)))))))))) 'nil)) 'nil))) 'nil))) (objdes (add-suffix-to-fn arg-term "-OBJDES")) ((mv thm-event thm-name thm-index names-to-avoid) (atc-gen-expr-pure-correct-thm gin.fn gin.fn-guard gin.context expr type term term objdes gin.compst-var hints nil gin.prec-tags gin.thm-index gin.names-to-avoid state))) (retok (make-expr-gout :expr expr :type type :term term :events (append arg-events (list thm-event)) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid)))))
Theorem:
(defthm expr-goutp-of-atc-gen-expr-integer-read.gout (b* (((mv acl2::?erp ?gout) (atc-gen-expr-integer-read fn arg-term arg-expr arg-type arg-events arg-thm type gin state))) (expr-goutp gout)) :rule-classes :rewrite)