Meta tags:
description=Just another WordPress.com weblog;

Headings (most frequently used words):

cdt, analysis, property, simulation, new, model, for, static, elliott, baron, blog, part, first, look, at, code, pages, archives, categories, blogroll, meta,

Text of the page (most frequently used words):
the (145), state (35), states (33), that (29), and (28), #property (28), for (27), analysis (25), this (21), execution (21), have (19), are (19), file (18), flow (18), symbolic (18), control (17), with (13), cdt (13), static (12), not (11), code (11), simulation (11), program (10), checker (10), close (10), open (10), from (10), all (10), each (10), graph (10), eclipse (9), opened (9), branch (9), algorithm (9), wordpress (8), variable (8), git (8), descriptor (7), point (7), path (7), sensitive (7), block (7), function (7), com (6), fedora (6), another (6), will (6), then (6), one (6), error (6), implementation (6), finite (6), machine (6), blog (5), org (5), 2009 (5), need (5), case (5), new (5), they (5), two (5), statements (5), fully (5), information (5), merge (5), our (5), call (5), example (5), just (5), comments (4), elliott (4), baron (4), uncategorized (4), assignment (4), work (4), codan (4), statement (4), ast (4), thus (4), false (4), which (4), also (4), boolean (4), called (4), set (4), model (4), where (4), modified (4), var (4), your (4), atoms (4), like (3), comment (3), report (3), log (3), already (3), december (3), posted (3), track (3), visit (3), order (3), visitor (3), problems (3), repository (3), look (3), has (3), list (3), variables (3), does (3), any (3), did (3), needs (3), use (3), abstract (3), via (3), extension (3), first (3), you (3), can (3), grouping (3), dataflow (3), more (3), 2002 (3), time (3), details (3), cause (3), their (3), into (3), either (3), paper (3), given (3), snippet (3), must (3), form (3), contains (3), temporal (3), occur (3), framework (3), consider (3), break (3), handles (3), them (3), since (3), edges (3), ivariable (3), get (2), design (2), site (2), website (2), required (2), sign (2), subscribed (2), subscribe (2), account (2), now (2), rss (2), create (2), september (2), about (2), search (2), multiple (2), translation (2), able (2), different (2), files (2), handle (2), there (2), much (2), user (2), clone (2), fedorapeople (2), ebaron (2), people (2), please (2), take (2), its (2), argument (2), iastname (2), iastfunctioncallexpression (2), looking (2), find (2), separately (2), because (2), stored (2), analyzing (2), source (2), syntax (2), tree (2), coding (2), problem (2), using (2), checkers (2), psa (2), performs (2), points (2), note (2), means (2), number (2), transition (2), esp (2), verification (2), polynomial (2), acm (2), language (2), only (2), discards (2), operations (2), complete (2), diagram (2), how (2), method (2), grouped (2), corresponding (2), joined (2), both (2), covers (2), methods (2), differ (2), way (2), here (2), execute (2), would (2), true (2), takes (2), structure (2), edge (2), references (2), out (2), following (2), associated (2), check (2), could (2), detect (2), condition (2), conditional (2), test (2), created (2), was (2), interface (2), along (2), plug (2), parsing (2), conditionals (2), than (2), literal (2), return (2), summaries (2), checking (2), unopened (2), node (2), implemented (2), class (2), expression (2), same (2), processed (2), objects (2), these (2), parallel (2), tools (2), project (2), weblog (2), started, name, email, write, loading, collapse, bar, manage, subscriptions, view, reader, content, privacy, entries, free, xfn, meta, blogroll, categories, archives, pages, units, should, descriptors, passed, between, secondary, may, copied, likely, still, done, usable, end, hosting, compared, previously, encountered, match, warning, action, begun, warn, users, attempting, yet, visits, expressions, store, returned, assigning, declaration, handled, declared, types, viewed, quite, differently, makes, generated, parser, detects, kind, pattern, elements, interest, unit, contributed, mechanism, recently, been, allows, quick, detection, potential, without, requiring, potentially, long, compile, running, through, external, tool, see, retains, doubles, seen, intractable, due, exponential, blowup, very, opposite, whenever, made, specific, discarded, mistakenly, lost, context, caused, image, credit, das, lerner, seigle, proceedings, sigplan, conference, programming, berlin, germany, june, pldi, york, implementing, follow, shortly, meets, approaches, middle, when, meaningful, but, even, though, depends, doing, avoid, inefficiencies, while, avoiding, reporting, click, shows, analyzes, sides, consolidated, union, join, performed, side, kept, three, simplified, known, keep, instant, includes, necessary, conditions, above, meaning, formula, subsequent, append, clause, basic, describe, solution, came, across, entitled, microsoft, research, university, washington, explains, compares, techniques, expressed, simply, traversed, containing, astvisitor, visited, before, assume, reality, know, improperly, executed, evaluates, int, o_rdonly, several, months, ago, discovered, improvements, namely, correctly, accounts, paths, abilities, instances, being, earlier, excerpt, md5sum, notice, eclipsecon, interested, thank, submitted, talk, gitweb, browse, hosted, pldt, ins, stock, included, unstructured, hurdle, assumption, children, parents, mentioned, constructs, improved, currently, recognize, similarly, pointer, dereferencing, arithmetic, issues, lastly, analyze, requires, value, switch, goto, continue, course, extended, global, rather, individual, functions, generating, contain, mappings, input, upon, consult, sites, simulate, executing, binary, closing, errors, callback, triggered, causes, displays, formatted, string, cases, fclose, tostring, extender, customizable, component, tracks, some, encoded, subclass, decisions, transitions, examining, defined, fsm, special, initial, define, own, core, extend, provide, encoding, rest, abstractpropsimchecker, performance, benefit, comes, groups, branches, cannot, partitions, suppose, group, disjunction, however, conjunctions, such, disjunctions, distinct, goal, minimal, terms, imply, original, simplifies, implies, leaves, every, fewer, faster, minimize, quine, mccluskey, minimization, works, demonstrated, further, simplify, substituting, truth, assignments, learned, traverses, breadth, manner, populating, dictionary, maps, sets, represents, operates, formulas, trick, chose, basis, obtainable, advantage, maintaining, binding, declarations, therefore, instance, conjunction, negations, covered, motivation, behind, move, onto, thing, needed, luckily, development, sub, provides, encapsulate, crucial, properly, vertices, blocks, directed, version, simple, intra, procedural, platform, previous, entry, part,

