steve
/
factor
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fixing soundness issues with recursive combinators

db4
Slava Pestov 2008-08-15 04:09:23 -05:00
parent 10b75276ff
commit 32b762f5ec
7 changed files with 95 additions and 67 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
basis/compiler/tree/normalization/normalization-tests.factor
View File

@ -3,8 +3,6 @@ USING: compiler.tree.builder compiler.tree.normalization
compiler.tree sequences accessors tools.test kernel math ;
\ count-introductions must-infer
\ fixup-enter-recursive must-infer
\ eliminate-introductions must-infer
\ normalize must-infer
[ 3 ] [ [ 3drop 1 2 3 ] build-tree count-introductions ] unit-test
@ -27,3 +25,19 @@ compiler.tree sequences accessors tools.test kernel math ;
] unit-test
[ ] [ [ [ 1 ] [ 2 ] if + * ] build-tree normalize drop ] unit-test
DEFER: bbb
: aaa ( x -- ) dup [ dup >r bbb r> aaa ] [ drop ] if ; inline recursive
: bbb ( x -- ) >r drop 0 r> aaa ; inline recursive
[ ] [ [ bbb ] build-tree normalize drop ] unit-test
: ccc ( -- ) ccc drop 1 ; inline recursive
[ ] [ [ ccc ] build-tree normalize drop ] unit-test
DEFER: eee
: ddd ( -- ) eee ; inline recursive
: eee ( -- ) swap ddd ; inline recursive
[ ] [ [ eee ] build-tree normalize drop ] unit-test

83
basis/compiler/tree/normalization/normalization.factor
View File

