Research On The Key Techniques Of Runtime Verification On Typestate Property

Programmers usually have to conform to some constraints when using the third-party or system libraries.These constraints are also known as the typestate properties,and can be expressed by temporal specifications with free variables.Lots of large-scale software system errors are caused by the violations of typestate properties.What is worse,it is very difficult and time-consuming to find out and fix these errors.The static analysis of a program with respect to a typestate property is generally undecidable.Usually,dynamic analysis approaches,such as runtime verification,has been applied to check whether the program violate the specified typestate.Runtime verification automatically convert typestate properties into runtime monitors that can detect the property violations at runtime.Implementing runtime monitoring needs to instrument the monitored programs.However,the programs monitored by runtime monitors usually contain many redundant instrumentations,which result in a significant monitoring overhead.In the recent years,hybrid typestate analysis has been proposed to eliminate unnecessary monitoring instrumentations for runtime monitors at compile-time.Nop-shadows Analysis(NSA)proposed by Eric Bodden is one of these hybrid typestate analysis.Before generating residual monitors,NSA performs the dataflow analysis which is intra-procedural flow-sensitive and partially context-sensitive to improve runtime performance.Although NSA is precise,there are some cases on which it has little effects.In order to find out the reasons,we dissected the algorithm of data-flow analysis used in the NSA,and made an investigation on the failed cases.In this paper,we propose three optimizations to further improve the precision of NSA.These three optimizations are complementary to each other.They separately address different aspects of the issues that can potentially lead NSA to lose precision.To summarize,our works has the following contributions:1.We make a definition for the changeless configurations generated from backward data flow analysis,and propose the first optimization based on the changeless configuration.In order to identify these types of configurations,we extend the original configuration tuple with a boolean variable which indicates whether the states of this configuration have ever been through a state transition.In addition,we modify the configuration transition algorithm,and propose a rule 1 to filter changeless configurations when identifying unnecessary instrumentations.We have proved the correctness of the rule.In general,the first optimization works well on the methods containing several interleaved relevant method invocations on different objects.2.We make a definition for local object and inter-procedural configuration,and propose the second optimization based on the local object to improve the accuracy of NSA.We propose and implement an approximate,but sound,intra-procedural flow-sensitive algorithm to determine whether a variable points to a local object.We also extend the original configuration tuple with a boolean variable which indicates whether the current configuration is indeed gotten by statically modeling the multiple consecutive invocations of the method being analysed.In addition,we modify the configuration transition algorithm,and propose a rule to filter interprocedural configurations when identifying unnecessary instrumentations.We have proved the correctness of the rule too.3.We propose the third optimization based on partial inter-procedural flow-sensitive information.The main idea is to refine the inter-procedural data-flow analysis induced by statements of method call with partial flow-sensitive information contained in the called methods.Compared to the full inter-procedural flow-sensitive static analysis,the extra overhead incurred by our optimization can be negligible.We introduce two new operators on variable bindings and configuration to calculate the resulting configuration set related to statements of method call.In addition,we design an algorithm to determine whether two static objects coming from a caller and the responding callee respectively are must-alias during the execution of the caller,and introduce the workflow of the third optimization.4.We have integrated our optimizations into Clara and conducted extensive experiments on the Da Capo benchmark to evaluate our optimizations.The experimental results indicate that our optimizations can further remove unnecessary instrumentations after the original NSA in more than half of the cases.Specifically,our optimizations can remove 11 unnecessary instrumentations on average.For two cases,all the remaining instrumentations in the monitored programs are removed,which implies the program is proved to satisfy the typestate property and free of runtime monitoring.The extra analysis time incurred by our optimization is relatively few.Considering the total compilation time,the overhead incurred by our optimizations is acceptable.