		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-funcall

Validate a function call expression, given the types of the sub-expressions.

Signature
(valid-funcall expr type-fun types-arg ienv) → (mv erp type)
Arguments: expr — Guard (exprp expr).; type-fun — Guard (typep type-fun).; types-arg — Guard (type-listp types-arg).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; type — Type (typep type).

After converting function types to pointer types, the first sub-expression must have pointer type [C17:6.5.2.2/1]; Furthermore, it must be a pointer to a function type.

There is no need to perform array-to-pointer conversion, because array types cannot have function element types, but only (complete) object element types [C17:6.2.5/20]. Thus, the conversion could never result into a pointer to a function.

When the function expression is a pointer to a function type which includes a prototype, we validate the arguments against the prototype parameter list [C17:6.5.2.2/2] (see valid-prototype-args). We return the function return type.

Definitions and Theorems

Function: valid-funcall

(defun valid-funcall (expr type-fun types-arg ienv)
 (declare (xargs :guard (and (exprp expr)
                             (typep type-fun)
                             (type-listp types-arg)
                             (ienvp ienv))))
 (declare
      (xargs :guard (and (expr-case expr :funcall)
                         (equal (len types-arg)
                                (len (expr-funcall->args expr))))))
 (b*
  (((reterr) (irr-type))
   ((when (type-case type-fun :unknown))
    (retok (type-unknown)))
   (type (type-fpconvert type-fun))
   ((unless (type-case type :pointer))
    (retmsg$
     "In the function call expression ~x0, ~
                  the first sub-expression is expected to have a pointer type, ~
                  but it has type ~x1."
     (expr-fix expr)
     (type-fix type-fun)))
   (to-type (type-pointer->to type))
   ((when (type-case to-type :unknown))
    (retok (type-unknown)))
   ((unless (type-case to-type :function))
    (retmsg$
     "In the function call expression ~x0, ~
                  the first sub-expression is expected
                  to have a function pointer or unknown pointer type,
                  but it has type ~x1."
     (expr-fix expr)
     (type-fix type-fun)))
   (type-params (type-function->params to-type))
   ((erp)
    (type-params-case
         type-params
         :prototype
         (valid-prototype-args type-params.params
                               (expr-funcall->args expr)
                               types-arg type-params.ellipsis ienv)
         :otherwise (retok))
    :iferr (msg$ "Error in function call ~x0:~%~@1"
                 (expr-fix expr)
                 erp)))
  (retok (type-function->ret to-type))))

Theorem: maybe-msgp-of-valid-funcall.erp

(defthm maybe-msgp-of-valid-funcall.erp
  (b* (((mv acl2::?erp ?type)
        (valid-funcall expr type-fun types-arg ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: typep-of-valid-funcall.type

(defthm typep-of-valid-funcall.type
  (b* (((mv acl2::?erp ?type)
        (valid-funcall expr type-fun types-arg ienv)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-funcall-of-expr-fix-expr

(defthm valid-funcall-of-expr-fix-expr
  (equal (valid-funcall (expr-fix expr)
                        type-fun types-arg ienv)
         (valid-funcall expr type-fun types-arg ienv)))

Theorem: valid-funcall-expr-equiv-congruence-on-expr

(defthm valid-funcall-expr-equiv-congruence-on-expr
  (implies
       (expr-equiv expr expr-equiv)
       (equal (valid-funcall expr type-fun types-arg ienv)
              (valid-funcall expr-equiv type-fun types-arg ienv)))
  :rule-classes :congruence)

Theorem: valid-funcall-of-type-fix-type-fun

(defthm valid-funcall-of-type-fix-type-fun
  (equal (valid-funcall expr (type-fix type-fun)
                        types-arg ienv)
         (valid-funcall expr type-fun types-arg ienv)))

Theorem: valid-funcall-type-equiv-congruence-on-type-fun

(defthm valid-funcall-type-equiv-congruence-on-type-fun
  (implies
       (type-equiv type-fun type-fun-equiv)
       (equal (valid-funcall expr type-fun types-arg ienv)
              (valid-funcall expr type-fun-equiv types-arg ienv)))
  :rule-classes :congruence)

Theorem: valid-funcall-of-type-list-fix-types-arg

(defthm valid-funcall-of-type-list-fix-types-arg
  (equal (valid-funcall expr type-fun (type-list-fix types-arg)
                        ienv)
         (valid-funcall expr type-fun types-arg ienv)))

Theorem: valid-funcall-type-list-equiv-congruence-on-types-arg

(defthm valid-funcall-type-list-equiv-congruence-on-types-arg
  (implies
       (type-list-equiv types-arg types-arg-equiv)
       (equal (valid-funcall expr type-fun types-arg ienv)
              (valid-funcall expr type-fun types-arg-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-funcall-of-ienv-fix-ienv

(defthm valid-funcall-of-ienv-fix-ienv
  (equal (valid-funcall expr type-fun types-arg (ienv-fix ienv))
         (valid-funcall expr type-fun types-arg ienv)))

Theorem: valid-funcall-ienv-equiv-congruence-on-ienv

(defthm valid-funcall-ienv-equiv-congruence-on-ienv
  (implies
       (ienv-equiv ienv ienv-equiv)
       (equal (valid-funcall expr type-fun types-arg ienv)
              (valid-funcall expr type-fun types-arg ienv-equiv)))
  :rule-classes :congruence)