What is a type error? [correction]
in [Lisp]
|
From: David Hopwood on 17 Jul 2006 15:41 David Hopwood wrote: > Darren New wrote: > >>From what I can determine, the authors seem to imply that typestate is >>dataflow analysis modified in (at least) two ways: >> >>1) When control flow joins, the new typestate is the intersection of >>typestates coming into the join, where as dataflow analysis doesn't >>guarantee that. (They imply they think dataflow analysis is allowed to >>say "the variable might or might not be initialized here", while >>typestate would ensure the variable is uninitialized.) > > Right, but this is a disadvantage of their typestate algorithm. It is why > the example in Figure 2 of > <http://www.cs.ubc.ca/local/reading/proceedings/spe91-95/spe/vol25/issue4/spe950wk.pdf> > fails to check, even though it "obviously" initializes all variables. > > Consider the equivalent Java program: I mixed up Figures 1 and 2. Here is the Java program that Figure 2 should be compared to: public class LoopInitTest { public static String getString() { return "foo"; } public static void main(String[] args) { String line = getString(); boolean is_last = false; while (!is_last) { if (line.charAt(0) == 'q') { is_last = true; } // insert line into inputs (not important for analysis) if (!is_last) { line = getString(); } } } } which compiles without error, because is_last is definitely initialized. -- David Hopwood <david.nospam.hopwood(a)blueyonder.co.uk>
From: Darren New on 17 Jul 2006 15:55 David Hopwood wrote: > > public class LoopInitTest { > public static String getString() { return "foo"; } > > public static void main(String[] args) { > String line = getString(); > boolean is_last = false; > > while (!is_last) { > if (line.charAt(0) == 'q') { > is_last = true; > } > > // insert line into inputs (not important for analysis) > > if (!is_last) { > line = getString(); > } > } > } > } > > which compiles without error, because is_last is definitely initialized. At what point do you think is_last or line would seem to not be initialized? They're both set at the start of the function, and (given that it's Java) nothing can unset them. At the start of the while loop, it's initialized. At the end of the while loop, it's initialized. So the merge point of the while loop has it marked as initialized. Now, if the "insert line into inputs" actually unset "line", then yes, you're right, Hermes would complain about this. Alternately, if you say if (x) v = 1; if (x) v += 1; then Hermes would complain when it wouldn't need to. However, that's more a limitation of the typestate checking algorithms than the concept itself; that is to say, clearly the typestate checker could be made sufficiently intelligent to track most simple versions of this problem and not complain, by carrying around conditionals in the typestate description. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops.
From: Darren New on 17 Jul 2006 16:18 Darren New wrote: > Now, if the "insert line into inputs" actually unset "line", then yes, > you're right, Hermes would complain about this. Oh, I see. You translated from Hermes into Java, and Java doesn't have the "insert into" statement. Indeed, the line you commented out is *exactly* what's important for analysis, as it unsets line. Had it been insert copy of line into inputs then you would not have gotten any complaint from Hermes, as it would not have unset line there. In this case, it's equivalent to if (!is_line) line = getString(); if (!is_line) use line for something... except the second test is at the top of the loop instead of the bottom. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops.
From: David Hopwood on 17 Jul 2006 22:32 Darren New wrote: > David Hopwood wrote: > >> public class LoopInitTest { >> public static String getString() { return "foo"; } >> >> public static void main(String[] args) { >> String line = getString(); >> boolean is_last = false; >> >> while (!is_last) { >> if (line.charAt(0) == 'q') { >> is_last = true; >> } >> >> // insert line into inputs (not important for analysis) >> >> if (!is_last) { >> line = getString(); >> } >> } >> } >> } >> >> which compiles without error, because is_last is definitely initialized. > > At what point do you think is_last or line would seem to not be > initialized? They're both set at the start of the function, and (given > that it's Java) nothing can unset them. > > At the start of the while loop, it's initialized. At the end of the > while loop, it's initialized. So the merge point of the while loop has > it marked as initialized. Apparently, Hermes (at least the version of it described in that paper) essentially forgets that is_last has been initialized at the top of the loop, and so when it does the merge, it is merging 'not necessarily initialized' with 'initialized'. This sounds like a pretty easy thing to fix to me (and maybe it was fixed later, since there are other papers on Hermes' typestate checking that I haven't read yet). -- David Hopwood <david.nospam.hopwood(a)blueyonder.co.uk>
From: Darren New on 18 Jul 2006 12:13
David Hopwood wrote: > Darren New wrote: > >>David Hopwood wrote: >> >> >>>public class LoopInitTest { >>> public static String getString() { return "foo"; } >>> >>> public static void main(String[] args) { >>> String line = getString(); >>> boolean is_last = false; >>> >>> while (!is_last) { >>> if (line.charAt(0) == 'q') { >>> is_last = true; >>> } >>> >>> // insert line into inputs (not important for analysis) >>> >>> if (!is_last) { >>> line = getString(); >>> } >>> } >>> } >>>} >>> >>>which compiles without error, because is_last is definitely initialized. >> >>At what point do you think is_last or line would seem to not be >>initialized? They're both set at the start of the function, and (given >>that it's Java) nothing can unset them. >> >>At the start of the while loop, it's initialized. At the end of the >>while loop, it's initialized. So the merge point of the while loop has >>it marked as initialized. > > > Apparently, Hermes (at least the version of it described in that paper) > essentially forgets that is_last has been initialized at the top of the > loop, and so when it does the merge, it is merging 'not necessarily initialized' > with 'initialized'. No, it's not that it "forgets". It's that the "insert line into inputs" unitializes "line". Hence, "line" is only conditionally set at the bottom of the loop, so it's only conditionally set at the top of the loop. > This sounds like a pretty easy thing to fix to me (and maybe it was fixed > later, since there are other papers on Hermes' typestate checking that I > haven't read yet). You simply misunderstand the "insert line into inputs" semantics. Had that line actually been commented out in the Hermes code, the loop would have compiled without a problem. That said, in my experience, finding this sort of typestate error invariably led me to writing clearer code. boolean found_ending = false; while (!found_ending) { string line = getString(); if (line.charAt(0) == 'q') found_ending = true; else insert line into inputs; } It seems that's much clearer to me than the contorted version presented as the example. If you want it to work like the Java code, where you can still access the "line" variable after the loop, the rearrangement is trivial and transparent as well. -- Darren New / San Diego, CA, USA (PST) This octopus isn't tasty. Too many tentacles, not enough chops. |