@ -1,6 +1,7 @@
! Copyright (C) 2008 Slava Pestov.
! See http://factorcode.org/license.txt for BSD license.
USING: fry namespaces sequences math accessors kernel arrays
combinators sequences.deep assocs
stack-checker.backend
stack-checker.branches
stack-checker.inlining
@ -54,7 +55,8 @@ M: #branch count-introductions*
M: #recursive count-introductions*
[ label>> ] [ child>> count-introductions ] bi
>>introductions drop ;
>>introductions
drop ;
M: node count-introductions* drop ;
@ -72,34 +74,32 @@ M: #recursive collect-label-info
M: node collect-label-info drop ;
! Eliminate introductions
! Normalize
GENERIC: normalize* ( node -- node' )
SYMBOL: introduction-stack
: fixup-enter-recursive ( introductions recursive -- )
[ child>> first ] [ in-d>> ] bi >>in-d
[ append ] change-out-d
drop ;
GENERIC: eliminate-introductions* ( node -- node' )
: pop-introduction ( -- value )
introduction-stack [ unclip-last swap ] change ;
: pop-introductions ( n -- values )
introduction-stack [ swap cut* swap ] change ;
M: #introduce eliminate-introductions*
M: #introduce normalize*
out-d>> [ length pop-introductions ] keep #copy ;
SYMBOL: remaining-introductions
M: #branch eliminate-introductions*
dup children>> [
M: #branch normalize*
[
[
[ eliminate-introductions* ] change-each
introduction-stack get
] with-scope
] map
[
[ normalize* ] map flatten
introduction-stack get
2array
] with-scope
] map unzip swap
] change-children swap
[ remaining-introductions set ]
[ [ length ] map infimum introduction-stack [ swap head ] change ]
bi ;
@ -112,51 +112,52 @@ M: #branch eliminate-introductions*
] if
] 3map ;
M: #phi eliminate-introductions*
M: #phi normalize*
remaining-introductions get swap dup terminated>>
'[ , eliminate-phi-introductions ] change-phi-in-d ;
M: node eliminate-introductions* ;
: eliminate-introductions ( nodes introductions -- nodes )
: (normalize) ( nodes introductions -- nodes )
introduction-stack [
[ eliminate-introductions* ] map
[ normalize* ] map flatten
] with-variable ;
: eliminate-toplevel-introductions ( nodes -- nodes' )
dup count-introductions make-values
[ eliminate-introductions ] [ nip #introduce ] 2bi
prefix ;
: eliminate-recursive-introductions ( recursive n -- )
make-values
[ swap fixup-enter-recursive ]
[ '[ , eliminate-introductions ] change-child drop ]
M: #recursive normalize*
dup label>> introductions>>
[ drop [ child>> first ] [ in-d>> ] bi >>in-d drop ]
[ make-values '[ , (normalize) ] change-child ]
2bi ;
! Normalize
GENERIC: normalize* ( node -- node' )
M: #recursive normalize*
dup dup label>> introductions>>
eliminate-recursive-introductions ;
M: #enter-recursive normalize*
[ introduction-stack get prepend ] change-out-d
dup [ label>> ] keep >>enter-recursive drop
dup [ label>> ] [ out-d>> ] bi >>enter-out drop ;
: unchanged-underneath ( #call-recursive -- n )
[ out-d>> length ] [ label>> return>> in-d>> length ] bi - ;
M: #call-recursive normalize*
dup unchanged-underneath
: call<return ( #call-recursive n -- nodes )
neg dup make-values [
[ pop-introductions '[ , prepend ] change-in-d ]
[ '[ , prepend ] change-out-d ]
bi*
] [ introduction-stack [ prepend ] change ] bi ;
: call>return ( #call-recursive n -- nodes )
[ [ [ in-d>> ] [ out-d>> ] bi ] [ '[ , head ] ] bi* bi@ #copy ]
[ '[ , tail ] [ change-in-d ] [ change-out-d ] bi ]
2bi 2array ;
M: #call-recursive normalize*
dup unchanged-underneath {
{ [ dup 0 < ] [ call<return ] }
{ [ dup 0 = ] [ drop ] }
{ [ dup 0 > ] [ call>return ] }
} cond ;
M: node normalize* ;
: normalize ( nodes -- nodes' )
dup [ collect-label-info ] each-node
eliminate-toplevel-introductions
[ normalize* ] map-nodes ;
dup count-introductions make-values
[ (normalize) ] [ nip #introduce ] 2bi
prefix ;

7
basis/compiler/tree/tree.factor
View File

@ -112,14 +112,13 @@ TUPLE: #return < node in-d ;
\ #return new
swap >>in-d ;
TUPLE: #recursive < node in-d word label loop? returns calls child ;
TUPLE: #recursive < node in-d word label loop? child ;
: #recursive ( word label inputs child -- node )
: #recursive ( label inputs child -- node )
\ #recursive new
swap >>child
swap >>in-d
swap >>label
swap >>word ;
swap >>label ;
TUPLE: #enter-recursive < node in-d out-d label ;

42
basis/stack-checker/inlining/inlining.factor
View File

@ -39,14 +39,19 @@ M: inline-recursive hashcode* id>> hashcode* ;
dup pair? [ second effect? ] [ drop f ] if ;
: make-copies ( values effect-in -- values' )
[ quotation-param? [ copy-value ] [ drop <value> ] if ] 2map ;
[ length cut* ] keep
[ quotation-param? [ copy-value ] [ drop <value> ] if ] 2map
append ;
SYMBOL: enter-in
SYMBOL: enter-out
: prepare-stack ( word -- )
required-stack-effect in>> [ length ensure-d ] keep
[ drop enter-in set ] [ make-copies enter-out set ] 2bi ;
required-stack-effect in>>
[ length ensure-d drop ] [
meta-d get clone enter-in set
meta-d get swap make-copies enter-out set
] bi ;
: emit-enter-recursive ( label -- )
enter-out get >>enter-out
@ -74,7 +79,7 @@ SYMBOL: enter-out
: recursive-word-inputs ( label -- n )
entry-stack-height d-in get + ;
: (inline-recursive-word) ( word -- word label in out visitor )
: (inline-recursive-word) ( word -- label in out visitor )
dup prepare-stack
[
init-inference
@ -83,7 +88,7 @@ SYMBOL: enter-out
dup <inline-recursive>
[ dup emit-enter-recursive (inline-word) ]
[ end-recursive-word ]
[ ]
[ nip ]
2tri
check->r
@ -97,21 +102,26 @@ SYMBOL: enter-out
(inline-recursive-word)
[ consume-d ] [ output-d ] [ ] tri* #recursive, ;
: check-call-height ( word label -- )
entry-stack-height current-stack-height >
[ diverging-recursion-error inference-error ] [ drop ] if ;
: check-call-height ( label -- )
dup entry-stack-height current-stack-height >
[ word>> diverging-recursion-error inference-error ] [ drop ] if ;
: trim-stack ( label seq -- stack )
swap word>> required-stack-effect in>> length tail* ;
: call-site-stack ( label -- stack )
required-stack-effect in>> length meta-d get swap tail* ;
meta-d get trim-stack ;
: check-call-site-stack ( stack label -- )
tuck enter-out>>
: trimmed-enter-out ( label -- stack )
dup enter-out>> trim-stack ;
: check-call-site-stack ( label -- )
[ ] [ call-site-stack ] [ trimmed-enter-out ] tri
[ dup known [ [ known ] bi@ = ] [ 2drop t ] if ] 2all?
[ drop ] [ word>> inconsistent-recursive-call-error inference-error ] if ;
: add-call ( word label -- )
[ check-call-height ]
[ [ call-site-stack ] dip check-call-site-stack ] 2bi ;
: check-call ( label -- )
[ check-call-height ] [ check-call-site-stack ] bi ;
: adjust-stack-effect ( effect -- effect' )
[ in>> ] [ out>> ] bi
@ -122,9 +132,7 @@ SYMBOL: enter-out
: call-recursive-inline-word ( word -- )
dup "recursive" word-prop [
[ required-stack-effect adjust-stack-effect ] [ ] [ recursive-label ] tri
[ add-call drop ]
[ nip '[ , #call-recursive, ] consume/produce ]
3bi
[ 2nip check-call ] [ nip '[ , #call-recursive, ] consume/produce ] 3bi
] [ undeclared-recursion-error inference-error ] if ;
: inline-word ( word -- )

8
basis/stack-checker/stack-checker-tests.factor
View File

@ -568,4 +568,10 @@ M: object inference-invalidation-d inference-invalidation-c 2drop ;
dup 10 < [ 2drop 5 1 + unbalanced-retain-usage ] [ 2drop ] if ;
inline recursive
[ unbalanced-retain-usage ] [ inference-error? ] must-fail-with
[ [ unbalanced-retain-usage ] infer ] [ inference-error? ] must-fail-with
DEFER: eee'
: ddd' ( ? -- ) [ f eee' ] when ; inline recursive
: eee' ( ? -- ) >r swap [ ] r> ddd' call ; inline recursive
[ [ eee' ] infer ] [ inference-error? ] must-fail-with

2
basis/stack-checker/visitor/dummy/dummy.factor
View File

@ -19,7 +19,7 @@ M: f #if, 3drop ;
M: f #dispatch, 2drop ;
M: f #phi, drop drop drop drop drop ;
M: f #declare, drop ;
M: f #recursive, 2drop 2drop ;
M: f #recursive, 3drop ;
M: f #copy, 2drop ;
M: f #drop, drop ;
M: f #alien-invoke, drop ;

2
basis/stack-checker/visitor/visitor.factor
View File

@ -25,7 +25,7 @@ HOOK: #declare, stack-visitor ( declaration -- )
HOOK: #return, stack-visitor ( stack -- )
HOOK: #enter-recursive, stack-visitor ( label inputs outputs -- )
HOOK: #return-recursive, stack-visitor ( label inputs outputs -- )
HOOK: #recursive, stack-visitor ( word label inputs visitor -- )
HOOK: #recursive, stack-visitor ( label inputs visitor -- )
HOOK: #copy, stack-visitor ( inputs outputs -- )
HOOK: #alien-invoke, stack-visitor ( params -- )
HOOK: #alien-indirect, stack-visitor ( params -- )