Fix error where abstract analyzer needed to convert values to boolean…

…s; add non-negative constraint to many types

abi.rkt

@@ -2,7 +2,7 @@
 
 (require (submod "types.rkt" common))
 (require (submod "types.rkt" simulator))
-(require "typed/binaryio.rkt")
+(require (submod "typed.rkt" binaryio))
 
 (provide infer-type
          parse-type)
@@ -23,13 +23,13 @@
     [_ (error "parse-type: Unsupported type:" type)]
     ))
 
-(: type-size (-> AbiType Integer))
+(: type-size (-> AbiType Positive-Integer))
 (define (type-size type)
   (cond ((eq? type "uint256") 32)
         (else (error "type-size: Unsupported type" type))))
 
 (: parse-uint256 (-> Bytes EthWord))
-(define (parse-uint256 bs) (bytes->integer bs #f #t))
+(define (parse-uint256 bs) (bytes->nonnegative bs))
 
 (: parse-array (-> AbiType Bytes Any))
 (define (parse-array type bs)

abstract-analyzer.rkt

@@ -11,7 +11,7 @@
 (require (submod "types.rkt" common))
 (require (submod "types.rkt" abstract-machine))
 (require (submod "types.rkt" evm-assembly))
-(require "typed/binaryio.rkt")
+(require (submod "typed.rkt" binaryio))
 
 (: *m* machine)
 (define *m* (machine 0 ; pc
@@ -23,19 +23,19 @@
                      0 ; stack-size
                      null ; stack
                      #f)) ; halted?
-(: *abstract-symbol-table* (HashTable Symbol Integer))
+(: *abstract-symbol-table* (HashTable Symbol 0..∞))
 (define *abstract-symbol-table* (make-hash))
-(: *evm-symbol-table* (HashTable Symbol Integer))
+(: *evm-symbol-table* (HashTable Symbol 0..∞))
 (define *evm-symbol-table* (make-hash))
 (: *current-instruction* (Parameterof Instruction))
 (define *current-instruction* (make-parameter (assign 'val (const 0))))
 (: *current-evm-instruction* (Parameterof EthInstruction))
 (define *current-evm-instruction* (make-parameter (evm-op 'UNSET)))
 
-(: *evm-pc* (Parameterof Integer))
-(define *evm-pc* (make-parameter -1))
+(: *evm-pc* (Parameterof 0..∞))
+(define *evm-pc* (make-parameter 0))
 
-(: *num-iterations* (Parameterof Integer))
+(: *num-iterations* (Parameterof 0..∞))
 (define *num-iterations* (make-parameter 0))
 
 (module unsafe typed/racket
@@ -151,12 +151,12 @@
     (error "tick-iteration!: Didn't stop after iterations" n))
   (*num-iterations* (+ 1 n)))
 
-(: build-symbol-table (All (A) (-> (Listof (U A label-definition)) (HashTable Symbol Integer))))
+(: build-symbol-table (All (A) (-> (Listof (U A label-definition)) (HashTable Symbol 0..∞))))
 (define (build-symbol-table is)
-  (: ret (HashTable Symbol Integer))
+  (: ret (HashTable Symbol 0..∞))
   (define ret (make-hash))
   (for ([i is]
-        [ id (in-range (length is))])
+        [ id : 0..∞ (in-range (length is))])
     (match i
       [(struct label-definition (name offset virtual?)) (hash-set! ret name id)]
       [_ (void)]))
@@ -176,7 +176,7 @@
     [(struct label-definition (name offset virtual?)) (next)]
     [(struct assign (reg-name e)) (write-reg reg-name (eval-mexpr e)) (next)]
     [(struct test (condition))    (push-stack (eval-mexpr condition)) (next)]
-    [(struct branch (dest))       (if (pop-stack)                     (jump (eval-mexpr dest)) (next))]
+    [(struct branch (dest))       (if (value->bool (pop-stack))       (jump (eval-mexpr dest)) (next))]
     [(struct goto (dest))                                             (jump (eval-mexpr dest))]
     [(struct save (e))            (push-stack (eval-mexpr e))         (next)]
     [(struct restore (reg-name))  (write-reg reg-name (pop-stack))    (next)]
@@ -205,7 +205,7 @@
     ['val        (set-machine-val!        *m* v)]
     ['stack-size (begin
                    (assert v exact-integer?)
-                   (set-machine-stack-size! *m* (cast v Integer))
+                   (set-machine-stack-size! *m* (cast v 0..∞))
                    (let ([ size (length (machine-stack *m*))])
                      (unless (= size v)
                        (error "write-reg: Attempted to write an incorrect stack size" v size))))]
@@ -372,7 +372,7 @@
     ['AND (binop* bitwise-and)]
     ['OR  (binop* bitwise-ior)]
     ['XOR (binop* bitwise-xor)]
-    ['NOT (unop*  bitwise-not)]
+    ['NOT (unop*  (compose truncate-int bitwise-not))]
     ['EXP (binop (λ (a b) (cast (expt a b) Integer)))]
     ['ADD (binop +)]
     ['SUB (binop -)]
@@ -446,7 +446,7 @@
 
 (: eval-op-false? (-> value value))
 (define (eval-op-false? value)
-  (if value #f #t))
+  (if (value->bool value) #f #t))
 
 (: eval-op-singleton (-> value value))
 (define (eval-op-singleton v)
@@ -482,7 +482,7 @@
 (: eval-op-read-memory (-> value value value))
 (define (eval-op-read-memory ptr os)
   (with-asserts ([ ptr exact-integer? ]
-                 [ os exact-integer?    ])
+                 [ os exact-integer?  ])
     (match (get-allocated-fixnum (+ ptr os))
       [#f (let*-values ([(os2 bs) (get-allocation ptr os) ]
                         [(word)   (bytes->integer bs #f #t os2 (+ os2 WORD))])
@@ -491,9 +491,10 @@
 
 (: eval-op-write-memory (-> value value value value))
 (define (eval-op-write-memory ptr os val)
-  (with-asserts ([ ptr exact-integer? ]
-                 [ os  exact-integer? ]
-                 [ val exact-integer? ])
+
+  (with-asserts ([ ptr 0..∞? ]
+                 [ os  0..∞? ]
+                 [ val 0..∞? ])
     (match (get-allocated-fixnum (- ptr WORD))
       [#f (let-values ([(os2 bs) (get-allocation ptr os)])
             ; If (bytes-copy!) triggers an exception, on the EVM this would instead corrupt nearby memory.
@@ -658,3 +659,11 @@
   (assert x v-char?)
   (char->integer (v-char-value x))
   )
+
+(: value->bool (-> value Boolean))
+(define (value->bool x)
+  (match x
+    [0  #f]
+    [#f #f]
+    [x  #t]
+    ))

codegen.rkt

@@ -10,7 +10,7 @@
 (require "globals.rkt")
 (require racket/list)
 
-(require "typed/binaryio.rkt")
+(require (submod "typed.rkt" binaryio))
 
 (provide ;codegen
  ;codegen-list
@@ -192,20 +192,20 @@ These optimizations are currently unimplemented:
 (define-generator (cg-perform i)
   (cg-mexpr (perform-action i))) ; TODO: Watch the number of stack writes here to pop them.
 
-(: reg-address (-> reg Integer))
+(: reg-address (-> reg 0..∞))
 (define (reg-address r)
   (register-address (reg-name r)))
 
-  (: register-address (-> RegisterName Integer))
-  (define (register-address r)
-    (match r
-      ['env        MEM-ENV]
-      ['proc       MEM-PROC]
-      ['continue   MEM-CONTINUE]
-      ['argl       MEM-ARGL]
-      ['val        MEM-VAL]
-      ['stack-size MEM-STACK-SIZE]
-      [x (error "reg-address: Unknown register" x)]))
+(: register-address (-> RegisterName 0..∞))
+(define (register-address r)
+  (match r
+    ['env        MEM-ENV]
+    ['proc       MEM-PROC]
+    ['continue   MEM-CONTINUE]
+    ['argl       MEM-ARGL]
+    ['val        MEM-VAL]
+    ['stack-size MEM-STACK-SIZE]
+    [x (error "reg-address: Unknown register" x)]))
 
 ;;; Primitive operations emitted by the abstract compiler
 

crypto.rkt

@@ -1,6 +1,6 @@
 #lang typed/racket
 
-(require "typed/binaryio.rkt")
+(require (submod "typed.rkt" binaryio))
 
 (provide (all-defined-out))
 
@@ -13,6 +13,6 @@
         (lambda ()
           (system "keccak-256sum"))))))
 
-(: keccak-256-word (-> Bytes Integer))
+(: keccak-256-word (-> Bytes Nonnegative-Integer))
 (define (keccak-256-word bs)
-  (bytes->integer bs #f #t))
+  (bytes->nonnegative bs))

debugger.rkt

@@ -52,7 +52,7 @@
 (: memory-dict (-> vm-exec (Listof (List UnlinkedOffset EthWord))))
 (define (memory-dict vm)
   (for/list : (Listof (List UnlinkedOffset EthWord))
-      ([ i (in-range 0 (vm-exec-largest-accessed-memory vm) 32) ])
+      ([ i : MemoryOffset (in-range 0 (vm-exec-largest-accessed-memory vm) 32) ])
     (list i (read-memory-word vm i 32))))
 
 
@@ -166,7 +166,6 @@
                               addr
                               (λ () 'ERROR))))))
 
-
 (: vm-procedure (-> vm-exec EthWord value))
 (define (vm-procedure vm ptr)
   (vm-label vm (read-memory-word vm (+ ptr WORD) WORD)))
@@ -188,7 +187,7 @@
          [ end  (+ addr len)]
          )
     (v-vector
-     (for/vector : (Vectorof value) ([ i (in-range addr end WORD)])
+     (for/vector : (Vectorof value) ([ i : 0..∞ (in-range addr end WORD)])
        (vm-value vm i)))))
 
 (: vm-environment (-> vm-exec EthWord v-environment))

disassembler.rkt

@@ -1,15 +1,16 @@
 #lang typed/racket
 
+(require (submod "types.rkt" common))
 (require (submod "types.rkt" evm-assembly))
 (require "serializer.rkt")
 (require "utils.rkt")
 (require "globals.rkt")
 
-(require "typed/binaryio.rkt")
-(require "typed/dict.rkt")
+(require (submod "typed.rkt" binaryio))
+(require (submod "typed.rkt" dict))
 (provide (all-defined-out))
 
-(: disassemble-one (-> Bytes Integer EthInstruction))
+(: disassemble-one (-> Bytes 0..∞ EthInstruction))
 (define (disassemble-one bs i)
   (let* ([ byte (cast (bytes-or-zero bs i 1) Byte)])
     (if (hash-has-key? opcodes-by-byte byte)
@@ -22,7 +23,7 @@
         (else          (evm-op (opcode-name op)))
         ))
 
-   
+
 (: disassemble-push (-> Bytes Integer EthInstruction))
 (define (disassemble-push bs i)
   (let ([ op (hash-ref opcodes-by-byte (bytes-ref bs i)) ])
@@ -37,14 +38,14 @@
 (: print-disassembly (-> Bytes Void))
 (define (print-disassembly bs)
   (let ((reverse-symbol-table (invert-hash (*symbol-table*))))
-    (: loop (-> Integer Void))
+    (: loop (-> 0..∞ Void))
     (define (loop n)
       (if (>= n (- (bytes-length bs) 1))
           (void)
           (begin
             (printf "~x" n)
             (write-char #\tab)
-            (display (reverse-symbol-name reverse-symbol-table (- n (*loader-size*))))
+            (display (reverse-symbol-name reverse-symbol-table (assert-0..∞ (- n (*loader-size*)))))
             ;; (print `(,(bytes-ref bs n)
             ;;          ,(push-op? (hash-ref opcodes-by-byte (bytes-ref bs n)))
             ;;          ,(op-extra-size (hash-ref opcodes-by-byte (bytes-ref bs n)))))

globals.rkt

@@ -52,13 +52,13 @@
 (: *exports* (Parameterof (Listof Any)))
 (define *exports* (make-parameter null)) ; Used to generate the standard ABI for the current Pyramid contract
 
-(: *loader-size* (Parameterof Integer))
+(: *loader-size* (Parameterof 0..∞))
 (define *loader-size* (make-parameter 0)) ; Size of the most recently generated loader
 
 (: *byte-offset* (Parameterof UnlinkedOffset))
 (define *byte-offset* (make-parameter 0)) ; Used during serialization to track output stream position
 
-(: *abstract-offset* (Parameterof Integer))
+(: *abstract-offset* (Parameterof 0..∞))
 (define *abstract-offset* (make-parameter 0)) ; Used to generate debug labels. Index of the last-generated abstract machine instruction.
 
 (: *symbol-table* (Parameterof SymbolTable))
@@ -85,28 +85,28 @@
 (: *required-modules* (Parameterof (Setof Any)))
 (define *required-modules* (make-parameter (set)))
 
-(: *addresses-by-name* (Parameterof (HashTable Symbol Address)))
-(define *addresses-by-name* (make-parameter (make-symbol-table)))
+(: *addresses-by-name* (Parameterof AddressTable))
+(define *addresses-by-name* (make-parameter (make-address-table)))
 
-(: *txn-nonce* (Parameterof Integer))
+(: *txn-nonce* (Parameterof 0..∞))
 (define *txn-nonce* (make-parameter 0))
 
-(: *account-nonce* (Parameterof Integer))
+(: *account-nonce* (Parameterof 0..∞))
 (define *account-nonce* (make-parameter 100))
 
 ; TODO: Contract address should use actual Ethereum spec rather than a counter
-(: *contract-create-counter* (Parameterof Integer))
+(: *contract-create-counter* (Parameterof 0..∞))
 (define *contract-create-counter* (make-parameter 200))
 
-(: *label-counter* (Parameterof Integer))
+(: *label-counter* (Parameterof 0..∞))
 (define *label-counter* (make-parameter 0))
 
 (: *primops* (Parameterof PrimopTable))
 (define *primops*
   (let ([ tbl : PrimopTable (make-hash)])
     (make-parameter tbl)))
 
-(: *recursion-depth* (Parameterof Integer))
+(: *recursion-depth* (Parameterof 0..∞))
 (define *recursion-depth* (make-parameter 10))
 
 (: *evm-source-map-stack* (Parameterof (Listof Symbol)))
@@ -120,7 +120,7 @@
 (define *on-simulate-instruction* (make-parameter on-simulate-nop))
 
 ; Constants
-(define assumed-label-size 2) ; TODO: Number of bytes to leave behind for label relocations. This makes it difficult to write programs larger than 65536 bytes.
+(define assumed-label-size 3) ; TODO: Number of bytes to leave behind for label relocations. This makes it difficult to write programs larger than 65536 bytes.
 (define *assumed-label-size* assumed-label-size)
 (define MEMORY-SIZE 200000)
 (define MAX-ITERATIONS 1000000)

io.rkt

@@ -8,8 +8,8 @@
 (require "parser.rkt")
 (require "wallet.rkt")
 
-(require "typed/binaryio.rkt")
-(require "typed/dict.rkt")
+(require (submod "typed.rkt" binaryio))
+(require (submod "typed.rkt" dict))
 
 (provide (all-defined-out)
          (all-from-out 'macros))

macro.rkt

@@ -16,7 +16,7 @@
 (require "compiler.rkt")
 (require racket/match)
 
-(require "typed/binaryio.rkt")
+(require (submod "typed.rkt" binaryio))
 
 (provide (all-defined-out)
          make-label
@@ -151,7 +151,7 @@ Functions defined here are available to Pyramid programs within macros.
 (: make-test-account (-> PyramidQ test-account))
 (define (make-test-account exp)
   (match exp
-    [`((quote ,(? symbol? name)) ,(? exact-integer? balance)) (test-account name balance)]
+    [`((quote ,(? symbol? name)) ,(? exact-nonnegative-integer? balance)) (test-account name balance)]
     [ _ (error "make-test-account: Unknown syntax" exp)]))
 
 (: make-test-deploy (-> PyramidQ test-txn))

parser.rkt

@@ -8,7 +8,7 @@
 (require "utils.rkt")
 (require "globals.rkt")
 
-(require "typed/binaryio.rkt")
+(require (submod "typed.rkt" binaryio))
 
 (require/typed racket/pretty
   [ pretty-print (-> Any Void)])

psl/primitives.pmd

@@ -147,6 +147,12 @@
        (restore 'val)
        ))
 
+(defmacro (%#-bool->word x)
+  `(begin ,x
+          (asm (save (op 'bool->unboxed (reg 'val)))
+               (restore 'val))
+          ))
+
 (defmacro (%-bool->fixnum a)
   `(begin
      ,a
@@ -221,7 +227,7 @@
   (loop (%-unbox 0)))
 
 (define (%#-bytes->words x)
-  (%#-/ x (%-unbox WORD)))
+  (%#-u/ x (%-unbox WORD)))
 
 (define (%-unbox a)
   (cond [(%-fixnum?    a) (%-unbox-fixnum    a)]