tclbdd

Check-in [6e68626558]
Login

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Program flow analysis - reaching definitions example
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:6e68626558d806abf2f72bf14e7c89fcba305dfb
User & Date: kbk 2013-12-20 20:00:09
Context
2013-12-20
21:36
fix a bug in Quantify where things fall over trying to quantify an unused variable check-in: 179080d4b1 user: kbk tags: trunk
20:00
Program flow analysis - reaching definitions example check-in: 6e68626558 user: kbk tags: trunk
2013-12-19
17:19
Added proof-of-concept relational algebra methods. Still in need of some serious love, that is, commenting and thorough testing. check-in: 07b1771e35 user: kbk tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Added examples/loadProgram.tcl.





































































































































































































































>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
# loads a program into an FDDD database

# Program for simple examples of flow analysis

package require tclbdd::fddd

# Find the size of the database, and find labels in the program
#
# Returns: A list of variable names used in the program, and a list of
#          labels and their locations in the list of instructions.

proc pass1 {program} {
    set vars {}
    set labels {}
    set i 0
    set vn 0
    foreach insn $program {
	if {[regexp {^(_[[:alnum:]_]+):$} [lindex $insn 0] -> label]} {
	    dict set labels $label $i
	    set insn [lrange $insn[set insn {}] 1 end]
	}
	foreach token $insn {
	    if {[regexp {^[[:alpha:]][[:alnum:]_]*$} $token]} {
		if {![dict exists $vars $token]} {
		    dict set vars $token $vn
		    incr vn
		}
	    }
	}
	incr i
    }
    return [list $vars $labels]
}

# finds the number of bits needed to represent a finite domain

proc fdbits {numvals} {
    set bits 1
    set bound 2
    while {$bound < $numvals} {
	incr bits
	incr bound $bound
    }
    return $bits
}

# Calculates 'reads', 'writes' and 'seq'

proc pass2 {program vars labels} {
    set i 0
    foreach insn $program {
	if {[regexp {^(_[[:alnum:]_]+):$} [lindex $insn 0] label]} {
	    set insn [lrange $insn[set insn {}] 1 end]
	}
	if {[lindex $insn 1] eq {:=}} {
	    lappend writes $i [dict get $vars [lindex $insn 0]]
	    set insn [lrange $insn[set insn {}] 2 end]
	}
	foreach token $insn {
	    if {[regexp {^[[:alpha:]][[:alnum:]_]*$} $token]} {
		lappend reads $i [dict get $vars $token]
	    }
	}
	if {[lindex $insn 0] eq {*GOTO}} {
	    lappend seq $i [dict get $labels [lindex $insn 1]]
	} elseif {[lindex $insn 0] eq {*IF} && [lindex $insn 2] eq {*GOTO}} {
	    lappend seq $i [dict get $labels [lindex $insn 3]] $i [expr {$i+1}]
	} else {
	    lappend seq $i [expr {$i+1}]
	}
	incr i
    }
    return [list $reads $writes $seq]
}
    
proc analyzeProgram {program db} {
    # pass 1 - find variables, resolve labels, calculate domain sizes
    lassign [pass1 $program] vars labels
    puts [list variables: {*}$vars]
    puts [list labels: {*}$labels]
    set stbits [fdbits [llength $program]]
    set vbits [fdbits [dict size $vars]]
    puts "statements need $stbits bits, vars need $vbits bits"

    # Create the program database
    
    bdd::fddd::database create $db \
	[bdd::fddd::concatenate \
	     [bdd::fddd::domain v $vbits bigendian] \
	     [bdd::fddd::interleave \
		  [bdd::fddd::domain st  $stbits littleendian] \
		  [bdd::fddd::domain st2 $stbits littleendian] \
		  [bdd::fddd::domain st3 $stbits littleendian]]]
    
    $db relation reads st v
    $db relation writes st v
    $db relation seq st st2

    # pass 2 - discover 'reads', 'writes', 'seq' relations
    lassign [pass2 $program $vars $labels] reads writes seq
    puts "reads: $reads"
    puts "writes: $writes"
    puts "seq: $seq"

    # TODO - Load incrementally in pass 2
    
    $db load reads $reads
    $db load writes $writes
    $db load seq $seq

    # Return the variable dictionary, since it is not readily recoverable

    return $vars
}

