Match any
(vl-lex-integer echars breakp warnings) → (mv token? remainder warnings)
We assume here that we have already checked
The
integral_number ::= decimal_number | octal_number | binary_number | hex_number hex_number ::= [size] hex_base hex_value octal_number ::= [size] octal_base octal_value binary_number ::= [size] binary_base binary_value decimal_number ::= unsigned_number | [size] decimal_base decimal_value size ::= non_zero_unsigned_number
Function:
(defun vl-lex-integer (echars breakp warnings) (declare (xargs :guard (and (vl-echarlist-p echars) (booleanp breakp) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-lex-integer)) (declare (ignorable __function__)) (b* ((warnings (vl-warninglist-fix warnings)) (breakp (and breakp t)) ((mv number remainder1) (vl-read-unsigned-number echars)) (normalized-number (vl-echarlist-kill-underscores number)) (value-of-number (vl-echarlist-unsigned-value normalized-number 10)) ((mv ws remainder2) (vl-read-while-whitespace remainder1)) ((mv base remainder2) (vl-read-any-base remainder2)) ((when (and (not number) (not base))) (mv nil echars warnings)) (firstchar (if number (car number) (car base))) ((when (and number (not value-of-number))) (mv (raise "Lexer error (~s0): thought this was impossible; cannot ~ interpret ~s1 as a number." (vl-location-string (vl-echar->loc firstchar)) (vl-echarlist->string number)) echars warnings)) ((unless base) (b* ((val-fix (mod value-of-number (expt 2 32))) (warnings (cond ((< value-of-number (expt 2 31)) warnings) ((< value-of-number (expt 2 32)) (warn :type :vl-warn-overflow :msg "~l0: the plain number ~s1 is in [2^31, ~ 2^32); it will be considered a negative ~ number by 32-bit Verilog implementations, ~ but will be positive on 64-bit systems, so ~ you should add an explicit size." :args (list (vl-echar->loc firstchar) (vl-echarlist->string number)))) (t (warn :type :vl-warn-overflow :msg "~l0: the plain number ~s1 is over 2^32; we ~ truncate it to ~x2 like a 32-bit Verilog ~ implementation. But this number will have a ~ different value on 64-bit systems and ~ beyond, so you should add an explicit size." :args (list (vl-echar->loc firstchar) (vl-echarlist->string number) val-fix))))) (token (make-vl-inttoken :etext number :width 32 :signedp t :value val-fix :bits nil :wasunsized t :breakp breakp))) (mv token remainder1 warnings))) (width-was-0 (eql 0 value-of-number)) (unsizedp (or (not number) width-was-0)) (width (if unsizedp 32 value-of-number)) (chars-of-base (vl-echarlist->chars base)) (signedp (vl-signed-basep chars-of-base)) (radix (vl-base-to-radix chars-of-base)) ((mv ws2 remainder2) (vl-read-while-whitespace remainder2)) ((mv edigits remainder2) (case radix (16 (vl-read-hex-value remainder2)) (10 (vl-read-decimal-value remainder2)) (8 (vl-read-octal-value remainder2)) (otherwise (vl-read-binary-value remainder2)))) (etext (append number ws base ws2 edigits)) (normalized-edigits (vl-echarlist-kill-underscores edigits)) (value (vl-echarlist-unsigned-value normalized-edigits radix)) ((when value) (b* ((val-fix (mod value (expt 2 width))) (token (make-vl-inttoken :etext etext :width width :signedp signedp :value val-fix :bits nil :wasunsized unsizedp :breakp breakp)) (warnings (if width-was-0 (warn :type :vl-0-width-number-literal :msg "~l0: Number ~s1 has explicit width 0, which ~ is not allowed by the SystemVerilog standard. ~ Implementations usually interpret these as ~ unsized (that is, actually 32 bits wide)." :args (list (vl-echar->loc firstchar) (vl-echarlist->string etext))) warnings)) (warnings (cond ((not unsizedp) (if (eql value val-fix) warnings (warn :type :vl-warn-overflow :msg "~l0: the number ~s1 is not within the ~ range [0, 2^~x2) indicated by its size, ~ and is being truncated to ~x2 bits, ~ yielding ~x2'd~x3 (hex: ~x2'h~s4)." :args (list (vl-echar->loc firstchar) (vl-echarlist->string etext) width val-fix (str::nat-to-hex-string val-fix))))) ((< value (expt 2 31)) warnings) ((and signedp (< value (expt 2 32))) (warn :type :vl-warn-overflow :msg "~l0: the unsized, signed number ~s1 is in ~ [2^31, 2^32). It will be considered a ~ negative number by 32-bit Verilog ~ implementations, but positive by 64-bit ~ tools. You should add an explicit size." :args (list (vl-echar->loc firstchar) (vl-echarlist->string number)))) ((< value (expt 2 32)) warnings) (t (warn :type :vl-warn-overflow :msg "~l0: the unsized number ~s1 is over 2^32; ~ we truncate it to 32'd~x2 (hex: 32'h~s3) ~ to emulate a 32-bit Verilog ~ implementation, but it will have a ~ different value on 64-bit tools. You ~ should add an explicit size." :args (list (vl-echar->loc firstchar) (vl-echarlist->string number) val-fix (str::nat-to-hex-string val-fix))))))) (mv token remainder2 warnings))) (digits (vl-echarlist->chars normalized-edigits)) (bits (case radix (16 (vl-hex-digits-to-bitlist digits)) (10 (vl-decimal-digits-to-bitlist digits)) (8 (vl-octal-digits-to-bitlist digits)) (otherwise (vl-binary-digits-to-bitlist digits)))) ((unless bits) (mv (cw "Lexer error (~s0): invalid number: ~s1.~%" (vl-location-string (vl-echar->loc firstchar)) (vl-echarlist->string etext)) echars warnings)) ((mv warnings bits) (vl-correct-bitlist (vl-echar->loc firstchar) bits (and (not width-was-0) value-of-number) etext warnings)) (token (make-vl-inttoken :etext etext :width width :signedp signedp :value value :bits bits :wasunsized unsizedp :breakp breakp))) (mv token remainder2 warnings))))
Theorem:
(defthm vl-warninglist-p-of-vl-lex-integer.warnings (b* (((mv ?token? ?remainder ?warnings) (vl-lex-integer echars breakp warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-token-p-of-vl-lex-integer (implies (and (force (vl-echarlist-p echars)) t) (equal (vl-token-p (mv-nth 0 (vl-lex-integer echars breakp warnings))) (if (mv-nth 0 (vl-lex-integer echars breakp warnings)) t nil))))
Theorem:
(defthm true-listp-of-vl-lex-integer (equal (true-listp (mv-nth 1 (vl-lex-integer echars breakp warnings))) (true-listp echars)) :rule-classes ((:rewrite) (:type-prescription :corollary (implies (true-listp echars) (true-listp (mv-nth 1 (vl-lex-integer echars breakp warnings)))))))
Theorem:
(defthm vl-echarlist-p-of-vl-lex-integer (implies (force (vl-echarlist-p echars)) (equal (vl-echarlist-p (mv-nth 1 (vl-lex-integer echars breakp warnings))) t)))
Theorem:
(defthm append-of-vl-lex-integer (implies (and (mv-nth 0 (vl-lex-integer echars breakp warnings)) (force (vl-echarlist-p echars)) t) (equal (append (vl-token->etext (mv-nth 0 (vl-lex-integer echars breakp warnings))) (mv-nth 1 (vl-lex-integer echars breakp warnings))) echars)))
Theorem:
(defthm no-change-loser-of-vl-lex-integer (implies (not (mv-nth 0 (vl-lex-integer echars breakp warnings))) (equal (mv-nth 1 (vl-lex-integer echars breakp warnings)) echars)))
Theorem:
(defthm acl2-count-of-vl-lex-integer-weak (<= (acl2-count (mv-nth 1 (vl-lex-integer echars breakp warnings))) (acl2-count echars)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm acl2-count-of-vl-lex-integer-strong (implies (and (mv-nth 0 (vl-lex-integer echars breakp warnings)) t) (< (acl2-count (mv-nth 1 (vl-lex-integer echars breakp warnings))) (acl2-count echars))) :rule-classes ((:rewrite) (:linear)))