Steven Evans edited Hypotheses_Upon_executing_the_analysis__.md  about 8 years ago

Commit id: c1de4cda862b4c7b460690bf78fd80b981993251

deletions | additions      

       

(1) follows from the fact that sets of system calls for each basic block \(F_i\) form their containing function \(f\) while (2) and (3) made from two partitions of \(F_i\) for \(i..n\). However, (3) would require extra types of system calls if \(f\) were called from \(g\). Because the analysis is done on a per function basis but considers system calls from other functions, \(g\) would have it's own sets of executed and to be executed system call which we'll call \(B\) and \(B'\). The context of \(B'\) is required because if it contained a system call \(s\) that was also in \(A\) but not \(A'\), then a pledge discluding \(s\) would be made after the latest added basic block in \(A\). With that context unioned with \(A'\), \(s\) will not be removed from subsequent pledges within \(f\) since it will be required after \(f\) has completed in \(g\). It's also important to note that if an execution of a program has a call stack with multiple functions \(g_i\) called before \(f\), only the context of the function call before it is required because each function would union its context into its subsequent called function.  The notion of a call stack is a dynamic one that would be normally be seen in an execution trace even though this analysis is static. The information needed to complete the analysis meaningfully can be derived from a call graph. A call graph can be used to determine which functions can possibly be called from any function. That determination is used to derive any recursion as well as the necessary contexts that will be needed when solving for \(A'\) so breaking pledges are not made.