From Jinja bytecode to term rewriting: a complexity reflecting transformation. (English) Zbl 1395.68160
Summary: In this paper we show how the runtime complexity of imperative programs can be analysed fully automatically by a transformation to term rewrite systems, the complexity of which can then be automatically verified by existing complexity tools. We restrict to well-formed Jinja bytecode programs that only make use of non-recursive methods. The analysis can handle programs with cyclic data only if the termination behaviour is independent thereof.
We exploit a term-based abstraction of programs within the abstract interpretation framework. The proposed transformation encompasses two stages. For the first stage we perform a combined control and data flow analysis by evaluating program states symbolically, which is shown to yield a finite representation of all execution paths of the given program through a graph, dubbed computation graph. In the second stage we encode the (finite) computation graph as a term rewrite system. This is done while carefully analysing complexity preservation and reflection of the employed transformations such that the complexity of the obtained term rewrite system reflects on the complexity of the initial program. Finally, we show how the approach can be automated and provide ample experimental evidence of the advantages of the proposed analysis.
We exploit a term-based abstraction of programs within the abstract interpretation framework. The proposed transformation encompasses two stages. For the first stage we perform a combined control and data flow analysis by evaluating program states symbolically, which is shown to yield a finite representation of all execution paths of the given program through a graph, dubbed computation graph. In the second stage we encode the (finite) computation graph as a term rewrite system. This is done while carefully analysing complexity preservation and reflection of the employed transformations such that the complexity of the obtained term rewrite system reflects on the complexity of the initial program. Finally, we show how the approach can be automated and provide ample experimental evidence of the advantages of the proposed analysis.
MSC:
| 68Q30 | Algorithmic information theory (Kolmogorov complexity, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
| 68Q42 | Grammars and rewriting systems |
References:
| [1] | Middeldorp, A.; Moser, G.; Neurauter, F.; Waldmann, J.; Zankl, H., Joint spectral radius theory for automated complexity analysis of rewrite systems, (Proc. 4th CAI, LNCS, vol. 6742, (2011)), 1-20 · Zbl 1307.68042 |
| [2] | Avanzini, M.; Moser, G., Polynomial path orders, Log. Methods Comput. Sci., 9, 4, (2013) · Zbl 1314.68170 |
| [3] | Waldmann, J., Matrix interpretations on polyhedral domains, (Proc. of 26th RTA, (2015)), 318-333 · Zbl 1366.68129 |
| [4] | Avanzini, M.; Eguchi, N.; Moser, G., New order-theoretic characterisation of the polytime computable functions, Theor. Comput. Sci., 585, 3-24, (2015) · Zbl 1327.68142 |
| [5] | Hirokawa, N.; Moser, G., Automated complexity analysis based on the dependency pair method, (Proc. 4th IJCAR, LNCS, vol. 5195, (2008)), 364-380 · Zbl 1165.68390 |
| [6] | Hirokawa, N.; Moser, G., Complexity, graphs, and the dependency pair method, (Proc. of 15th LPAR, (2008)), 652-666 · Zbl 1182.68095 |
| [7] | Noschinski, L.; Emmes, F.; Giesl, J., Analyzing innermost runtime complexity of term rewriting by dependency pairs, J. Autom. Reason., 51, 1, 27-56, (2013) · Zbl 1314.68174 |
| [8] | Zankl, H.; Korp, M., Modular complexity analysis via relative complexity, (Proc. 21st RTA, LIPIcs, vol. 6, (2010)), 385-400 · Zbl 1236.68158 |
| [9] | Avanzini, M.; Moser, G., A combination framework for complexity, Inf. Comput., 248, 22-55, (2016) · Zbl 1339.68135 |
| [10] | Frohn, F.; Giesl, J.; Hensel, J.; Aschermann, C.; Ströder, T., Inferring lower bounds for runtime complexity, (Proc. of 26th RTA, LIPIcs, (2015)), 334-349 · Zbl 1366.68116 |
| [11] | Moser, G., Proof theory at work: complexity analysis of term rewrite systems, (2009), CoRR |
| [12] | Giesl, J.; Ströder, T.; Schneider-Kamp, P.; Emmes, F.; Fuhs, C., Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs, (Proc. of 14th PPDP, (2012), ACM), 1-12 |
| [13] | Avanzini, M.; Lago, U. D.; Moser, G., Analysing the complexity of functional programs: higher-order meets first-order, (Proc. 20th ICFP, (2015), ACM), 152-164 · Zbl 1360.68313 |
| [14] | Stärk, R.; Schmid, J.; Börger, E., Java and the Java virtual machine: definition, verification, validation, (2001), Springer · Zbl 0978.68033 |
| [15] | Klein, G.; Nipkow, T., A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Trans. Program. Lang. Syst., 28, 4, 619-695, (2006) |
| [16] | Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Proc. 4th POPL, (1977)), 238-252 |
| [17] | Secci, S.; Spoto, F., Pair-sharing analysis of object-oriented programs, (Proc. 12th SAS, LNCS, vol. 3672, (2005)), 320-335 · Zbl 1141.68378 |
| [18] | Rossignoli, S.; Spoto, F., Detecting non-cyclicity by abstract compilation into Boolean functions, (Proc. 7th VMCAI, LNCS, vol. 3855, (2006)), 95-110 · Zbl 1176.68043 |
| [19] | Genaim, S.; Zanardini, D., Reachability-based acyclicity analysis by abstract interpretation, Theor. Comput. Sci., 474, 60-79, (2013) · Zbl 1259.68242 |
| [20] | Avanzini, M.; Moser, G., Tyrolean complexity tool: features and usage, (Proc. of 24th RTA, LIPIcs, vol. 21, (2013)), 71-80 · Zbl 1356.68093 |
| [21] | Avanzini, M.; Moser, G.; Schaper, M., Tct: Tyrolean complexity tool, (Proc. 22nd TACAS, LNCS, (2016)), 407-423 |
| [22] | Lochbihler, A., Jinja with threads, Arch. Formal Proofs, (2007) |
| [23] | Lochbihler, A., Verifying a compiler for Java threads, (Proc. 19th ESOP, LNCS, vol. 6012, (2010)), 427-447 · Zbl 1260.68080 |
| [24] | Schaper, M., A complexity preserving transformation from jinja bytecode to rewrite systems, (2014), University of Innsbruck Austria, Master’s thesis |
| [25] | Frohn, F.; Brockschmidt, M.; Giesl, J., Automated inference of upper complexity bounds for Java programs, (Proceedings of the 15th International Workshop on Termination, (2016)) · Zbl 1475.68134 |
| [26] | Hoffmann, J.; Aehlig, K.; Hofmann, M., Multivariate amortized resource analysis, ACM Trans. Program. Lang. Syst., 34, 3, 14, (2012) |
| [27] | Otto, C.; Brockschmidt, M.; v. Essen, C.; Giesl, J., Automated termination analysis of Java bytecode by term rewriting, (Proc. 21st RTA, (2010)), 259-276 · Zbl 1236.68145 |
| [28] | TeReSe, Term rewriting systems, Cambridge Tracks in Theoretical Computer Science, vol. 55, (2003), Cambridge University Press · Zbl 1030.68053 |
| [29] | Brockschmidt, M.; Otto, C.; von Essen, C.; Giesl, J., Termination graphs for Java bytecode, (Verification, Induction, Termination Analysis, LNCS, vol. 6463, (2010)), 17-37 · Zbl 1309.68038 |
| [30] | Brockschmidt, M.; Otto, C.; Giesl, J., Modular termination proofs of recursive Java bytecode programs by term rewriting, (Proc. 22nd RTA, LIPIcs, (2011)), 155-170 · Zbl 1236.68036 |
| [31] | Brockschmidt, M.; Musiol, R.; Otto, C.; Giesl, J., Automated termination proofs for Java bytecode with cyclic data, (Proc. 24th CAV, LNCS, vol. 7358, (2012)), 105-122 |
| [32] | Sagiv, M.; Reps, T.; Wilhelm, R., Parametric shape analysis via 3-valued logic, (Proc. 26th POPL, (1999), ACM), 105-118 |
| [33] | Nielson, F.; Nielson, H.; Hankin, C., Principles of program analysis, (2005), Springer · Zbl 1069.68534 |
| [34] | Falke, S.; Kapur, D., A term rewriting approach to the automated termination analysis of imperative programs, (Proc. 22nd CADE, LNCS, vol. 5663, (2009)), 277-293 · Zbl 1250.68141 |
| [35] | Falke, S.; Kapur, D.; Sinz, C., Termination analysis of C programs using compiler intermediate languages, (Proc. 22nd RTA, LIPIcs, vol. 10, (2011)), 41-50 · Zbl 1236.68040 |
| [36] | Sakata, T.; Nishida, N.; Sakabe, T., On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs, (Proc. of 20th WFLP, LNCS, vol. 6816, (2011)), 138-155 · Zbl 1339.68141 |
| [37] | Kop, C.; Nishida, N., Term rewriting with logical constraints, (Proc. 9th FroCos, LNCS, vol. 8152, (2013), Springer), 343-358 · Zbl 1398.68276 |
| [38] | Fuhs, C.; Giesl, J.; Plücker, M.; Schneider-Kamp, P.; Falke, S., Proving termination of integer term rewriting, (Proc. 20th RTA, LNCS, vol. 5595, (2009)), 32-47 · Zbl 1242.68131 |
| [39] | Kop, C.; Nishida, N., Constrained term rewriting tool, (Proc. 20th LPAR, LNCS, (2015)), 549-557 · Zbl 1471.68110 |
| [40] | Brockschmidt, M.; Emmes, F.; Falke, S.; Fuhs, C.; Giesl, J., Alternating runtime and size complexity analysis of integer programs, (Proc. 20th TACAS, (2014)), 140-155 |
| [41] | Atkey, R., Amortised resource analysis with separation logic, (Proc. 19th ESOP, LNCS, vol. 6012, (2010), Springer), 85-103 · Zbl 1260.68083 |
| [42] | Albert, E.; Arenas, P.; Genaim, S.; Puebla, G.; Zanardini, D., Cost analysis of object-oriented bytecode programs, Theor. Comput. Sci., 413, 1, 142-159, (2012) · Zbl 1236.68042 |
| [43] | Zuleger, F.; Gulwani, S.; Sinn, M.; Veith, H., Bound analysis of imperative programs with the size-change abstraction, (Proc. 18th SAS, LNCS, vol. 6887, (2011)), 280-297 |
| [44] | Sinn, M.; Zuleger, F.; Veith, H., A simple and scalable static analysis for bound analysis and amortized complexity analysis, (Proc. 26th CAV, (2014)), 745-761 |
| [45] | Flores-Montoya, A.; Hähnle, R., Resource analysis of complex programs with cost equations, (Proc. 12th APLAS, (2014)), 275-295 · Zbl 1453.68047 |
| [46] | Fenacci, D.; MacKenzie, K., Static resource analysis for Java bytecode using amortisation and separation logic, Proc. 6th BYTECODE, Electron. Notes Theor. Comput. Sci., 279, 19-32, (2011) |
| [47] | Panitz, S. E.; Schmidt-Schauß TEA, M., Automatically proving termination of programs in a non-strict higher-order functional language, (Proc. 4th SAS, (1997)), 345-360 |
| [48] | Spoto, F.; Mesnard, F.; Payet, É., A termination analyzer for Java bytecode based on path-length, ACM Trans. Program. Lang. Syst., 32, 3, (2010) |
| [49] | Roşu, G.; Stefănescu, A., Checking reachability using matching logic, (Proc. 27th OOPSLA, (2012), ACM), 555-574 |
| [50] | Roşu, G.; Ellison, C.; Schulte, W., Matching logic: an alternative to Hoare/floyd logic, (Proc. 13th AMAST, LNCS, vol. 6486, (2010)), 142-162 · Zbl 1308.68045 |
| [51] | Stefănescu, A., Matchc: a matching logic reachability verifier using the K framework, Electron. Notes Theor. Comput. Sci., 304, 183-198, (2014) |
| [52] | Rival, X.; Mauborgne, L., The trace partitioning abstract domain, ACM Trans. Program. Lang. Syst., 29, 5, (2007) |
| [53] | Endrullis, J.; Waldmann, J.; Zantema, H., Matrix interpretations for proving termination of term rewriting, J. Autom. Reason., 40, 2-3, 195-220, (2008) · Zbl 1139.68049 |
| [54] | Avanzini, M.; Eguchi, N.; Moser, G., A path order for rewrite systems that compute exponential time functions, (Proc. of 22nd RTA, LIPIcs, vol. 10, (2011), Dagstuhl), 123-138 · Zbl 1236.68118 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
