		Search-engine friendly clone of the ACL2 documentation.

Atc-expression-generation

Atc-gen-expr-pure/bool

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 nil, i.e. false), but the resulting C code may not compile. The additional type checking we do here should ensure that all the code satisfies the C static semantics.

Definitions and Theorems

Function: atc-gen-expr-pure

(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: atc-gen-expr-bool

(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 expression term returning boolean; ~
             see the ATC user documentation."
     gin.fn term)))))

Theorem: return-type-of-atc-gen-expr-pure.gout

(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: return-type-of-atc-gen-expr-bool.gout

(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)

Subtopics

Atc-gen-expr-bool: Generate a C expression from an ACL2 term that must be an expression term returning a boolean.
Atc-gen-expr-pure: Generate a C expression from an ACL2 term that must be a pure expression term.