(vl-arith-expr-range x ctxsize type ss scopes) → (mv ok min max)
Function:
(defun vl-arith-expr-range (x ctxsize type ss scopes) (declare (xargs :guard (and (vl-expr-p x) (natp ctxsize) (vl-exprsign-p type) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-arith-expr-range)) (declare (ignorable __function__)) (b* ((type (vl-exprsign-fix type))) (vl-expr-case x :vl-literal (vl-value-case x.val :vl-constint (case type (:vl-unsigned (b* ((val (acl2::loghead ctxsize x.val.value))) (mv t val val))) (t (b* ((val (acl2::logext (max (lnfix ctxsize) 1) x.val.value))) (mv t val val)))) :vl-extint (prog2$ (and (eq type :vl-signed) (raise "Expected extints to always be in an unsigned context")) (case x.val.value (:vl-0val (mv t 0 0)) (:vl-1val (b* ((val (acl2::loghead ctxsize -1))) (mv t val val))) (t (mv nil 0 0)))) :otherwise (mv nil 0 0)) :vl-index (b* (((mv ?vttree svex ?indtype) (vl-index-expr-to-svex x ss scopes)) ((unless (sv::svex-case svex :quote (sv::2vec-p svex.val) :otherwise nil)) (vl-expr-arith-range-from-size/type x ss scopes)) (val (sv::2vec->val (sv::svex-quote->val svex)))) (mv t val val)) :vl-unary (b* (((when (eq x.op :vl-unary-plus)) (vl-arith-expr-range x.arg ctxsize type ss scopes)) ((unless (eq x.op :vl-unary-minus)) (vl-expr-arith-range-from-size/type x ss scopes)) ((mv arg-ok arg-min arg-max) (vl-arith-expr-range x.arg ctxsize type ss scopes)) ((unless arg-ok) (mv nil 0 0))) (mv t (- (lifix arg-max)) (- (lifix arg-min)))) :vl-binary (b* (((unless (member x.op '(:vl-binary-plus :vl-binary-minus :vl-binary-times :vl-binary-div))) (vl-expr-arith-range-from-size/type x ss scopes)) ((mv left-ok left-min left-max) (vl-arith-expr-range x.left ctxsize type ss scopes)) ((mv right-ok right-min right-max) (vl-arith-expr-range x.right ctxsize type ss scopes)) ((unless (and left-ok right-ok)) (mv nil 0 0)) (left-min (lifix left-min)) (right-min (lifix right-min)) (left-max (lifix left-max)) (right-max (lifix right-max)) (min (case x.op (:vl-binary-plus (+ left-min right-min)) (:vl-binary-minus (- left-min right-max)) (:vl-binary-times (min (min (* left-min right-min) (* left-min right-max)) (min (* left-max right-min) (* left-max right-max)))) (t (min (min (my-trunc left-min right-min) (my-trunc left-min right-max)) (min (my-trunc left-max right-min) (my-trunc left-max right-max)))))) (max (case x.op (:vl-binary-plus (+ left-max right-max)) (:vl-binary-minus (- left-max right-min)) (:vl-binary-times (max (max (* left-min right-min) (* left-min right-max)) (max (* left-max right-min) (* left-max right-max)))) (t (max (max (my-trunc left-min right-min) (my-trunc left-min right-max)) (max (my-trunc left-max right-min) (my-trunc left-max right-max))))))) (mv t min max)) :otherwise (vl-expr-arith-range-from-size/type x ss scopes)))))
Theorem:
(defthm integerp-of-vl-arith-expr-range.min (b* (((mv ?ok common-lisp::?min common-lisp::?max) (vl-arith-expr-range x ctxsize type ss scopes))) (integerp min)) :rule-classes :type-prescription)
Theorem:
(defthm integerp-of-vl-arith-expr-range.max (b* (((mv ?ok common-lisp::?min common-lisp::?max) (vl-arith-expr-range x ctxsize type ss scopes))) (integerp max)) :rule-classes :type-prescription)