		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Expr-pure-formalp

Check if an expression has formal dynamic semantics, as a pure expression.

Signature
(expr-pure-formalp expr) → yes/no
Arguments: expr — Guard (exprp expr).
Returns: yes/no — Type (booleanp yes/no).

Our formal semantics of C characterizes certain expressions as pure, and restricts certain expressions in the syntax to be pure. Thus, here we define a predicate that says whether an expression has formal semantics as a pure expression. Later we define other predicates for other kinds of expressions.

The expressions not supported by ldm-expr are not supported here either. The remaining expressions are supported or not according to c::exec-expr-pure and the specialized functions it calls (e.g. c::exec-arrsub). In order for an expression to be supported, it is necessary that its sub-expressions are supported.

The tests for identifiers and constants reduce to the ones defined in predicates defined earlier.

Parenthesized expressions lose the parentheses through ldm-expr, so they are supported if and only if the unparenthesized versions are.

The check we perform here on cast expressions is an over-approximation of what we should check. It is not enough for the destination type to be integer; we should also check that the source value is an integer. But this cannot be done purely syntactically: we need type information, about the type of the argument expression. After we have a validator, if the validator annotates the abstract syntax with type information, then we could make this check more precise.

Definitions and Theorems

Function: expr-pure-formalp

(defun expr-pure-formalp (expr)
 (declare (xargs :guard (exprp expr)))
 (declare (xargs :guard (expr-unambp expr)))
 (let ((__function__ 'expr-pure-formalp))
  (declare (ignorable __function__))
  (expr-case
      expr
      :ident (ident-formalp expr.ident)
      :const (const-formalp expr.const)
      :string nil
      :paren (expr-pure-formalp expr.inner)
      :gensel nil
      :arrsub (and (expr-pure-formalp expr.arg1)
                   (expr-pure-formalp expr.arg2))
      :funcall nil
      :member (expr-pure-formalp expr.arg)
      :memberp (expr-pure-formalp expr.arg)
      :complit nil
      :unary (unop-case expr.op
                        :address (expr-pure-formalp expr.arg)
                        :indir (expr-pure-formalp expr.arg)
                        :plus (expr-pure-formalp expr.arg)
                        :minus (expr-pure-formalp expr.arg)
                        :bitnot (expr-pure-formalp expr.arg)
                        :lognot (expr-pure-formalp expr.arg)
                        :preinc nil
                        :predec nil
                        :postinc nil
                        :postdec nil
                        :sizeof nil)
      :sizeof nil
      :sizeof-ambig (impossible)
      :alignof nil
      :cast (and (tyname-formalp expr.type)
                 (expr-pure-formalp expr.arg))
      :binary (and (member-eq (binop-kind expr.op)
                              '(:mul :div
                                     :rem :add
                                     :sub :shl
                                     :shr :lt
                                     :gt :le
                                     :ge :eq
                                     :ne :bitand
                                     :bitxor :bitior
                                     :logand :logor))
                   (expr-pure-formalp expr.arg1)
                   (expr-pure-formalp expr.arg2))
      :cond
      (and (expr-pure-formalp expr.test)
           (expr-option-case expr.then
                             :some (expr-pure-formalp expr.then.val)
                             :none t)
           (expr-pure-formalp expr.else))
      :comma nil
      :cast/call-ambig (impossible)
      :cast/mul-ambig (impossible)
      :cast/add-ambig (impossible)
      :cast/sub-ambig (impossible)
      :cast/and-ambig (impossible)
      :stmt nil
      :tycompat nil
      :offsetof nil
      :va-arg nil
      :extension nil)))

Theorem: booleanp-of-expr-pure-formalp

(defthm booleanp-of-expr-pure-formalp
  (b* ((yes/no (expr-pure-formalp expr)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: expr-pure-formalp-of-expr-fix-expr

(defthm expr-pure-formalp-of-expr-fix-expr
  (equal (expr-pure-formalp (expr-fix expr))
         (expr-pure-formalp expr)))

Theorem: expr-pure-formalp-expr-equiv-congruence-on-expr

(defthm expr-pure-formalp-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (expr-pure-formalp expr)
                  (expr-pure-formalp expr-equiv)))
  :rule-classes :congruence)