Filtering...

cgen-rules

books/acl2s/cgen/cgen-rules
other
(in-package "CGEN")
other
(include-book "acl2s/defdata/defdata-util" :dir :system)
other
(include-book "utilities")
other
(table fixer-rules-table nil nil :clear)
other
(table preservation-rules-table nil nil :clear)
other
(def-const *cgen-rule-keywords*
  '(:test-hyp :hyp :meta-precondition :rule :rule-classes :override-check :verbose))
other
(def-const *cgen-rule-classes*
  '(:fixer :preservation))
define-rulemacro
(defmacro define-rule
  (name &rest keys)
  (b* ((verbosep (let ((lst (member :verbose keys)))
         (and lst (cadr lst)))) (keys (remove-keywords-from-args '(:verbose) keys)))
    `(with-output ,@(AND (NOT CGEN::VERBOSEP)
       '(:OFF :ALL :SUMMARY-OFF :ALL :ON (ERROR CGEN::COMMENT)))
      :stack :push (make-event (cgen-rule-events ',CGEN::NAME
          ',CGEN::KEYS
          ',CGEN::VERBOSEP
          (w state)
          state)))))
guard-obligation/without-checkfunction
(defun guard-obligation/without-check
  (term guard-debug state)
  (declare (xargs :mode :program :stobjs (state)))
  (mv-let (cl-set cl-set-ttree)
    (guard-obligation-clauses (cons :term term)
      guard-debug
      (ens state)
      (w state)
      state)
    (value (list* term cl-set cl-set-ttree))))
body-contracts-obligationmacro
(defmacro body-contracts-obligation
  (term &key guard-debug)
  `(er-let* ((tuple (guard-obligation/without-check ,CGEN::TERM
         ',CGEN::GUARD-DEBUG
         state)))
    (cond ((eq tuple :redundant) (value :redundant))
      (t (let ((displayed-goal (prettyify-clause-set (cadr tuple)
               (let*-abstractionp state)
               (w state))))
          (value displayed-goal))))))
destruct-mv1function
(defun destruct-mv1
  (n mv-exp arity ans)
  (if (zp n)
    ans
    (b* ((i (1- n)))
      (destruct-mv1 (1- n)
        mv-exp
        arity
        (cons (list 'mv-nth
            (kwote i)
            (list 'mv-list (kwote arity) mv-exp))
          ans)))))
destruct-mvfunction
(defun destruct-mv
  (mv-exp arity wrld)
  (declare (xargs :mode :program))
  (if (zp arity)
    (er hard?
      'destruct-mv
      "~| ~x0 arity not legal.~%"
      arity)
    (if (<= arity 1)
      (list mv-exp)
      (b* ((possible-list-exp (untranslate mv-exp nil wrld)) ((when (and (consp possible-list-exp)
               (eq (car possible-list-exp) 'list))) (cdr possible-list-exp)))
        (destruct-mv1 arity
          mv-exp
          arity
          'nil)))))
other
(program)
other
(set-state-ok t)
translate-cmp-lstfunction
(defun translate-cmp-lst
  (xs stobjs-out
    logic-modep
    known-stobjs
    ctx
    w
    state-vars)
  (if (endp xs)
    (value-cmp nil)
    (b* (((cmp term) (translate-cmp (car xs)
           stobjs-out
           logic-modep
           known-stobjs
           ctx
           w
           state-vars)) ((cmp rest-terms) (translate-cmp-lst (cdr xs)
            stobjs-out
            logic-modep
            known-stobjs
            ctx
            w
            state-vars)))
      (value-cmp (cons term rest-terms)))))
destructure-fixer-rulefunction
(defun destructure-fixer-rule
  (rule)
  (cond ((and (= 4 (len rule))
       (eq (car rule) 'mv-let)) (b* ((`(mv-let ,CGEN::OUT ,CGEN::FIXER-EXP ,CGEN::CONSTRAINT) rule))
        (list out fixer-exp constraint)))
    ((and (= 3 (len rule))
       (eq (car rule) 'let)
       (= 1 (len (second rule)))) (b* ((`(let ((,CGEN::Y ,CGEN::FIXER-EXP))
            ,CGEN::CONSTRAINT) rule))
        (list (list y) fixer-exp constraint)))
    (t (er hard?
        'destructure-fixer-rule
        "~| ~x0 is not a fixer rule.~%"
        rule))))
make-cgen-rule-events/fixerfunction
(defun make-cgen-rule-events/fixer
  (rule kwd-alist
    override-checkp
    verbosep
    ctx
    wrld
    state)
  (b* (((list out fixer-exp constraint) (destructure-fixer-rule rule)) ((unless (and (proper-symbol-listp out)
           (> (len out) 0))) (er soft
          ctx
          "~| ~x0 is not a non-empty list of variable names.~%"
          out))
      ((er constraint-term) (translate constraint
          t
          nil
          t
          ctx
          wrld
          state))
      ((er fixer-term) (translate fixer-exp
          t
          nil
          t
          ctx
          wrld
          state))
      (in (reverse (all-vars fixer-term)))
      (mv-expanded-fixer-terms (destruct-mv fixer-term
          (len out)
          wrld))
      (fixer-binding (listlis out mv-expanded-fixer-terms))
      (vars (reverse (all-vars constraint-term)))
      ((unless (and (subsetp-eq vars
             (union-eq in out))
           (subsetp-eq out vars))) (er soft
          ctx
          "~| Invariant doesnt hold: ~x0 subsetof ~x1 and ~x2 subsetof ~x0~%"
          vars
          (union-eq in out)
          out))
      (rule-metadata (list (cons :in in)
          (cons :out out)
          (cons :fixer-vars (union-eq in out))
          (cons :fixer-term fixer-term)
          (cons :constraint-vars vars)
          (cons :constraint-term constraint-term)
          (cons :fixer-let-binding fixer-binding)))
      (rule-metadata (append kwd-alist rule-metadata))
      (key (cons constraint-term fixer-term))
      (fixer-table-alist (table-alist 'fixer-rules-table wrld))
      ((when (assoc-equal key fixer-table-alist)) (er soft
          ctx
          "~| Duplicate entry found in fixer-rules-table: ~x0~%"
          key))
      (table-ev `((table fixer-rules-table
           ',CGEN::KEY
           ',CGEN::RULE-METADATA
           :put)))
      (hyps (union-equal (get1 :hyps rule-metadata)
          (get1 :test-hyps rule-metadata)))
      (vl (if verbosep
          4
          1))
      (proof-obligation4 (if (> (len out) 1)
          `(implies (and . ,CGEN::HYPS)
            (mv-let ,CGEN::OUT
              ,CGEN::FIXER-TERM
              ,CGEN::CONSTRAINT-TERM))
          `(implies (and . ,CGEN::HYPS)
            (let ((,(CAR CGEN::OUT) ,CGEN::FIXER-TERM))
              ,CGEN::CONSTRAINT-TERM))))
      (invariant4-ev `((test? ,CGEN::PROOF-OBLIGATION4
           :verbosity-level ,CGEN::VL)))
      ((mv erp guard-ob state) (body-contracts-obligation fixer-term
          :guard-debug verbosep))
      ((when erp) (er soft
          ctx
          "~| guard-obligation error~%"))
      (proof-obligation1 `(implies (and . ,CGEN::HYPS) ,CGEN::GUARD-OB))
      (invariant1-ev `((test? ,CGEN::PROOF-OBLIGATION1
           :verbosity-level ,CGEN::VL)))
      (proof-obligation3 `(implies (and . ,CGEN::HYPS)
          (let ,CGEN::FIXER-BINDING
            (declare (ignorable ,@(CGEN::STRIP-CARS CGEN::FIXER-BINDING)))
            (and . ,CGEN::HYPS))))
      (invariant3-ev (and hyps
          `((test? ,CGEN::PROOF-OBLIGATION3
             :verbosity-level ,CGEN::VL)))))
    (value (append (and (not override-checkp)
          `((value-triple (cw? t
               "~|Test? obligation: Body contracts of fixer term should be satisfied. ~% ~x0~%"
               ',CGEN::PROOF-OBLIGATION1))))
        (and (not override-checkp) invariant1-ev)
        (and hyps
          (not override-checkp)
          `((value-triple (cw? t
               "~|Test? Obligation: Hypotheses should be preserved through fixer changes. ~x0~%"
               ',CGEN::PROOF-OBLIGATION3))))
        (and (not override-checkp) invariant3-ev)
        (and (not override-checkp)
          `((value-triple (cw? t
               "~|Test? Obligation: Fixer rule should be valid under hypotheses. ~x0~%"
               ',CGEN::PROOF-OBLIGATION4))))
        (and (not override-checkp) invariant4-ev)
        table-ev))))
destructure-preservation-rulefunction
(defun destructure-preservation-rule
  (rule wrld)
  (declare (ignorable wrld))
  (b* ((`(implies ,CGEN::CONSTRAINT1 ,CGEN::CONCL) rule) (ctx 'destructure-preservation-rule))
    (cond ((eq (car concl) 'mv-let) (b* ((`(mv-let ,CGEN::OUT
              ,CGEN::SINGLE-MV-FIXER-EXP
              ,CGEN::CONSTRAINT) concl))
          (list :mv out
            (list single-mv-fixer-exp)
            constraint1
            constraint)))
      ((eq (car concl) 'let) (b* ((`(let ,CGEN::FIXER-BINDING
              ,CGEN::CONSTRAINT) concl) (out (strip-cars fixer-binding))
            (fixer-exps (strip-cadrs fixer-binding)))
          (list :let out
            fixer-exps
            constraint1
            constraint)))
      (t (er hard?
          ctx
          "~| ~x0 is not a preservation rule.~%"
          rule)))))
assoc-equal-lstfunction
(defun assoc-equal-lst
  (keys alist)
  "give back the subset of the alist that correspond to these keys. the order
of the entries is same as of the alist"
  (declare (xargs :guard (and (true-listp keys)
        (alistp alist))))
  (if (endp alist)
    nil
    (b* (((cons k &) (car alist)))
      (if (member-equal k keys)
        (cons (car alist)
          (assoc-equal-lst keys (cdr alist)))
        (assoc-equal-lst keys (cdr alist))))))
make-cgen-rule-events/preservationfunction
(defun make-cgen-rule-events/preservation
  (rule kwd-alist
    override-checkp
    verbosep
    ctx
    wrld
    state)
  (b* (((list kind
        out
        fixer-exps
        c1
        constraint) (destructure-preservation-rule rule wrld)) ((unless (equal c1 constraint)) (er soft
          ctx
          "~| ~x0 should be same as ~x1 in a preservation rule.~%"
          c1
          constraint))
      ((unless (and (proper-symbol-listp out)
           (> (len out) 0))) (er soft
          ctx
          "~| ~x0 is not a non-empty list of variable names.~%"
          out))
      ((er constraint-term) (translate constraint
          t
          nil
          t
          ctx
          wrld
          state))
      ((er fixer-terms) (cmp-to-error-triple (translate-cmp-lst fixer-exps
            t
            nil
            t
            ctx
            wrld
            (default-state-vars nil))))
      (mv-expanded-fixer-terms (if (and (eq kind :mv)
            (= 1 (len fixer-terms)))
          (destruct-mv (car fixer-terms)
            (len out)
            wrld)
          fixer-terms))
      (fixer-binding (listlis out mv-expanded-fixer-terms))
      (vars (reverse (all-vars constraint-term)))
      ((unless (and (intersectp-equal out vars))) (er soft
          ctx
          "~| Invariant does not hold: ~x1 should have a common member with ~x0~%"
          vars
          out))
      (rule-metadata (list (cons :out out)
          (cons :constraint-vars vars)
          (cons :constraint-term constraint-term)
          (cons :fixer-terms fixer-terms)
          (cons :fixer-let-binding fixer-binding)))
      (rule-metadata (append kwd-alist rule-metadata))
      (key (cons constraint-term fixer-terms))
      (p-table-alist (table-alist 'preservation-rules-table
          wrld))
      ((when (assoc-equal key p-table-alist)) (er soft
          ctx
          "~| Duplicate entry found in preservation-rules-table: ~x0~%"
          key))
      (table-ev `((table preservation-rules-table
           ',CGEN::KEY
           ',CGEN::RULE-METADATA
           :put)))
      (hyps (union-equal (get1 :hyps rule-metadata)
          (get1 :test-hyps rule-metadata)))
      (vl (if verbosep
          4
          1))
      (relevant-fixer-binding (assoc-equal-lst (intersection-eq out vars)
          fixer-binding))
      (proof-obligation4 `(implies (and ,@(APPEND CGEN::HYPS (LIST CGEN::CONSTRAINT-TERM)))
          (let ,CGEN::RELEVANT-FIXER-BINDING
            ,CGEN::CONSTRAINT-TERM)))
      (invariant4-ev `((test? ,CGEN::PROOF-OBLIGATION4
           :verbosity-level ,CGEN::VL)))
      ((er guard-ob) (body-contracts-obligation (cons ''t fixer-terms)
          :guard-debug verbosep))
      (proof-obligation1 `(implies (and . ,CGEN::HYPS) ,CGEN::GUARD-OB))
      (invariant1-ev `((test? ,CGEN::PROOF-OBLIGATION1
           :verbosity-level ,CGEN::VL))))
    (value (append (and (not override-checkp)
          `((value-triple (cw? t
               "~|Test? obligation: Body contracts of fixer term should be satisfied. ~% ~x0~%"
               ',CGEN::PROOF-OBLIGATION1))))
        (and (not override-checkp) invariant1-ev)
        (and (not override-checkp)
          `((value-triple (cw? t
               "~|Test? Obligation: Preservation rule should be valid under hypotheses. ~x0~%"
               ',CGEN::PROOF-OBLIGATION4))))
        (and (not override-checkp) invariant4-ev)
        table-ev))))
make-cgen-rule-eventsfunction
(defun make-cgen-rule-events
  (rule rule-class
    kwd-alist
    override-checkp
    verbosep
    ctx
    wrld
    state)
  (cond ((eq rule-class :fixer) (make-cgen-rule-events/fixer rule
        kwd-alist
        override-checkp
        verbosep
        ctx
        wrld
        state))
    ((eq rule-class :preservation) (make-cgen-rule-events/preservation rule
        kwd-alist
        override-checkp
        verbosep
        ctx
        wrld
        state))
    (t (er soft
        ctx
        "~| Unindentified rule-class: ~x0~%"
        rule-class))))
cgen-rule-eventsfunction
(defun cgen-rule-events
  (name keys
    verbosep
    wrld
    state)
  (declare (xargs :mode :program))
  (b* ((ctx 'cgen-rule) ((mv kwd-alist rest) (extract-keywords ctx
          *cgen-rule-keywords*
          keys
          nil
          nil))
      ((when rest) (er soft
          ctx
          "~| Unsupported/Extra args: ~x0~%"
          rest))
      (- (cw? verbosep
          "~|Got kwd-alist: ~x0~%"
          kwd-alist))
      (rule (get1 :rule kwd-alist))
      (pre (or (get1 :meta-precondition kwd-alist) 't))
      ((unless (pseudo-termp pre)) (er soft
          ctx
          "~| meta-precondition ~x0 should be a pseudo-termp~%"
          pre))
      (hyp (or (get1 :hyp kwd-alist) 't))
      ((unless (pseudo-termp hyp)) (er soft
          ctx
          "~| hyp ~x0 should be a pseudo-termp~%"
          hyp))
      (hyps (if (and (consp hyp) (eq (car hyp) 'and))
          (cdr hyp)
          (if (equal hyp 't)
            nil
            (list hyp))))
      (test-hyp (or (get1 :test-hyp kwd-alist) 't))
      ((unless (pseudo-termp test-hyp)) (er soft
          ctx
          "~| test-hyp ~x0 should be a pseudo-termp~%"
          test-hyp))
      (test-hyps (if (and (consp test-hyp) (eq (car test-hyp) 'and))
          (cdr test-hyp)
          (if (equal test-hyp 't)
            nil
            (list test-hyp))))
      (rule-class (get1 :rule-classes kwd-alist))
      ((unless (member-eq rule-class *cgen-rule-classes*)) (er soft
          ctx
          "~| rule-class ~x0 should be one of ~x1~%"
          rule-class
          *cgen-rule-classes*))
      ((er events) (make-cgen-rule-events rule
          rule-class
          (list (cons :meta-precondition pre)
            (cons :rule-name name)
            (cons :hyps hyps)
            (cons :test-hyps test-hyps))
          (get1 :override-check kwd-alist)
          verbosep
          ctx
          wrld
          state))
      (program-mode-p (eq :program (default-defun-mode wrld))))
    (value (cons 'progn
        (append (and program-mode-p '((logic)))
          events
          (and program-mode-p '((program)))
          `((value-triple (list :registered ',CGEN::NAME))))))))
fixer-rules-tablefunction
(defun fixer-rules-table
  (wrld)
  (table-alist 'fixer-rules-table wrld))
preservation-rules-tablefunction
(defun preservation-rules-table
  (wrld)
  (table-alist 'preservation-rules-table
    wrld))