#lang racket

(require "inst.rkt" "memory-rosette.rkt" "queue-rosette.rkt"

"memory-racket.rkt" "queue-racket.rkt" "special.rkt")

(provide (all-defined-out))

(define debug #f)

(struct instclass (opcodes pool args ins outs commute) #:mutable)

(struct argtype (validfunc valid statetype) #:mutable)

(struct statetype (get set min max const structure))

(define machine%

(class object%

(super-new)

(init-field

;; Required fields to be initialized when extending this class.

[bitwidth #f] ;; Number of bits to represent a number

[random-input-bits #f] ;; Number of bits to generate random inputs. Often equal to 'bit'.

[config #f] ;; Machine configuration such as # of regs, memory size, etc.

[opcodes #f] ;; A vector of opcode names.

[nop-id #f] ;; The index of nop in 'opcodes' vector.

[opcode-id-to-class (make-hash)] ;; Map from opcode id to class name

[classes-info (list)] ;; Store classes' info

[argtypes-info (make-hash)] ;; Map from arg type to arg type info

[statetypes-info (make-hash)] ;; Map from state type to state type info

[groups-of-opcodes #f]

[max-number-of-args 0]

[vector2scalar (make-hash)]

;; Fields to be set by method 'analyze-opcode'

[opcode-pool #f] ;; Opcodes to be considered during synthesis.

)

;; Required methods to be implemented.

;; See comments at the point of method declaration in llvm/llvm-machine.rkt for example.

(abstract progstate-structure)

;; Provided default methods. Can be overriden if needed.

(public

;; ISA description

define-instruction-class init-machine-description finalize-machine-description

define-progstate-type define-arg-type

;; Search configuration

window-size

set-config get-config

get-constructor

;; Search helper functions

no-assumption clean-code

get-state clone-state display-state state-eq?

get-opcode-id get-opcode-name

progstate->vector vector->progstate

get-states-from-file parse-state-text

;; For stochastic & enumerative search

update-live update-live-backward

reset-opcode-pool get-valid-opcode-pool update-classes-pool

reset-arg-ranges

analyze-opcode analyze-args

get-arg-ranges get-arg-types get-class-opcodes

has-opcode-id?

;; For enumerative search

get-inst-key

get-progstate-ins-types get-progstate-outs-types

get-progstate-ins-vals get-progstate-outs-vals

get-all-progstate-types get-progstate-type-min-max-const

update-progstate-ins update-progstate-ins-load update-progstate-ins-store

update-progstate-del-mem kill-outs

is-cannonical

)

(define (get-constructor) (raise "Please implement machine:get-constructor"))

;; Non-context-aware window decomposition size. Set it to very high value.

;; Context-aware window decomposition size is set in xxx-symbolic.rkt and xxx-forwardbackward.rkt

(define (window-size) 100)

(define (get-config) config)

(define (set-config info) (set! config info))

;; opcode: opcode name as symbol (not string)

(define (get-opcode-id opcode)

(if (symbol? opcode)

(vector-member opcode opcodes)

(for/vector ([name opcode]

[vec opcodes])

(or (vector-member name vec) -1))))

(define (get-opcode-name id)

(if (number? id)

(vector-ref opcodes id)

(for/vector ([i id]

[vec opcodes])

(if (>= i 0) (vector-ref vec i) '||))))

(define (no-assumption) #f)

(define (display-state x) (pretty-display x))

(define (progstate->vector x) x)

(define (vector->progstate x) x)

(define (parse-state-text str)

(raise "machine:parse-state-text: override this method to read program states from file"))

(define (get-states-from-file file)

(define port (open-input-file file))

(define (parse)

(define line (read-line port))

(if (equal? line eof)

(list)

(cons (parse-state-text line)

(parse))))

(define ret (parse))

(close-input-port port)

ret)

(define (clean-code code [prefix (vector)])

(vector-filter-not (lambda (x)

(if (number? (inst-op x))

(equal? (inst-op x) nop-id)

(equal? (vector-ref (inst-op x) 0) (vector-ref nop-id 0))))

code))

(define (state-eq? state1 state2 pred)

;(pretty-display `(state-eq? ,state1 ,state2 ,pred))

(cond

[(equal? pred #t)

(equal? state1 state2)]

[(equal? pred #f)

#t]

[(number? pred)

(for/and ([i pred]

[s1 state1]

[s2 state2])

(equal? s1 s2))]

[else

(for/and ([i pred]

[s1 state1]

[s2 state2])

(state-eq? s1 s2 i))]))

;; This function can be overriden to update opcode-pool and instclass-pool given code.

(define (analyze-opcode prefix code postfix) (void))

(define (reset-opcode-pool) (void))

(define (get-state init #:concrete [concrete #t])

(define (recursive-init structure init-min init-max init-const)

(define (inner x)

(cond

[(symbol? x) (init #:min init-min #:max init-max #:const init-const)]

[(vector? x) (for/vector ([xi x]) (inner xi))]

[(list? x) (for/list ([xi x]) (inner xi))]

[(pair? x) (cons (inner (car x)) (inner (cdr x)))]

[else (raise "Program state uses unknown data strucutures (beyound vector, list, and pair)")]))

(inner structure))

(define progstate (progstate-structure))

(define (inner x)

(cond

[(equal? x (get-memory-type))

(new (if concrete memory-racket% memory-rosette%) [get-fresh-val init])]

[(equal? x (get-queue-in-type))

(new (if concrete queue-in-racket% queue-in-rosette%) [get-fresh-val init])]

[(equal? x (get-queue-out-type))

(new (if concrete queue-out-racket% queue-out-rosette%) [get-fresh-val init])]

[(symbol? x)

(define info (hash-ref statetypes-info x))

(recursive-init (statetype-structure info)

(statetype-min info)

(statetype-max info)

(statetype-const info))]

[(vector? x) (for/vector ([xi x]) (inner xi))]

[(list? x) (for/list ([xi x]) (inner xi))]

[(pair? x) (cons (inner (car x)) (inner (cdr x)))]

[else (raise "Program state uses unknown data strucutures (beyound vector, list, and pair)")]

))

(inner progstate))

(define (clone-state state)

(define (inner x)

(cond

[(or (number? x) (boolean? x)) x]

[(vector? x) (for/vector ([xi x]) (inner xi))]

[(list? x) (for/list ([xi x]) (inner xi))]

[(pair? x) (cons (inner (car x)) (inner (cdr x)))]

[else x]))

(inner state))

(define (get-valid-opcode-pool index n live-in)

(cond

[live-in

(flatten

(for/list

([class classes-info])

(let ([pass #t])

;; check that all its inputs are live

(for ([in (instclass-ins class)] #:break (not pass))

(unless (number? in)

(let ([info (hash-ref statetypes-info in)])

(unless ((statetype-get info) live-in)

(set! pass #f)))))

(if pass

(instclass-pool class)

(list)))))]

[else opcode-pool]))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; instruction & arg class ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Inform GreenThumb how many opcodes there are in one instruction.

(define (init-machine-description opcode-types)

(set! groups-of-opcodes opcode-types)

(if (= opcode-types 1)

(set! opcodes (list))

(set! opcodes (make-vector opcode-types (list)))))

;; name: name of this class of instructions

;; class-opcodes:

;; if groups-of-opcodes = 1, class-opcodes is a list of opcodes

;; if groups-of-opcodes = n > 1, class-opcodes is a list of <= n sublists of opcodes.

;; where sublist i corresponds to opcodes in group i.

;; (see ARM for an example)

(define (define-instruction-class name class-opcodes

#:scalar [scalar #f] #:vector-width [vector-width #f]

#:args [args '()] #:ins [ins '()] #:outs [outs '()] #:commute [commute #f]

#:required [required (list)])

(unless opcodes

(raise "Call 'init-machine-description' before defining instruction classes"))

;;(pretty-display `(class-opcodes ,class-opcodes))

(for ([arg (flatten args)])

(unless (hash-has-key? argtypes-info arg)

(raise (format "Undefined argument type ~a in 'args'" arg))))

(for ([in (flatten ins)])

(unless (or (number? in) (hash-has-key? statetypes-info in))

(raise (format "Undefined program state type ~a in 'ins'" in))))

(for ([out (flatten outs)])

(unless (or (number? out) (hash-has-key? statetypes-info out))

(raise (format "Undefined program state type ~a in 'outs'" out))))

;; filter out an entry that is not a part of program state (get & set = #f)

(cond

;; if opcodes is a list of lists

[(> groups-of-opcodes 1)

(when scalar

(raise "define-instruction-class does not support defining vector instructions with opcode groups > 1."))

(when (symbol? (car class-opcodes))

(set! class-opcodes (list class-opcodes))

(set! args (list args))

(set! ins (list ins))

(set! required (list #t)))

(when (> (length class-opcodes) groups-of-opcodes)

(raise (format "The number of groups of opcodes provided at define-instruction-class '~a' is more than '~a', which is defined at init-machine-description." (length class-opcodes) groups-of-opcodes)))

(unless (= (length class-opcodes) (length required))

(raise (format "At define-instruction-class '~a', there are ~a groups of opcodes, but only ~a groups are specified with required or optional." name (length class-opcodes) (length required))))

(unless (= (length class-opcodes) (length args))

(raise (format "At define-instruction-class '~a', there are ~a groups of opcodes, but ~a groups of arguments are given." name (length class-opcodes) (length args))))

(unless (= (length class-opcodes) (length ins))

(raise (format "At define-instruction-class '~a', there are ~a groups of opcodes, but ~a groups of inputs are given." name (length class-opcodes) (length ins))))

(define all-args (flatten args))

(set! ins (for/list ([in ins]) (filter-statetype in all-args)))

(set! outs (filter-statetype outs (car args)))

;; collect opcodes

(for ([group class-opcodes]

[id (in-naturals)])

(for ([opcode group])

(unless (member opcode (vector-ref opcodes id))

(vector-set! opcodes id (cons opcode (vector-ref opcodes id))))))

;; insert instruction classes

(for ([group (all-opcodes-groups class-opcodes args ins required)])

(check-max-number-of-args (second group))

(set! classes-info

(cons (instclass (first group) #f

(list->vector (second group))

(third group) outs commute)

classes-info)))

]

[else

(unless (symbol? (car class-opcodes))

(raise (format "The number of groups of opcodes provided at define-instruction-class '~a' is more than '1', which is defined at init-machine-description." (length class-opcodes))))

(check-max-number-of-args args)

(set! ins (filter-statetype ins args))

(set! outs (filter-statetype outs args))

;; collect opcodes

(for ([opcode class-opcodes])

(unless (member opcode opcodes)

(set! opcodes (cons opcode opcodes))))

;; insert instruction class

(set! classes-info

(cons (instclass class-opcodes #f (list->vector args) ins outs commute)

classes-info))

;; map vector opcode to scalar opcode

(when scalar

(unless

(= (length class-opcodes) (length scalar))

(raise "Number of vector opcodes is not equal to number of corresponding scalar opcodes."))

(for ([v class-opcodes]

[s scalar])

(hash-set! vector2scalar v (cons s vector-width))))

])

;;(pretty-display (format "[DEFINE] class=~a | args=~a ins=~a outs=~a" name args ins outs))

)

(define (check-max-number-of-args args)

(when (> (length args) max-number-of-args) (set! max-number-of-args (length args))))

(define (filter-statetype locs args)

(define (pred x)

(if (number? x)

(hash-has-key? statetypes-info

(argtype-statetype (hash-ref argtypes-info (list-ref args x))))

(hash-has-key? statetypes-info x)))

(filter pred locs))

;; Given an instruction class with multiple types of opcodes (both required and optional).

;; Generate all instruction classes with required opcode types.

;; TODO: when ins/outs refer to args using numbers***

(define (all-opcodes-groups opcodes-groups args-groups ins-groups required)

(define ret (list))

;; (define (adjust ins-groups args-groups)

;; (define offset 0)

;; (for/list ([ins ins-groups]

;; [args args-groups])

;; (let ([ret

;; (for/list ([in ins])

;; (if (number? in) ( in offset) in))])

;; (set! offset ( offset (length args)))

;; ret)))

(define (adjust-ins ins offset)

(for/list ([l ins])

(for/list ([i l])

(if (number? i) (- i offset) i))))

(define (recurse opcodes-final args-final ins-final

opcodes-groups args-groups ins-groups required)

(cond

[(empty? opcodes-groups)

(set! ret

(cons

(list (reverse opcodes-final)

(flatten (reverse args-final)) (flatten (reverse ins-final)))

ret))]

[(empty? (car opcodes-groups))

(recurse (cons (list '||) opcodes-final)

(cons (list) args-final)

(cons (list) ins-final)

(cdr opcodes-groups) (cdr args-groups) (cdr ins-groups) (cdr required))]

[else

;; If this opcode type is not required, try excluding it.

(unless (car required)

(recurse (cons (list '||) opcodes-final)

(cons (list) args-final)

(cons (list) ins-final)

(cdr opcodes-groups) (cdr args-groups)

(adjust-ins (cdr ins-groups) (length (car args-groups)))

(cdr required)))

;; Include this opcode type.

(recurse (cons (car opcodes-groups) opcodes-final)

(cons (car args-groups) args-final)

(cons (car ins-groups) ins-final)

(cdr opcodes-groups) (cdr args-groups) (cdr ins-groups) (cdr required))]))

(define extra (- groups-of-opcodes (length opcodes-groups)))

(recurse (list) (list) (list)

(append opcodes-groups (make-list extra (list)))

(append args-groups (make-list extra (list)))

(append ins-groups (make-list extra (list)))

(append required (make-list extra #t)))

ret)

;; Given an instruction class with (one or more) required opcode types.

;; Enumerate all possible combinations, and converting opcode name to opcode id in the process.

(define (all-opcodes-combinations opcodes-groups)

(when debug (pretty-display `(groups ,opcodes-groups)))

(define ret (list))

(define (recurse final work)

(cond

[(empty? work) (set! ret (cons (list->vector final) ret))]

[else

(define remain (cdr work))

(for ([op (car work)]) (recurse (cons op final) remain))]))

(if (list? (car opcodes-groups))

;; multiple opcode types, enumerate.

(begin

(unless (= (length opcodes-groups) groups-of-opcodes)

(raise (format "all-opcodes-combinations: number of generated opcode groups is ~a, not equal to ~a, which is defined at init-machine-description." (length opcodes-groups) groups-of-opcodes)))

(recurse (list)

(reverse

(for/list ([group opcodes-groups]

[ops opcodes])

;; if opcode doens't exist, use -1 (default nop)

(map (lambda (x) (or (vector-member x ops) -1)) group))))

ret)

;; one opcode type, don't have to enumerate.

(map (lambda (x) (vector-member x opcodes)) opcodes-groups)))

(define (define-progstate-type name #:get [get #f] #:set [set #f]

#:min [min #f] #:max [max #f] #:const [const #f]

#:structure [st 'x])

(hash-set! statetypes-info name (statetype get set min max const st)))

(define (define-arg-type name validfunc #:progstate [state name])

(hash-set! argtypes-info name (argtype validfunc #f state)))

(define (finalize-machine-description)

;; set nop-id and convert opcodes into vector format

(cond

[(> groups-of-opcodes 1)

;; (for ([group1 opcodes] [id1 (in-naturals)])

;; (for ([group2 opcodes] [id2 (in-naturals)])

;; (when (< id1 id2)

;; (let ([common (set-intersect (list->set group1) (list->set group2))])

;; (unless (set-empty? common)

;; (raise (format "~a cannot be in both opcode groups ~a and ~a." id1 id2)))))))

(set! opcodes (for/vector ([group opcodes]) (list->vector (reverse group))))

(set! nop-id (vector-member 'nop (vector-ref opcodes 0)))

]

[else

(set! opcodes (list->vector (reverse opcodes)))

(set! nop-id (vector-member 'nop opcodes))])

;; Need to convert opcodes into vector format before this because

;; all-opcodes-combinations requires opcodes to be in vector format.

(set! classes-info (reverse classes-info))

(for ([info classes-info]

[id (in-naturals)])

;; (pretty-display `(class ,(instclass-opcodes info)))

;; (pretty-display `(ins ,(instclass-ins info)))

(let* ([class-opcodes (all-opcodes-combinations (instclass-opcodes info))])

(set-instclass-opcodes! info class-opcodes)

(set-instclass-pool! info class-opcodes)

(for ([ops-vec class-opcodes])

(hash-set! opcode-id-to-class ops-vec id))))

;; convert classes-info into vector format

(set! opcode-pool (flatten (for/list ([info classes-info]) (instclass-pool info))))

(set! classes-info (list->vector classes-info))

(define nop-ops-vec #f)

(when (> groups-of-opcodes 1)

(for ([ops-vec (hash-keys opcode-id-to-class)])

(when (= nop-id (vector-ref ops-vec 0))

(when nop-ops-vec (raise "'nop' cannot be in multiple instruction classes."))

(set! nop-ops-vec ops-vec)))

(set! nop-id nop-ops-vec))

;; convert to id domain

(define new-vector2scalar (make-hash))

(for ([pair (hash->list vector2scalar)])

(hash-set! new-vector2scalar (get-opcode-id (car pair))

(cons

(get-opcode-id (cadr pair))

(cddr pair))))

(set! vector2scalar new-vector2scalar)

(when debug

(pretty-display `(opcodes ,opcodes))

;;(pretty-display `(opcode-id-to-class ,opcode-id-to-class))

(pretty-display `(nop-id ,nop-id)))

;; (for ([info classes-info]

;; [id (in-naturals)])

;; (pretty-display `(class ,id ,(instclass-args info) ,(instclass-ins info))))

)

(define (update-classes-pool)

(for ([class classes-info])

(set-instclass-pool!

class

(filter

(lambda (opcode-id) (member opcode-id opcode-pool))

(instclass-opcodes class)))))

(define (get-class-opcodes opcode-id)

(instclass-pool (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id))))

(define (has-opcode-id? opcode-id)

(hash-has-key? opcode-id-to-class opcode-id))

;; Return types of operands given opcode-name.

(define (get-arg-types opcode-id)

(instclass-args (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id))))

;; Reset valid operands' ranges.

(define (reset-arg-ranges)

(for ([pair (hash->list argtypes-info)])

(let ([name (car pair)]

[argtype-info (cdr pair)])

(when (argtype-validfunc argtype-info)

(set-argtype-valid! argtype-info ((argtype-validfunc argtype-info) config))))))

;; Return valid operands' ranges given opcode-name, live-in, live-out, and mode.

;; Return #f if the given opcode is not a valid instruction given live-in and live-out.

;; opcode-name: symbol

;; live-in & live-out: vector/list/pair format

;; There are 3 modes.

;; 1) `basic (no restriction)

;; 2) `no-args = ignore reigster operands. Return `var-o and `var-i for operand that is input variable and output variable respectively. This mode is only used for enumerative search.

(define (get-arg-ranges opcode-id entry live-in

#:live-out [live-out #f] #:mode [mode `basic])

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define types (instclass-args class))

(define ins (instclass-ins class))

(define outs (instclass-outs class))

;; non-argument inputs have to be live

(define pass #t)

(when live-in

(for ([in ins])

(unless (number? in)

(let ([info (hash-ref statetypes-info in)])

(unless ((statetype-get info) live-in)

(set! pass #f))))))

(and pass

(if (equal? mode `basic)

(for/vector

([type types] [id (in-naturals)])

(cond

[(not pass) (vector)] ;; if not pass, return empty list

[(and (member id ins) (member id outs))

(define vals (get-arg-range-of-type type live-in))

(get-arg-range-of-type type live-out #:vals (vector->list vals))]

[(member id ins) (get-arg-range-of-type type live-in)]

[(member id outs) (get-arg-range-of-type type live-out)]

[else (get-arg-range-of-type type #f)]))

(for/vector

([type types] [id (in-naturals)])

(cond

[(or (member id ins) (member id outs)) type]

[else (get-arg-range-of-type type #f)]))))

)

;; Return valid operands' range given an argument type and liveness.

(define (get-arg-range-of-type type live #:vals [vals #f])

(define argtype-info (hash-ref argtypes-info type))

(unless vals (set! vals (argtype-valid argtype-info)))

;;(pretty-display `(vals ,type ,vals))

(list->vector

(if live

(let ([get (statetype-get (hash-ref statetypes-info

(argtype-statetype (hash-ref argtypes-info type))))])

(filter (lambda (val) (get live val)) vals))

vals))

)

(define (get-all-progstate-types) (hash-keys statetypes-info))

(define (get-progstate-type-min-max-const type)

(define info (hash-ref statetypes-info type))

(values (statetype-min info) (statetype-max info) (statetype-const info)))

;; instruction x: e.g. add v0, v1, v2

;; livenss before execute inst (given live): (vector * #t #t)

;; liveness after execute inst (output): (vector #t #t #t)

;; v0 is live after executing inst, so set the first entry to #t.

(define (update-live live my-inst)

(cond

[live

(define new-live (clone-state live))

(define opcode-id (inst-op my-inst))

(define args (inst-args my-inst))

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define types (instclass-args class))

(define outs (instclass-outs class))

(when args

(for ([type types] [id (in-naturals)] [arg args])

(when (member id outs)

(let ([info (hash-ref statetypes-info

(argtype-statetype (hash-ref argtypes-info type)))])

((statetype-set info) new-live arg #t)))))

(for ([out outs])

(when (hash-has-key? statetypes-info out)

(let ([info (hash-ref statetypes-info out)])

((statetype-set info) new-live #t))))

new-live]

[else live])

)

;; For enumerative search

;; instruction x: e.g. add v0, v1, v2

;; liveness *after* execute inst (given live): (vector #t * *)

;; liveness *before* execute inst (output): (vector #f #t #t).

;; v1 and v2 must be live-in. v0 is not live-in.

(define (update-live-backward live my-inst)

(cond

[live

(define new-live (clone-state live))

(define opcode-id (inst-op my-inst))

(define args (inst-args my-inst))

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define types (instclass-args class))

(define ins (instclass-ins class))

(define outs (instclass-outs class))

(when args

;; kill outs first

(for ([type types] [id (in-naturals)] [arg args])

(when (member id outs)

(let ([info (hash-ref statetypes-info

(argtype-statetype (hash-ref argtypes-info type)))])

((statetype-set info) new-live arg #f)))))

(for ([out outs])

(when (and (not (special-type? out))

(hash-has-key? statetypes-info out))

(let ([info (hash-ref statetypes-info out)])

((statetype-set info) new-live #f))))

(when args

;; add live

(for ([type types] [id (in-naturals)] [arg args])

(when (member id ins)

(let ([info (hash-ref statetypes-info

(argtype-statetype (hash-ref argtypes-info type)))])

((statetype-set info) new-live arg #t)))))

(for ([in ins])

(when (hash-has-key? statetypes-info in)

(let ([info (hash-ref statetypes-info in)])

((statetype-set info) new-live #t))))

new-live]

[else live]))

;; Analyze input code and update operands' ranges.

(define (analyze-args prefix code postfix live-in-list live-out)

(for ([x (vector-append prefix code postfix)])

(analyze-args-inst x))

(when debug

(pretty-display `(analyze-args))

(for ([pair (hash->list argtypes-info)])

(let ([name (car pair)]

[info (cdr pair)])

(pretty-display `(ARG ,name ,(argtype-valid info))))))

)

(define (analyze-args-inst my-inst)

(define opcode-id (inst-op my-inst))

(define args (inst-args my-inst))

(when

args

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define types (instclass-args class))

(for ([type types] [arg args])

(let* ([argtype-info (hash-ref argtypes-info type)]

[vals (argtype-valid argtype-info)])

(unless (member arg vals)

(set-argtype-valid! argtype-info (cons arg vals))))))

)

;; For building behavior-bw

(define (get-inst-key my-inst)

(define opcode-id (inst-op my-inst))

(define args (inst-args my-inst))

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define ins (instclass-ins class))

(define outs (instclass-outs class))

(cons

opcode-id

(filter (lambda (x) x)

(for/list ([arg args] [id (in-naturals)])

(and (not (or (member id ins) (member id outs))) arg)))))

(define (get-progstate-ins-types my-inst)

(define opcode-id (inst-op my-inst))

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define ins (instclass-ins class))

(define types (instclass-args class))

(for/list ([in ins]) (if (number? in) (vector-ref types in) in)))

(define/public (get-progstate-ins-outs opcode-id)

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(values (instclass-ins class) (instclass-outs class)))

(define (get-progstate-outs-types my-inst)

(define opcode-id (inst-op my-inst))

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define outs (instclass-outs class))

(define types (instclass-args class))

(for/list ([out outs]) (if (number? out) (vector-ref types out) out)))

(define-syntax-rule (get-progstate-at state locs types args)

(for/list

([loc locs])

(if (number? loc)

(let ([info (hash-ref statetypes-info

(argtype-statetype (hash-ref argtypes-info (vector-ref types loc))))])

((statetype-get info) state (vector-ref args loc)))

(let ([info (hash-ref statetypes-info loc)])

((statetype-get info) state)))))

(define (get-progstate-ins-vals my-inst state)

(define opcode-id (inst-op my-inst))

(define args (inst-args my-inst))

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define ins (instclass-ins class))

(define types (instclass-args class))

(get-progstate-at state ins types args))

(define (get-progstate-outs-vals my-inst state)

(define opcode-id (inst-op my-inst))

(define args (inst-args my-inst))

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define outs (instclass-outs class))

(define types (instclass-args class))

(get-progstate-at state outs types args))

;; For building inverse behavior table & inverse interpret

;; Update sate if the entry in the state = val or the entry is #f.

(define (update-progstate-ins my-inst vals state)

(define new-state (clone-state state))

(define opcode-id (inst-op my-inst))

(define args (inst-args my-inst))

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define ins (instclass-ins class))

(define types (instclass-args class))

(define pass #t)

(for/list

([in ins] [val vals] #:break (not pass))

(cond

[(number? in)

(define info (hash-ref statetypes-info

(argtype-statetype (hash-ref argtypes-info (vector-ref types in)))))

(define current-val ((statetype-get info) new-state (vector-ref args in)))

(if (or (not current-val) (equal? current-val val))

((statetype-set info) new-state (vector-ref args in) val)

(set! pass #f))]

[else

(define info (hash-ref statetypes-info in))

(define current-val ((statetype-get info) new-state))

(if (or (not current-val) (equal? current-val val))

((statetype-set info) new-state val)

(set! pass #f))]))

(and pass new-state))

(define (update-progstate-del-mem addr new-state)

(let* ([mem-type (hash-ref statetypes-info (get-memory-type))]

[mem ((statetype-get mem-type) new-state)]

[new-mem (send mem clone)]) ;;clone-all

(send new-mem del addr)

((statetype-set mem-type) new-state new-mem)

new-state))

(define (kill-outs my-inst state)

(define new-state (clone-state state))

(define opcode-id (inst-op my-inst))

(define args (inst-args my-inst))

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define outs (instclass-outs class))

(define types (instclass-args class))

(for/list

([out outs])

(cond

[(number? out)

(let ([info (hash-ref statetypes-info

(argtype-statetype (hash-ref argtypes-info (vector-ref types out))))])

((statetype-set info) new-state (vector-ref args out) #f))]

[(special-type? out) (void)]

[else

(let ([info (hash-ref statetypes-info out)])

((statetype-set info) new-state #f))]))

new-state)

(define (update-progstate-ins-load my-inst addr mem state)

(raise "update-progstate-ins-load: unimplemented. Need to extend this function."))

(define (update-progstate-ins-store my-inst addr val state)

(raise "update-progstate-ins-store: unimplemented. Need to extend this function."))

;; Return #t if args of a given opcode is cannonical.

;; args is cannonical if arg-a's ID <= arg-b's ID

;; for arg-a op arg-b, and op is commutative.

;; If op is not commutative, then always return #t.

;; arg: list of arguments' IDs

(define (is-cannonical opcode-id args)

(define class (vector-ref classes-info (hash-ref opcode-id-to-class opcode-id)))

(define commute (instclass-commute class))

(cond

[commute

(define arg-a (list-ref args (car commute)))

(define arg-b (list-ref args (cdr commute)))

(<= arg-a arg-b)]

[else #t]))

))