		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-atc

Atc-check-cfun-call

Check if a term may represent a call to a C function, and in that case check the requirements on the call arguments.

Signature
(atc-check-cfun-call term var-term-alist prec-fns wrld) → (mv erp yes/no fn args in-types out-type affect extobjs limit fn-guard)
Arguments: term — Guard (pseudo-termp term).; var-term-alist — Guard (symbol-pseudoterm-alistp var-term-alist).; prec-fns — Guard (atc-symbol-fninfo-alistp prec-fns).; wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn).; args — Type (pseudo-term-listp args).; in-types — Type (type-listp in-types).; out-type — Type (typep out-type).; affect — Type (symbol-listp affect).; extobjs — Type (symbol-listp extobjs).; limit — Type (pseudo-termp limit).; fn-guard — Type (symbolp fn-guard).

If the check is successful, we return the called function along with the arguments. We also return the input and output types of the function, the variables affected by the function, the formals of the function that represent external objects, the limit sufficient to execute the function, and the local function that encapsulates the function's guard.

We also check each actual argument for a formal parameter of array or pointer type, or for a formal parameter that represents an external object, is identical to the formal, as required in the ATC user documentation.

The limit retrieved from the function table refers to the formal parameters. We must instantiate it to the actual parameters in order to obtain an appropriate limit for the call, but we also need to substitute all the bindings in order to obtain the real arguments of the call from the point of view of the top level of where this call term occurs.

Definitions and Theorems

Function: atc-check-cfun-call-args