Added examples/program1.tcl.













































































>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
source [file join [file dirname [info script]] loadProgram.tcl]

# sample program is (more or less)
#
# proc cosine {x n} {
#     set j 0
#     set s 1.0
#     set t 1.0
#     set i 0
#     while {[incr i] < $n} {
#         set t [expr {-$t * $x * $x / [incr j] / [incr j]}]
#         set s [expr  {$s + $t}]
#     }
#     return s
# }

set program [split [string trim {
    *ENTRY
    x := *PARAMETER 0
    n := *PARAMETER 1
    j := 0
    s := 1.0
    t := 1.0
    i := 0
    *GOTO _entry 
_loop: a := - t
    a := a * x
    a := a * x
    j := j + 1
    a := a / j
    j := j + 1
    t := a / j
    s := s + t
_entry: i := i + 1
    a := i < n
    *IF a *GOTO _loop
    *RETURN s
}] "\n"]

Added examples/reach.tcl.













































































































































































































































































































>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
source [file join [file dirname [info script]] loadProgram.tcl]

proc profile! {db var} {
    puts "$var: [$db profile $var]"
}
interp alias {} profile {} profile!

source [file join [file dirname [info script]] program1.tcl]

set vars [analyzeProgram $program db]

puts "profiles:"
puts "reads:  [db profile reads]"
puts "writes: [db profile writes]"
puts "seq:    [db profile seq]"

#############################################################################

# PROPOSED OBJECT CODE OF A DATALOG PROGRAM

# flowspast(v,st,st2) means: Control may pass from the end of
# instruction 'st1' to the start of instruction 'st2' without
# assigning to the variable 'v'.  Note how the induction case
# recurses twice into 'flowspast' rather than using 'seq'. This
# means that the path length of the 'flowpast' relation can
# roughly double on each pass, meaning that the number of passes
# in the iteration-to-convergence is only logarithmic in the
# length of the longest loop in the program.

# reach(v,st,st2) means: "The use of variable v at instruction st2
# might see the assignment to variable v at instruction st1"

# Reachability: relation definitions that might be generated by a Datalog
# compiler.

db relation t10 v;		# The universal set of variables
db relation t11 v st3;	# writes(v, st3)
db relation t12 v st st3;	# flowspast(v, st, st3)
db relation t13 v st st3;	# flowspast(v, st, st3),!writes(st3,v)
db relation t14 v st2 st3;	# flowspast(v, st3, st2)
db relation t15 v st st2 st3;	# flowspast(v, st, st3),
				# !writes(st3,v),
				# flowspast(v, st3, st2)
db relation t16 v st st2;	# project{v,st,st2}(t15)
db relation t17 v st st2;	# writes(st,v),flowspast(v,st,st2)
db relation t18 v st2;		# reads(st2,v)

db relation flowspast v st st2
db relation flowspast' v st st2
db relation reaches v st st2

# Reachability: code that might be generated by a Datalog compiler

