Jason (jcreed) wrote,
Jason
jcreed

Adventures in debugging:

The princeton suite is roughtly 10kTd (kiloTwelf declarations) in size. I run my code on it, it chokes at declaration 2447. So I have 2kTd to think about. I finally get my stupid code working that is supposed to filter out just those declarations that a given one depends on, and reduce this to 100Td that are sufficient to evince the same bug. By manually inlining some definitions and performing some habitual reductions, I get this down to around 80Td before I find a single definition which, if inlined, makes the bug not tripped. An educated guess leads me to a file only 5Td long:
%use word32.
zero : word32 = 0.
a : word32 -> type.
c : {x:word32} a x.
test : a zero = c 0.

Now to figure out why this breaks. A typical line from the 80Td thing that I was afraid I'd have to painfully whittle down by hand is this beast:
pow2_32_eq_65536*65536 = cut_1313 (eq_1244 k (arr (*_1762 (const_83 0)
(const_83 bignum_base_169)) (const_83 1)) (const_83 1)) (eq_1244 k
(dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0)
(arr (const_83 65536) (c_2394 65536))) (congr_1315 k (*_1762 (const_83
0) (const_83 bignum_base_169)) (const_83 0) ([z1:o] eq_1244 k (arr z1
(const_83 1)) (const_83 1)) (zero_times_1808 (const_83
bignum_base_169)) (zero_plus_1770 (const_83 1))) ([p1:pf_5 (eq_1244 k
(dig_171 bignum_170 1) (const_83 1))] cut_1313 (==_1246 k (dig_171
(dig_171 bignum_170 1) 0) (c_2394 bignum_base_169)) (eq_1244 k
(dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0)
(arr (const_83 65536) (c_2394 65536))) (trans_1321 k (dig_171 (dig_171
bignum_170 1) 0) (*_1762 (const_83 1) (c_2394 bignum_base_169))
(c_2394 bignum_base_169) (dig0lem1_2446 (dig_171 bignum_170 1)
(const_83 1) p1) (one_times_1778 (c_2394 bignum_base_169))) ([p2:pf_5
(eq_1244 k (dig_171 (dig_171 bignum_170 1) 0) (const_83
bignum_base_169))] cut_1313 (==_1246 k (dig_171 (dig_171 (dig_171
bignum_170 1) 0) 0) (c_2394 65536)) (eq_1244 k (dig_171 (dig_171
(dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0) (arr (const_83
65536) (c_2394 65536))) (trans_1321 k (dig_171 (dig_171 (dig_171
bignum_170 1) 0) 0) (*_1762 (const_83 bignum_base_169) (c_2394
bignum_base_169)) (c_2394 65536) (dig0lem1_2446 (dig_171 (dig_171
bignum_170 1) 0) (const_83 bignum_base_169) p2) (eval_times_2438 256
256 65536 256*256_2427)) ([p3:pf_5 (eq_1244 k (dig_171 (dig_171
(dig_171 bignum_170 1) 0) 0) (const_83 65536))] cut_1313 (==_1246 k
(dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0)
(*_1762 (const_83 65536) (*_1762 (c_2394 bignum_base_169) (c_2394
bignum_base_169)))) (eq_1244 k (dig_171 (dig_171 (dig_171 (dig_171
(dig_171 bignum_170 1) 0) 0) 0) 0) (arr (const_83 65536) (c_2394
65536))) (trans_1321 k (dig_171 (dig_171 (dig_171 (dig_171 (dig_171
bignum_170 1) 0) 0) 0) 0) (*_1762 (*_1762 (const_83 65536) (c_2394
bignum_base_169)) (c_2394 bignum_base_169)) (*_1762 (const_83 65536)
(*_1762 (c_2394 bignum_base_169) (c_2394 bignum_base_169)))
(dig0lem1_2446 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0)
0) (*_1762 (const_83 65536) (c_2394 bignum_base_169)) (dig0lem1_2446
(dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) (const_83 65536) p3))
(times_assoc_1775 (const_83 65536) (c_2394 bignum_base_169) (c_2394
bignum_base_169))) ([p4:pf_5 (eq_1244 k (dig_171 (dig_171 (dig_171
(dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0) (arr (const_83 65536) (arr
(const_83 bignum_base_169) (const_83 bignum_base_169))))] congr_1315 k
(c_2394 65536) (*_1762 (c_2394 256) (c_2394 256)) ([z2:o] eq_1244 k
(dig_171 (dig_171 (dig_171 (dig_171 (dig_171 bignum_170 1) 0) 0) 0) 0)
(arr (const_83 65536) z2)) (symm_1320 k (*_1762 (c_2394 256) (c_2394
256)) (c_2394 65536) (eval_times_2438 256 256 65536 256*256_2427))
p4)))).
Tags: programming, work
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 5 comments