(defun atc-check-cfun-call-args
       (fn formals actuals in-types extobjs)
 (declare (xargs :guard (and (symbolp fn)
                             (symbol-listp formals)
                             (pseudo-term-listp actuals)
                             (type-listp in-types)
                             (symbol-listp extobjs))))
 (let ((__function__ 'atc-check-cfun-call-args))
  (declare (ignorable __function__))
  (b*
   (((reterr))
    ((when (endp formals))
     (cond ((consp actuals)
            (reterr (raise "Internal error: extra actuals ~x0."
                           actuals)))
           ((consp in-types)
            (reterr (raise "Internal error: extra types ~x0."
                           in-types)))
           (t (retok))))
    ((when (or (endp actuals) (endp in-types)))
     (reterr (raise "Internal error: extra formals ~x0."
                    formals)))
    (formal (car formals))
    (actual (car actuals))
    (in-type (car in-types))
    ((when (and (not (type-case in-type :pointer))
                (not (type-case in-type :array))
                (not (member-eq formal extobjs))))
     (atc-check-cfun-call-args fn (cdr formals)
                               (cdr actuals)
                               (cdr in-types)
                               extobjs))
    ((unless (eq formal actual))
     (reterr
      (msg
       "Since the formal parameter ~x0 of ~x1 ~
                  has array or pointer type, ~
                  or represents an external object, ~
                  the actual argument passed to the call must be ~
                  identical to the formal parameters, ~
                  but it is ~x2 instead."
       formal fn actual))))
   (atc-check-cfun-call-args fn (cdr formals)
                             (cdr actuals)
                             (cdr in-types)
                             extobjs))))

Function: atc-check-cfun-call

(defun atc-check-cfun-call (term var-term-alist prec-fns wrld)
  (declare
       (xargs :guard (and (pseudo-termp term)
                          (symbol-pseudoterm-alistp var-term-alist)
                          (atc-symbol-fninfo-alistp prec-fns)
                          (plist-worldp wrld))))
  (let ((__function__ 'atc-check-cfun-call))
    (declare (ignorable __function__))
    (b* (((reterr)
          nil nil nil nil (irr-type)
          nil nil nil nil)
         ((acl2::fun (no))
          (retok nil nil nil nil (irr-type)
                 nil nil nil nil))
         ((unless (pseudo-term-case term :fncall))
          (no))
         ((pseudo-term-fncall term) term)
         ((when (irecursivep+ term.fn wrld))
          (no))
         (fn+info (assoc-eq term.fn
                            (atc-symbol-fninfo-alist-fix prec-fns)))
         ((unless (consp fn+info)) (no))
         (info (cdr fn+info))
         (in-types (atc-fn-info->in-types info))
         (out-type (atc-fn-info->out-type info))
         (affect (atc-fn-info->affect info))
         (extobjs (atc-fn-info->extobjs info))
         ((when (null out-type)) (no))
         (limit (atc-fn-info->limit info))
         (limit (fty-fsublis-var var-term-alist limit))
         (fn-guard (atc-fn-info->guard info))
         ((erp)
          (atc-check-cfun-call-args term.fn (formals+ term.fn wrld)
                                    term.args in-types extobjs)))
      (retok t term.fn term.args in-types out-type
             affect extobjs limit fn-guard))))

Theorem: booleanp-of-atc-check-cfun-call.yes/no

(defthm booleanp-of-atc-check-cfun-call.yes/no
  (b* (((mv acl2::?erp ?yes/no
            ?fn acl2::?args ?in-types ?out-type
            ?affect ?extobjs ?limit ?fn-guard)
        (atc-check-cfun-call term var-term-alist prec-fns wrld)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-cfun-call.fn

(defthm symbolp-of-atc-check-cfun-call.fn
  (b* (((mv acl2::?erp ?yes/no
            ?fn acl2::?args ?in-types ?out-type
            ?affect ?extobjs ?limit ?fn-guard)
        (atc-check-cfun-call term var-term-alist prec-fns wrld)))
    (symbolp fn))
  :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-atc-check-cfun-call.args

(defthm pseudo-term-listp-of-atc-check-cfun-call.args
  (b* (((mv acl2::?erp ?yes/no
            ?fn acl2::?args ?in-types ?out-type
            ?affect ?extobjs ?limit ?fn-guard)
        (atc-check-cfun-call term var-term-alist prec-fns wrld)))
    (pseudo-term-listp args))
  :rule-classes :rewrite)

Theorem: type-listp-of-atc-check-cfun-call.in-types

(defthm type-listp-of-atc-check-cfun-call.in-types
  (b* (((mv acl2::?erp ?yes/no
            ?fn acl2::?args ?in-types ?out-type
            ?affect ?extobjs ?limit ?fn-guard)
        (atc-check-cfun-call term var-term-alist prec-fns wrld)))
    (type-listp in-types))
  :rule-classes :rewrite)

Theorem: typep-of-atc-check-cfun-call.out-type

(defthm typep-of-atc-check-cfun-call.out-type
  (b* (((mv acl2::?erp ?yes/no
            ?fn acl2::?args ?in-types ?out-type
            ?affect ?extobjs ?limit ?fn-guard)
        (atc-check-cfun-call term var-term-alist prec-fns wrld)))
    (typep out-type))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-check-cfun-call.affect

(defthm symbol-listp-of-atc-check-cfun-call.affect
  (b* (((mv acl2::?erp ?yes/no
            ?fn acl2::?args ?in-types ?out-type
            ?affect ?extobjs ?limit ?fn-guard)
        (atc-check-cfun-call term var-term-alist prec-fns wrld)))
    (symbol-listp affect))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-check-cfun-call.extobjs

(defthm symbol-listp-of-atc-check-cfun-call.extobjs
  (b* (((mv acl2::?erp ?yes/no
            ?fn acl2::?args ?in-types ?out-type
            ?affect ?extobjs ?limit ?fn-guard)
        (atc-check-cfun-call term var-term-alist prec-fns wrld)))
    (symbol-listp extobjs))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-check-cfun-call.limit

(defthm pseudo-termp-of-atc-check-cfun-call.limit
  (b* (((mv acl2::?erp ?yes/no
            ?fn acl2::?args ?in-types ?out-type
            ?affect ?extobjs ?limit ?fn-guard)
        (atc-check-cfun-call term var-term-alist prec-fns wrld)))
    (pseudo-termp limit))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-cfun-call.fn-guard

(defthm symbolp-of-atc-check-cfun-call.fn-guard
  (b* (((mv acl2::?erp ?yes/no
            ?fn acl2::?args ?in-types ?out-type
            ?affect ?extobjs ?limit ?fn-guard)
        (atc-check-cfun-call term var-term-alist prec-fns wrld)))
    (symbolp fn-guard))
  :rule-classes :rewrite)

Theorem: pseudo-term-count-of-atc-check-cfun-call

(defthm pseudo-term-count-of-atc-check-cfun-call
  (b* (((mv acl2::?erp ?yes/no
            ?fn acl2::?args ?in-types ?out-type
            ?affect ?extobjs ?limit ?fn-guard)
        (atc-check-cfun-call term var-term-alist prec-fns wrld)))
    (implies yes/no
             (< (pseudo-term-list-count args)
                (pseudo-term-count term))))
  :rule-classes :linear)