invariant-risk

(defun tbody
  (fn wrld)
  (declare (xargs :mode :program))
  (or (body fn nil wrld)
    (let ((ev (get-defun-event fn wrld)))
      (and ev
        (mv-let (erp body)
          (translate-cmp (car (last ev))
            t
            nil
            t
            'tbody
            wrld
            (default-state-vars nil :temp-touchable-fns t))
          (cond (erp (er hard 'tbody "Unable to translate the body of ~x0." fn))
            (t body)))))))

(defun invariant-risk-callees1
  (body-fns fn wrld acc)
  (declare (xargs :guard (and (symbol-listp body-fns)
        (symbolp fn)
        (plist-worldp wrld)
        (true-listp acc))))
  (cond ((endp body-fns) acc)
    (t (invariant-risk-callees1 (cdr body-fns)
        fn
        wrld
        (if (and (getpropc (car body-fns) 'invariant-risk nil wrld)
            (not (member-eq (car body-fns) acc))
            (not (eq (car body-fns) fn)))
          (cons (car body-fns) acc)
          acc)))))

(defun invariant-risk-callees
  (fn wrld)
  (declare (xargs :mode :program :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((prop (getpropc fn 'invariant-risk nil wrld)))
    (cond ((null prop) nil)
      ((eq prop fn) prop)
      (t (invariant-risk-callees1 (all-fnnames1-exec nil (tbody fn wrld) nil)
          fn
          wrld
          nil)))))

(defun invariant-risk-call-path-rec
  (fns exceptions wrld)
  (declare (xargs :mode :program :guard (and (symbol-listp fns)
        (symbol-listp exceptions)
        (plist-worldp wrld))))
  (cond ((endp fns) (mv nil exceptions))
    (t (let* ((fn (car fns)) (e (member-eq fn exceptions))
          (prop (and (not e) (getpropc fn 'invariant-risk nil wrld))))
        (cond ((null prop) (invariant-risk-call-path-rec (cdr fns)
              (if e
                exceptions
                (cons fn exceptions))
              wrld))
          ((eq prop fn) (mv (list fn) exceptions))
          (t (mv-let (path exceptions)
              (invariant-risk-call-path-rec (all-fnnames1-exec nil (tbody fn wrld) nil)
                (add-to-set-eq fn exceptions)
                wrld)
              (cond (path (mv (cons fn path) exceptions))
                (t (invariant-risk-call-path-rec (cdr fns)
                    (add-to-set-eq fn exceptions)
                    wrld))))))))))

(defun invariant-risk-call-path
  (fn exceptions wrld)
  (declare (xargs :mode :program :guard (and (symbolp fn)
        (symbol-listp exceptions)
        (plist-worldp wrld))))
  (mv-let (path exceptions)
    (invariant-risk-call-path-rec (list fn) exceptions wrld)
    (declare (ignore exceptions))
    path))

(defun invariant-risk-call-path-alist
  (fns exceptions alist wrld)
  (declare (xargs :mode :program :guard (and (symbol-listp fns)
        (symbol-listp exceptions)
        (true-listp alist)
        (plist-worldp wrld))))
  (cond ((endp fns) (mv (reverse alist) (reverse exceptions)))
    ((member-eq (car fns) exceptions) (invariant-risk-call-path-alist (cdr fns)
        exceptions
        alist
        wrld))
    (t (mv-let (path exceptions)
        (invariant-risk-call-path-rec (list (car fns))
          exceptions
          wrld)
        (cond (path (invariant-risk-call-path-alist (cdr fns)
              exceptions
              (cons path alist)
              wrld))
          (t (invariant-risk-call-path-alist (cdr fns)
              exceptions
              alist
              wrld)))))))