proc reachability {db} [subst {

    ### input: reads(st,v)
    ### input: writes(st,v)
    ### input: seq(st,st2)
    ### output: flowspast(v,st,st2)
    ### output: reaches(v,st,st2)

    ### flowspast(v,st,st2) :- seq(st,st2)
    
    [db set t10 _]
    [db join flowspast seq t10]; 		profile \$db flowspast

    ### flowspast(v,st,st2) :- flowspast(v,st,st3),
    ###                        !writes(st3,v),
    ###                        flowspast(v,st3,st2)

    [db replace t11 writes st3 st]; # invariant code hoisted out of loop
    [db set flowspast' {}]
    while {!\[\$db === flowspast flowspast'\]} {
	[db set flowspast' flowspast]
	[db replace t12 flowspast st3 st2];	profile \$db t12
	[db antijoin t13 t12 t11]; 		profile \$db t13
	[db replace t14 flowspast st3 st];	profile \$db t14
	[db join t15 t13 t14];			profile \$db t15
	[db project t16 t15];			profile \$db t16
	[db union flowspast flowspast' t16];	profile \$db flowspast
    }

    ### reaches(v,st,st2) :- writes(st,v),
    ###                      flowspast(v,st,st2),
    ###                      reads(st2,v)

    [db join t17 writes flowspast]; 		profile \$db t17
    [db replace t18 reads st2 st]; 		profile \$db t18
    [db join reaches t17 t18];			profile \$db reaches

}]

#############################################################################

# DATALOG QUERY: reaches(_,_,i)?

db relation q1 st2
db relation q1result v st st2 
proc query1 {db i} [subst {
    [db set q1 {}]
    \$db load q1 \[list \$i\]
    [db join q1result reaches q1]
}]

#############################################################################

# DATALOG QUERY: reaches(_,i,_)?

db relation q2 st
db relation q2result v st st2 
proc query2 {db i} [subst {
    [db set q2 {}]
    \$db load q2 \[list \$i\]
    [db join q2result reaches q2]
}]

#############################################################################

# Report on reachability analysis

reachability db
puts [format {%-16s %2s  %-32s %-16s} PRODUCERS {} INSTRUCTIONS CONSUMERS]
set i 0
foreach stmt $program {

    query1 db $i
    set flowsto {}
    db enumerate result q1result {
	lappend flowsto \
	    [lindex $vars [expr {2*[dict get $result v]}]] \
	    [dict get $result st]
    }

    query2 db $i
    set flowsfrom {}
    db enumerate result q2result {
	lappend flowsfrom \
	    [lindex $vars [expr {2*[dict get $result v]}]] \
	    [dict get $result st2]
    }
    puts [format "%-16s %2d: %-32s %-16s" \
	      [lsort -stride 2 -index 0 -ascii \
		   [lsort -stride 2 -index 1 -integer $flowsto]] \
	      $i \
	      $stmt \
	      [lsort -stride 2 -index 0 -ascii \
		   [lsort -stride 2 -index 1 -integer $flowsfrom]]]

    incr i
}

Changes to library/tclbdd.tcl.

193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
    set coro [coroutine [namespace current]::_fullsat::[incr _seq] \
		  [namespace which ExpandedSatLauncher] $varlist $satterm]
    try {
	while {[llength [set var [$coro]]] != 0} {
	    try {
		uplevel 1 $script
	    } on error {message options} {
		dict incr $options -level 1
		return -options $options $message
	    } on return {retval options} {
		dict incr $options -level 1
		return -options $options $retval
	    } on break {} {
		break
	    } on continue {} {
		continue
	    } on 6 {} {
		return -code break







|


|







193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
    set coro [coroutine [namespace current]::_fullsat::[incr _seq] \
		  [namespace which ExpandedSatLauncher] $varlist $satterm]
    try {
	while {[llength [set var [$coro]]] != 0} {
	    try {
		uplevel 1 $script
	    } on error {message options} {
		dict incr options -level 1
		return -options $options $message
	    } on return {retval options} {
		dict incr options -level 1
		return -options $options $retval
	    } on break {} {
		break
	    } on continue {} {
		continue
	    } on 6 {} {
		return -code break

Changes to library/tclfddd.tcl.

304
305
306
307
308
309
310



















311
312
313
314
315
316
317
318
...
323
324
325
326
327
328
329

330
331
332
333
334
335
336
...
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
...
359
360
361
362
363
364
365




























366
367
368
369
370
371
372
...
560
561
562
563
564
565
566


567
568
569
570
571
572
573
	return $retval
    }

    method columns {} {
	return [dict keys $m_columns]
    }




















    method difference {dest source1 source2} {
	# TODO typecheck
	return [list [namespace which sys] > $dest $source1 $source2]
    }

    # TODO - How can this be streamlined?

    method enumerate {dictvar relation script} {
................................................................................
		"relation \"$relation\" is not defined in this database"
	}
	sys foreach_sat satterm $relation {
	    #puts "expand a term of $relation with variables [my Varlist $relation]"
	    bdd::foreach_fullsat vars [my Varlist $relation] $satterm {
		#puts "and values $vars"
		set i 0

		foreach column [dict get $m_relcolumns $relation] {
		    set varsForColumn [dict get $m_columns $column]
		    set value 0
		    for {set j 0} {$j < [llength $varsForColumn]} {incr j} {
			set value [expr {$value | ([lindex $vars $i] << $j)}]
			incr i
		    }
................................................................................
		}
		try {
		    uplevel 1 $script
		} on error {message options} {
		    dict incr options -level 1
		    return -options $options $message
		} on return {retval options} {
		    dict incr $options -level 1
		    return -options $options $message
		} on break {} {
		    return -level 0 -code 6
		} on continue {} {
		    continue
		}
	    }
................................................................................
	dict unset m_relcolumns $name
	return
    }

    method gc {} {
	return [sys gc]
    }





























    method join {dest source1 source2} {
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
................................................................................
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
	if {$source eq {}} {
	    set source 0


	} else {
	    if {![dict exists $m_relcolumns $source]} {
		return -code error \
		    -errorcode [list FDDD RelationNotDefined $source] \
		    "relation \"$source\" is not defined in this database"
	    }
	    if {[dict get $m_relcolumns $dest]







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
|







 







>







 







|







 







>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>







 







>
>







304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
...
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
...
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
...
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
...
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
	return $retval
    }

    method columns {} {
	return [dict keys $m_columns]
    }

    method set {dest source} {
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
	if {![dict exists $m_relcolumns $source]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $source] \
		"relation \"$source\" is not defined in this database"
	}
	if {[dict get $m_relcolumns $dest]
	    ne [dict get $m_relcolumns $source]} {
	    return -code error \
		-errorcode [list FDDD WrongColumns $dest $source] \
		"relations \"$dest\" and \"$source\" have different columns"
	}
	return [list [namespace which sys] negate $dest $source]
    }
    method antijoin {dest source1 source2} {
	# TODO typecheck
	return [list [namespace which sys] > $dest $source1 $source2]
    }

    # TODO - How can this be streamlined?

    method enumerate {dictvar relation script} {
................................................................................
		"relation \"$relation\" is not defined in this database"
	}
	sys foreach_sat satterm $relation {
	    #puts "expand a term of $relation with variables [my Varlist $relation]"
	    bdd::foreach_fullsat vars [my Varlist $relation] $satterm {
		#puts "and values $vars"
		set i 0
		set valdict {}
		foreach column [dict get $m_relcolumns $relation] {
		    set varsForColumn [dict get $m_columns $column]
		    set value 0
		    for {set j 0} {$j < [llength $varsForColumn]} {incr j} {
			set value [expr {$value | ([lindex $vars $i] << $j)}]
			incr i
		    }
................................................................................
		}
		try {
		    uplevel 1 $script
		} on error {message options} {
		    dict incr options -level 1
		    return -options $options $message
		} on return {retval options} {
		    dict incr options -level 1
		    return -options $options $message
		} on break {} {
		    return -level 0 -code 6
		} on continue {} {
		    continue
		}
	    }
................................................................................
	dict unset m_relcolumns $name
	return
    }

    method gc {} {
	return [sys gc]
    }

    method equate {dest col1 col2} {
	if {![dict exists $m_columns $col1]} {
	    return -code error -errorcode [list FDDD NoSuchColumn $col1] \
		"no such column: \"$col1\""
	}
	if {![dict exists $m_columns $col2]} {
	    return -code error -errorcode [list FDDD NoSuchColumn $col2] \
		"no such column: \"$col2\""
	}
	set vars1 [dict get $m_columns $col1]
	set vars2 [dict get $m_columns $col2]
	if {[llength $vars1] != [llength $vars2]} {
	    return -code error \
		-errorcode [list FDDD EquateWrongDomains $col1 $col2] \
		"cannot equate domains \"$col1\" and \"$col2\":\
                 sizes do not match"
	}
	# TODO - Typecheck $dest and sort one list in decreasing order by var#
	sys := $dest 1
	foreach v $vars1 v2 $vars2 {
	    sys nthvar _a $v
	    sys nthvar _b $v2
	    sys == temp _a _b
	    sys & $dest $dest temp
	}
	sys unset temp _a _b
    }

    method join {dest source1 source2} {
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
................................................................................
	if {![dict exists $m_relcolumns $dest]} {
	    return -code error \
		-errorcode [list FDDD RelationNotDefined $dest] \
		"relation \"$dest\" is not defined in this database"
	}
	if {$source eq {}} {
	    set source 0
	} elseif {$source eq {_}} {
	    set source 1
	} else {
	    if {![dict exists $m_relcolumns $source]} {
		return -code error \
		    -errorcode [list FDDD RelationNotDefined $source] \
		    "relation \"$source\" is not defined in this database"
	    }
	    if {[dict get $m_relcolumns $dest]