Text of the page (random words):
elliott baron s blog just another wordpress com weblog elliott baron s blog just another wordpress com weblog property simulation a new model for cdt s static analysis part 2 december 18 2009 in the previous entry i covered the details and motivation behind using property simulation for the cdt s static analysis now we will move onto the implementation details the first thing we needed was a control flow graph luckily the parallel language development tools sub project of the parallel tools platform already provides a control flow graph implementation for the cdt i modified this to encapsulate control flow edges since they are crucial to the property simulation algorithm thus the modified control flow graph properly contains both vertices blocks and directed edges the version of the property simulation algorithm i implemented is the simple intra procedural case this means the control flow of each function in the c c project is processed separately the algorithm traverses the control flow graph in a breadth first manner populating state information in a dictionary that maps control flow edges to sets of symbolic states each is a set of property states and an execution state each block in the control flow graph represents a node either an expression or statement in the ast to model execution states i have created a structure that operates on boolean formulas the trick is to then break if conditionals into atoms that are either true or false i chose ivariable objects as the basis for these atoms these objects are obtainable from the ast and have the advantage of maintaining a binding to their declarations therefore all references to a variable have the same ivariable instance associated with them so an execution state is conjunction of ivariable atoms and negations of atoms the performance benefit of property simulation comes from the way it groups symbolic states and discards branches that cannot occur the grouping function partitions all symbolic states by their property state then the execution states for all symbolic states with a given property state are joined for example suppose at a merge point we have two symbolic states opened xy and opened x y since they have the same property state we will group them into one symbolic state the execution state is then a disjunction of xy and x y however execution states are conjunctions of variables and as such disjunctions must be distinct execution states the goal is to find a minimal set of terms that imply the original execution states for our example xy x y simplifies to just x since x implies xy x y this leaves us with one symbolic state opened x every symbolic state must be processed for each block in the control flow graph thus the fewer symbolic states we have the faster the algorithm performs to minimize a set of execution states we use the quine mccluskey algorithm for boolean minimization which works much like i just demonstrated we further simplify this by substituting in any truth assignments we have learned from assignment statements property states are the extender s customizable component a checker tracks some temporal property that is encoded as a finite state machine of property states property states are implemented as an abstract class where the subclass handles decisions about state transitions by examining a statement or expression a finite state machine of property states is defined via an interface with methods to get all property states in the fsm along with the special initial and error states to define your own checker use the org eclipse cdt codan core checkers extension point and have your checker class extend abstractpropsimchecker provide your checker with the finite state machine encoding of your temporal property and the framework handles the rest we report errors via a callback by the algorithm with the ast node that triggered the problem and the execution state that causes the error condition to occur the execution state s tostring method displays the boolean form in a formatted string here is an example checking for cases where fclose is called on an unopened file checking for closing unopened files the test program is a modified excerpt from the md5sum program notice in one branch the file is not opened if binary is false of course this implementation is not complete the analysis needs to be extended to consider the global control flow of the program rather than just individual functions we can do this by generating summaries for each function which contain mappings from input symbolic states to where the function takes them upon its return we consult the summaries at function call sites to simulate executing the function unstructured code is another hurdle to consider break continue goto switch case statements and multiple return statements all cause problems in analyzing the control flow we have an assumption that a branch block has two children and a merge block has two parents which the mentioned constructs break conditional and assignment parsing also need to be improved currently we can only recognize conditionals that take the form var literal var literal var or var similarly pointer operations dereferencing arithmetic cause parsing issues lastly we need to be able to analyze more than one file handle at a time this requires an implementation of a value flow graph to track file handles i have hosted my code in a git repository on fedora people my property simulation implementation along with the open close example checker are in the org eclipse cdt codan extension plug in my modified pldt plug ins are also in the repository the stock static analysis framework is also included to check out the code git clone git fedorapeople org ebaron codan git or browse the gitweb interface i have submitted a talk for eclipsecon that covers property simulation and the cdt if you are interested please comment thank you posted in eclipse fedora static analysis uncategorized 1 comment property simulation a new model for cdt s static analysis december 16 2009 several months ago i discovered the need for improvements with eclipse cdt s static analysis namely we need an analysis model that correctly accounts for control flow paths of a program to test the abilities of the framework i created a checker to detect instances where close was being called on a file descriptor that did not have a corresponding open call earlier in the control flow consider the following snippet of code int fd if x fd open file o_rdonly close fd if we simply traversed a function containing this code with an astvisitor all we could do is detect that the open call is visited before the close call and assume there is no error condition in reality we know that close is called improperly if the branch is not executed thus we have a conditional error that will occur if x evaluates to false in my search for a solution i came across a paper entitled esp path sensitive program verification in polynomial time from microsoft research and the university of washington the paper explains and compares different static analysis techniques a temporal property to check is expressed as a finite state machine a finite state machine for our file open close example could look like 1 the finite state machine s states are known to the algorithm as property states we also keep track of the execution state of the program at a given instant this includes necessary conditions to execute a given block in the control flow graph in our code snippet above the open call would have an execution state of x meaning x must be true in order to execute that block each execution state takes the form of a boolean formula and subsequent if statements append another clause to it the basic structure that contains all of this information in the algorithm is called a symbolic state each symbolic state contains one or more property states and an execution state each edge in the control flow graph references a set of symbolic states that describe the state of the program at that point in our snippet the out edge of the open statement block would have the following symbolic state associated with it opened x the paper covers three static analysis methods which differ in the way symbolic states are grouped and simplified here is how they differ at merge points fully path sensitive analysis psa no grouping is performed all symbolic states from either side of the branch are kept dataflow analysis all symbolic states from both sides of the branch are consolidated into a union of the property states and join of execution states property simulation symbolic states are grouped by their property state corresponding execution states are joined this diagram shows how each method analyzes a control flow graph 1 click for the complete diagram you can see that the fully path sensitive analysis psa retains all information and performs no state grouping at merge points note that this means that each branch point doubles the number of states fully path sensitive analysis is seen as intractable due to this exponential blowup in the number of states the dataflow analysis does the very opposite whenever the execution state is made more specific by a branch point it is discarded at the merge point we then mistakenly transition to an error state because we lost the execution state context that caused the file to be opened property simulation meets the two approaches in the middle it only discards execution state information when the branch did not cause a property state transition thus it is not meaningful to our analysis note the fully path sensitive analysis but not property simulation stored execution state information for p even though the branch that depends on p does not have any file operations in doing this we avoid the inefficiencies of the fully path sensitive analysis while avoiding the false error reporting of the dataflow analysis details on my work implementing this algorithm for the cdt will follow shortly 1 image credit das m lerner s and seigle m 2002 esp path sensitive program verification in polynomial time in proceedings of the acm sigplan 2002 conference on programming language design and implementation berlin germany june 17 19 2002 pldi 02 acm new york ny 57 68 posted in eclipse fedora static analysis uncategorized 7 comments first look at cdt code analysis september 2 2009 recently i have been looking at static code analysis for the eclipse cdt this allows for quick detection of potential coding problems without requiring a potentially long compile or running the program through another external tool analyzing c c source code makes use of the abstract syntax tree generated by the cdt s c c parser a checker detects one kind of coding problem using a visitor pattern to visit elements of interest in the abstract syntax tree of a translation unit source file new checkers are contributed via eclipse s extension point mechanism i have begun work on a new checker to warn users if they are attempting to close a file that they did not open yet the visitor visits expressions looking for an open iastfunctioncallexpression then it needs to find the variable that will store the returned file descriptor from open the case of assigning the file descriptor to a variable in a declaration statement needs to be handled separately from assignment to an already declared variable this is because the two types of statements are viewed quite differently in the ast the iastname of the variable is stored in a list of opened file descriptor variables close file descriptor checker in action a close iastfunctioncallexpression has its argument compared with the list of previously encountered opened file descriptor variables if the iastname for close s argument does not match any in the list then we report a warning to the user i am hosting my cdt code analysis work in a git repository on fedora people please take a look git clone git fedorapeople org ebaron codan git there is still much work to be done for this checker to be usable for an end user problems visit order it is likely not the case that the visitor will visit code in the order of the control flow of a program secondary variable assignment we need to handle the case that an opened file descriptor variable may be copied to another variable multiple translation units we should be able to track file descriptors passed between different files posted in eclipse fedora static analysis uncategorized 2 comments search pages about archives december 2009 september 2009 categories eclipse 3 static analysis 3 fedora 3 uncategorized 3 blogroll wordpress com wordpress org meta create account log in xfn wordpress create a free website or blog at wordpress com entries rss and comments rss subscribe subscribed elliott baron s blog sign me up already have a wordpress com account log in now privacy elliott baron s blog subscribe subscribed sign up log in report this content view site in reader manage subscriptions collapse this bar loading comments write a comment email required name required website design a site like this with wordpress com get started