From 1ccab34cfa59bdcf3d566ad0e838ab5562638801 Mon Sep 17 00:00:00 2001 From: Slava Pestov Date: Sat, 7 Jun 2008 04:19:23 -0500 Subject: [PATCH] Fix inference bug erg found a while ago --- core/inference/backend/backend-docs.factor | 2 +- core/inference/backend/backend.factor | 151 ++++++++++++--------- core/inference/errors/errors.factor | 20 ++- core/inference/inference-docs.factor | 2 +- 4 files changed, 98 insertions(+), 77 deletions(-) diff --git a/core/inference/backend/backend-docs.factor b/core/inference/backend/backend-docs.factor index 91314d1312..ccfa490318 100755 --- a/core/inference/backend/backend-docs.factor +++ b/core/inference/backend/backend-docs.factor @@ -61,7 +61,7 @@ HELP: effect-error { $description "Throws an " { $link effect-error } "." } { $error-description "Thrown when a word's inferred stack effect does not match its declared stack effect." } ; -HELP: recursive-declare-error +HELP: no-recursive-declaration { $error-description "Thrown when inference encounters a recursive call to a word lacking a stack effect declaration. Recursive words must declare a stack effect in order to compile. Due to implementation detail, generic words are recursive, and thus the same restriction applies." } ; HELP: recursive-quotation-error diff --git a/core/inference/backend/backend.factor b/core/inference/backend/backend.factor index 9a0f4c772e..42a1c1dd19 100755 --- a/core/inference/backend/backend.factor +++ b/core/inference/backend/backend.factor @@ -90,8 +90,9 @@ M: object value-literal \ literal-expected inference-warning ; meta-d [ add-inputs ] change d-in [ + ] change ; : current-effect ( -- effect ) - d-in get meta-d get length - terminated? get over set-effect-terminated? ; + d-in get + meta-d get length + terminated? get >>terminated? ; : init-inference ( -- ) terminated? off @@ -115,13 +116,13 @@ M: wrapper apply-object terminated? on #terminate node, ; : infer-quot ( quot rstate -- ) - recursive-state get >r - recursive-state set - [ apply-object terminated? get not ] all? drop - r> recursive-state set ; + recursive-state get [ + recursive-state set + [ apply-object terminated? get not ] all? drop + ] dip recursive-state set ; : infer-quot-recursive ( quot word label -- ) - recursive-state get -rot 2array prefix infer-quot ; + 2array recursive-state get swap prefix infer-quot ; : time-bomb ( error -- ) [ throw ] curry recursive-state get infer-quot ; @@ -136,9 +137,9 @@ TUPLE: recursive-quotation-error quot ; value-literal recursive-quotation-error inference-error ] [ dup value-literal callable? [ - dup value-literal - over value-recursion - rot f 2array prefix infer-quot + [ value-literal ] + [ [ value-recursion ] keep f 2array prefix ] + bi infer-quot ] [ drop bad-call ] if @@ -191,26 +192,26 @@ TUPLE: too-many-r> ; meta-d get push-all ; : if-inline ( word true false -- ) - >r >r dup inline? r> r> if ; inline + [ dup inline? ] 2dip if ; inline : consume/produce ( effect node -- ) - over effect-in over consume-values - over effect-out over produce-values - node, - effect-terminated? [ terminate ] when ; + [ [ in>> ] dip consume-values ] + [ [ out>> ] dip produce-values ] + [ node, terminated?>> [ terminate ] when ] + 2tri ; GENERIC: constructor ( value -- word/f ) GENERIC: infer-uncurry ( value -- ) M: curried infer-uncurry - drop pop-d dup curried-obj push-d curried-quot push-d ; + drop pop-d [ obj>> push-d ] [ quot>> push-d ] bi ; M: curried constructor drop \ curry ; M: composed infer-uncurry - drop pop-d dup composed-quot1 push-d composed-quot2 push-d ; + drop pop-d [ quot1>> push-d ] [ quot2>> push-d ] bi ; M: composed constructor drop \ compose ; @@ -255,13 +256,13 @@ M: object constructor drop f ; DEFER: unify-values : unify-curries ( seq -- value ) - dup [ curried-obj ] map unify-values - swap [ curried-quot ] map unify-values + [ [ obj>> ] map unify-values ] + [ [ quot>> ] map unify-values ] bi ; : unify-composed ( seq -- value ) - dup [ composed-quot1 ] map unify-values - swap [ composed-quot2 ] map unify-values + [ [ quot1>> ] map unify-values ] + [ [ quot2>> ] map unify-values ] bi ; TUPLE: cannot-unify-specials ; @@ -292,7 +293,7 @@ TUPLE: unbalanced-branches-error quots in out ; : unify-inputs ( max-d-in d-in meta-d -- meta-d ) dup [ - [ >r - r> length + ] keep add-inputs nip + [ [ - ] dip length + ] keep add-inputs nip ] [ 2nip ] if ; @@ -318,21 +319,24 @@ TUPLE: unbalanced-branches-error quots in out ; [ swap at ] curry map ; : datastack-effect ( seq -- ) - dup quotation branch-variable - over d-in branch-variable - rot meta-d active-variable - unify-effect meta-d set d-in set ; + [ quotation branch-variable ] + [ d-in branch-variable ] + [ meta-d active-variable ] tri + unify-effect + [ d-in set ] [ meta-d set ] bi* ; : retainstack-effect ( seq -- ) - dup quotation branch-variable - over length 0 - rot meta-r active-variable - unify-effect meta-r set drop ; + [ quotation branch-variable ] + [ length 0 ] + [ meta-r active-variable ] tri + unify-effect + [ drop ] [ meta-r set ] bi* ; : unify-effects ( seq -- ) - dup datastack-effect - dup retainstack-effect - [ terminated? swap at ] all? terminated? set ; + [ datastack-effect ] + [ retainstack-effect ] + [ [ terminated? swap at ] all? terminated? set ] + tri ; : unify-dataflow ( effects -- nodes ) dataflow-graph branch-variable ; @@ -347,14 +351,17 @@ TUPLE: unbalanced-branches-error quots in out ; : infer-branch ( last value -- namespace ) [ copy-inference - dup value-literal quotation set - infer-quot-value + + [ value-literal quotation set ] + [ infer-quot-value ] + bi + terminated? get [ drop ] [ call node, ] if ] H{ } make-assoc ; inline : (infer-branches) ( last branches -- list ) [ infer-branch ] with map - dup unify-effects unify-dataflow ; inline + [ unify-effects ] [ unify-dataflow ] bi ; inline : infer-branches ( last branches node -- ) #! last is a quotation which provides a #return or a #values @@ -390,9 +397,10 @@ TUPLE: effect-error word effect ; : finish-word ( word -- ) current-effect - 2dup check-effect - over recorded get push - "inferred-effect" set-word-prop ; + [ check-effect ] + [ drop recorded get push ] + [ "inferred-effect" set-word-prop ] + 2tri ; : infer-word ( word -- effect ) [ @@ -408,8 +416,7 @@ TUPLE: effect-error word effect ; : custom-infer ( word -- ) #! Customized inference behavior - dup +inlined+ depends-on - "infer" word-prop call ; + [ +inlined+ depends-on ] [ "infer" word-prop call ] bi ; : cached-infer ( word -- ) dup "inferred-effect" word-prop make-call-node ; @@ -422,13 +429,13 @@ TUPLE: effect-error word effect ; [ dup infer-word make-call-node ] } cond ; -TUPLE: recursive-declare-error word ; +TUPLE: no-recursive-declaration word ; : declared-infer ( word -- ) dup stack-effect [ make-call-node ] [ - \ recursive-declare-error inference-error + \ no-recursive-declaration inference-error ] if* ; GENERIC: collect-label-info* ( label node -- ) @@ -463,40 +470,56 @@ M: #return collect-label-info* : inline-block ( word -- #label data ) [ copy-inference nest-node - dup word-def swap + [ word-def ] [ ] bi [ infer-quot-recursive ] 2keep #label unnest-node dup collect-label-info ] H{ } make-assoc ; : join-values ( #label -- ) - calls>> [ node-in-d ] map meta-d get suffix + calls>> [ in-d>> ] map meta-d get suffix unify-lengths unify-stacks meta-d [ length tail* ] change ; : splice-node ( node -- ) - dup node-successor [ - dup node, penultimate-node f over set-node-successor - dup current-node set - ] when drop ; + dup successor>> [ + [ node, ] [ penultimate-node ] bi + f >>successor + current-node set + ] [ drop ] if ; -: apply-infer ( hash -- ) - { meta-d meta-r d-in terminated? } - [ swap [ at ] curry map ] keep - [ set ] 2each ; +: apply-infer ( data -- ) + { meta-d meta-r d-in terminated? } swap extract-keys + namespace swap update ; + +: current-stack-height ( -- n ) + meta-d get length d-in get - ; + +: word-stack-height ( word -- n ) + stack-effect [ in>> length ] [ out>> length ] bi - ; + +: bad-recursive-declaration ( word inferred -- ) + dup 0 < [ 0 ] [ 0 swap ] if effect-error ; + +: check-stack-height ( word height -- ) + over word-stack-height over = + [ 2drop ] [ bad-recursive-declaration ] if ; + +: inline-recursive-word ( word #label -- ) + current-stack-height [ + flatten-meta-d [ join-values inline-block apply-infer ] dip >>in-d + [ node, ] + [ calls>> [ [ flatten-curries ] modify-values ] each ] + [ word>> ] + tri + ] dip + current-stack-height - + check-stack-height ; : inline-word ( word -- ) - dup inline-block over recursive-label? [ - flatten-meta-d >r - drop join-values inline-block apply-infer - r> over set-node-in-d - dup node, - calls>> [ - [ flatten-curries ] modify-values - ] each - ] [ - apply-infer node-child node-successor splice-node drop - ] if ; + dup inline-block over recursive-label? + [ drop inline-recursive-word ] + [ apply-infer node-child successor>> splice-node drop ] if ; M: word apply-object [ diff --git a/core/inference/errors/errors.factor b/core/inference/errors/errors.factor index f565420cac..3c6680bcde 100644 --- a/core/inference/errors/errors.factor +++ b/core/inference/errors/errors.factor @@ -15,10 +15,8 @@ M: inference-error error-help drop f ; M: unbalanced-branches-error error. "Unbalanced branches:" print - dup unbalanced-branches-error-quots - over unbalanced-branches-error-in - rot unbalanced-branches-error-out [ length ] map - 3array flip [ [ bl ] [ pprint ] interleave nl ] each ; + [ quots>> ] [ in>> ] [ out>> [ length ] map ] tri 3array flip + [ [ bl ] [ pprint ] interleave nl ] each ; M: literal-expected summary drop "Literal value expected" ; @@ -32,24 +30,24 @@ M: too-many-r> summary "Quotation pops retain stack elements which it did not push" ; M: no-effect error. - "Unable to infer stack effect of " write no-effect-word . ; + "Unable to infer stack effect of " write word>> . ; -M: recursive-declare-error error. +M: no-recursive-declaration error. "The recursive word " write - recursive-declare-error-word pprint + word>> pprint " must declare a stack effect" print ; M: effect-error error. "Stack effects of the word " write - dup effect-error-word pprint + dup word>> pprint " do not match." print "Declared: " write - dup effect-error-word stack-effect effect>string . - "Inferred: " write effect-error-effect effect>string . ; + dup word>> stack-effect effect>string . + "Inferred: " write effect>> effect>string . ; M: recursive-quotation-error error. "The quotation " write - recursive-quotation-error-quot pprint + quot>> pprint " calls itself." print "Stack effect inference is undecidable when quotation-level recursion is permitted." print ; diff --git a/core/inference/inference-docs.factor b/core/inference/inference-docs.factor index d79c82ed65..acc9329670 100755 --- a/core/inference/inference-docs.factor +++ b/core/inference/inference-docs.factor @@ -89,7 +89,7 @@ ARTICLE: "inference-errors" "Inference errors" { $subsection too-many-r> } { $subsection unbalanced-branches-error } { $subsection effect-error } -{ $subsection recursive-declare-error } ; +{ $subsection no-recursive-declaration } ; ARTICLE: "inference" "Stack effect inference" "The stack effect inference tool is used to check correctness of code before it is run. It is also used by the compiler to build a dataflow graph on which optimizations can be performed. Only words for which a stack effect can be inferred will compile."