		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Check-safe-expressions

Check if expressions are safe.

These are checked in the context of a variable table and a function table.

Definitions and Theorems

Function: check-safe-expression

(defun check-safe-expression (expr varset funtab)
  (declare (xargs :guard (and (expressionp expr)
                              (identifier-setp varset)
                              (funtablep funtab))))
  (let ((__function__ 'check-safe-expression))
    (declare (ignorable __function__))
    (expression-case
         expr :path
         (b* (((okf &)
               (check-safe-path expr.get varset)))
           1)
         :literal
         (b* (((okf &) (check-safe-literal expr.get)))
           1)
         :funcall (check-safe-funcall expr.get varset funtab))))

Function: check-safe-expression-list

(defun check-safe-expression-list (exprs varset funtab)
 (declare (xargs :guard (and (expression-listp exprs)
                             (identifier-setp varset)
                             (funtablep funtab))))
 (let ((__function__ 'check-safe-expression-list))
  (declare (ignorable __function__))
  (b*
   (((when (endp exprs)) 0)
    ((okf n)
     (check-safe-expression (car exprs)
                            varset funtab))
    ((unless (= n 1))
     (reserrf
         (list :multi-value-argument (expression-fix (car exprs)))))
    ((okf n)
     (check-safe-expression-list (cdr exprs)
                                 varset funtab)))
   (1+ n))))

Function: check-safe-funcall

(defun check-safe-funcall (call varset funtab)
  (declare (xargs :guard (and (funcallp call)
                              (identifier-setp varset)
                              (funtablep funtab))))
  (let ((__function__ 'check-safe-funcall))
    (declare (ignorable __function__))
    (b* (((funcall call) call)
         ((okf funty)
          (get-funtype call.name funtab))
         ((okf n)
          (check-safe-expression-list call.args varset funtab))
         ((unless (= n (funtype->in funty)))
          (reserrf (list :mismatched-formals-actuals
                         :required (funtype->in funty)
                         :supplied n))))
      (funtype->out funty))))

Theorem: return-type-of-check-safe-expression.results?

(defthm return-type-of-check-safe-expression.results?
  (b* ((?results? (check-safe-expression expr varset funtab)))
    (nat-resultp results?))
  :rule-classes :rewrite)

Theorem: return-type-of-check-safe-expression-list.number?

(defthm return-type-of-check-safe-expression-list.number?
  (b* ((?number? (check-safe-expression-list exprs varset funtab)))
    (nat-resultp number?))
  :rule-classes :rewrite)

Theorem: return-type-of-check-safe-funcall.results?

(defthm return-type-of-check-safe-funcall.results?
  (b* ((?results? (check-safe-funcall call varset funtab)))
    (nat-resultp results?))
  :rule-classes :rewrite)

Theorem: check-safe-expression-of-expression-fix-expr

(defthm check-safe-expression-of-expression-fix-expr
  (equal (check-safe-expression (expression-fix expr)
                                varset funtab)
         (check-safe-expression expr varset funtab)))

Theorem: check-safe-expression-of-identifier-set-fix-varset

(defthm check-safe-expression-of-identifier-set-fix-varset
  (equal (check-safe-expression expr (identifier-set-fix varset)
                                funtab)
         (check-safe-expression expr varset funtab)))

Theorem: check-safe-expression-of-funtable-fix-funtab

(defthm check-safe-expression-of-funtable-fix-funtab
  (equal (check-safe-expression expr varset (funtable-fix funtab))
         (check-safe-expression expr varset funtab)))

Theorem: check-safe-expression-list-of-expression-list-fix-exprs

(defthm check-safe-expression-list-of-expression-list-fix-exprs
  (equal (check-safe-expression-list (expression-list-fix exprs)
                                     varset funtab)
         (check-safe-expression-list exprs varset funtab)))

Theorem: check-safe-expression-list-of-identifier-set-fix-varset

(defthm check-safe-expression-list-of-identifier-set-fix-varset
  (equal
       (check-safe-expression-list exprs (identifier-set-fix varset)
                                   funtab)
       (check-safe-expression-list exprs varset funtab)))

Theorem: check-safe-expression-list-of-funtable-fix-funtab

(defthm check-safe-expression-list-of-funtable-fix-funtab
 (equal
     (check-safe-expression-list exprs varset (funtable-fix funtab))
     (check-safe-expression-list exprs varset funtab)))

Theorem: check-safe-funcall-of-funcall-fix-call

(defthm check-safe-funcall-of-funcall-fix-call
  (equal (check-safe-funcall (funcall-fix call)
                             varset funtab)
         (check-safe-funcall call varset funtab)))

Theorem: check-safe-funcall-of-identifier-set-fix-varset

(defthm check-safe-funcall-of-identifier-set-fix-varset
  (equal (check-safe-funcall call (identifier-set-fix varset)
                             funtab)
         (check-safe-funcall call varset funtab)))

Theorem: check-safe-funcall-of-funtable-fix-funtab

(defthm check-safe-funcall-of-funtable-fix-funtab
  (equal (check-safe-funcall call varset (funtable-fix funtab))
         (check-safe-funcall call varset funtab)))

Theorem: check-safe-expression-expression-equiv-congruence-on-expr

(defthm check-safe-expression-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (check-safe-expression expr varset funtab)
                  (check-safe-expression expr-equiv varset funtab)))
  :rule-classes :congruence)

Theorem: check-safe-expression-identifier-set-equiv-congruence-on-varset

(defthm
    check-safe-expression-identifier-set-equiv-congruence-on-varset
  (implies (identifier-set-equiv varset varset-equiv)
           (equal (check-safe-expression expr varset funtab)
                  (check-safe-expression expr varset-equiv funtab)))
  :rule-classes :congruence)

Theorem: check-safe-expression-funtable-equiv-congruence-on-funtab

(defthm check-safe-expression-funtable-equiv-congruence-on-funtab
  (implies (funtable-equiv funtab funtab-equiv)
           (equal (check-safe-expression expr varset funtab)
                  (check-safe-expression expr varset funtab-equiv)))
  :rule-classes :congruence)

Theorem: check-safe-expression-list-expression-list-equiv-congruence-on-exprs

(defthm
 check-safe-expression-list-expression-list-equiv-congruence-on-exprs
 (implies
     (expression-list-equiv exprs exprs-equiv)
     (equal (check-safe-expression-list exprs varset funtab)
            (check-safe-expression-list exprs-equiv varset funtab)))
 :rule-classes :congruence)

Theorem: check-safe-expression-list-identifier-set-equiv-congruence-on-varset

(defthm
 check-safe-expression-list-identifier-set-equiv-congruence-on-varset
 (implies
     (identifier-set-equiv varset varset-equiv)
     (equal (check-safe-expression-list exprs varset funtab)
            (check-safe-expression-list exprs varset-equiv funtab)))
 :rule-classes :congruence)

Theorem: check-safe-expression-list-funtable-equiv-congruence-on-funtab

(defthm
     check-safe-expression-list-funtable-equiv-congruence-on-funtab
 (implies
     (funtable-equiv funtab funtab-equiv)
     (equal (check-safe-expression-list exprs varset funtab)
            (check-safe-expression-list exprs varset funtab-equiv)))
 :rule-classes :congruence)

Theorem: check-safe-funcall-funcall-equiv-congruence-on-call

(defthm check-safe-funcall-funcall-equiv-congruence-on-call
  (implies (funcall-equiv call call-equiv)
           (equal (check-safe-funcall call varset funtab)
                  (check-safe-funcall call-equiv varset funtab)))
  :rule-classes :congruence)

Theorem: check-safe-funcall-identifier-set-equiv-congruence-on-varset

(defthm check-safe-funcall-identifier-set-equiv-congruence-on-varset
  (implies (identifier-set-equiv varset varset-equiv)
           (equal (check-safe-funcall call varset funtab)
                  (check-safe-funcall call varset-equiv funtab)))
  :rule-classes :congruence)

Theorem: check-safe-funcall-funtable-equiv-congruence-on-funtab

(defthm check-safe-funcall-funtable-equiv-congruence-on-funtab
  (implies (funtable-equiv funtab funtab-equiv)
           (equal (check-safe-funcall call varset funtab)
                  (check-safe-funcall call varset funtab-equiv)))
  :rule-classes :congruence)

Subtopics

Check-safe-expression-list: Check if a list of expressions is safe.
Check-safe-expression: Check if an expression is safe.
Check-safe-funcall: Check if a function call is safe.