A program executing on a low-end embedded system, such as a smart-card, faces scarce memory resources and fixed execution time constraints. We demonstrate that factorization of common instruction sequences in java byt...
详细信息
A program executing on a low-end embedded system, such as a smart-card, faces scarce memory resources and fixed execution time constraints. We demonstrate that factorization of common instruction sequences in java bytecode allows the memory footprint to be reduced, on average, to 85% of its original size, with a minimal execution time penalty. While preserving java compatibility, our solution requires only a few modifications which are straightforward to implement in any JVM used in a low-end embedded system.
It is important to prove that supposedly terminating programs actually terminate, particularly if those programs must be run on critical systems or downloaded into a client such as a mobile phone. Although termination...
详细信息
It is important to prove that supposedly terminating programs actually terminate, particularly if those programs must be run on critical systems or downloaded into a client such as a mobile phone. Although termination of computer programs is generally undecidable, it is possible and useful to prove termination of a large, nontrivial subset of the terminating programs. In this article, we present our termination analyzer for sequential java bytecode, based on a program property called path-length. We describe the analyses which are needed before the path-length can be computed such as sharing, cyclicity, and aliasing. Then we formally define the path-length analysis and prove it correct with respect to a reference denotational semantics of the bytecode. We show that a constraint logic program P-CLP can be built from the result of the path-length analysis of a java bytecode program P and formally prove that if P-CLP terminates, then P also terminates. Hence a termination prover for constraint logic programs can be applied to prove the termination of P. We conclude with some discussion of the possibilities and limitations of our approach. Ours is the first existing termination analyzer for java bytecode dealing with any kind of data structures dynamically allocated on the heap and which does not require any help or annotation on the part of the user.
The java virtual machine embodies a verifier that performs a set of checks on java bytecode programs before their execution. The verifier carries out an efficient data-flow analysis applied to a type-level abstract in...
详细信息
The java virtual machine embodies a verifier that performs a set of checks on java bytecode programs before their execution. The verifier carries out an efficient data-flow analysis applied to a type-level abstract interpretation of the code. The implementations of the bytecode verifier presented a significant problem with programs compiled with the Sun java compiler (until version 1.4.1): there were legal java programs which were correctly compiled into a bytecode that was rejected by the verifier. The problem was fixed by removing, in version 1.4.2 and following, some interesting features in the compilation of the try-finally java construct. Because removing such features has a cost in terms of memory space, in this paper we propose to enhance the bytecode verifier to accept such programs, maintaining the space efficiency of the previous versions of the compiler. We define an abstract interpretation framework in which we model the enhanced version of the verifier. The defined abstract interpretation framework can be considered a good basis for other static analyses of bytecode programs.
This paper presents a method for translation of java byte-code sequences into synthesizable hardware, using the Bluespec SystemVerilog (BSV) environment. At the core of our approach lies a BSV description of a subset ...
详细信息
ISBN:
(纸本)9781450316880
This paper presents a method for translation of java byte-code sequences into synthesizable hardware, using the Bluespec SystemVerilog (BSV) environment. At the core of our approach lies a BSV description of a subset of java bytecodes, that can be used to directly translate bytecode sequences into a BSV specification. The result is intended as an accelerator for existing java processors (JOP, BlueJEP) or even standalone hardware. Preliminary evaluation shows our solution to produce hardware on par with established methods (area/performance), while supporting rare features (e.g. easy to automate, method calls and recursion).
Reasoning about java bytecode (JBC) is complicated due to its unstructured control-flow, the use of three-address code combined with the use of an operand stack, etc. Therefore, many static analyzers and model checker...
详细信息
Reasoning about java bytecode (JBC) is complicated due to its unstructured control-flow, the use of three-address code combined with the use of an operand stack, etc. Therefore, many static analyzers and model checkers for JBC first convert the code into a higher-level representation. In contrast to traditional decompilation, such representation is often not java source, but rather some intermediate language which is a good input for the subsequent phases of the tool. Interpretive decompilation consists in partially evaluating an interpreter for the compiled language (in this case JBC) written in a high-level language with respect to the code to be decompiled. There have been proofs-of-concept that interpretive decompilation is feasible, but there remain important open issues when it comes to decompile a real language such as JBC. This paper presents, to the best of our knowledge, the first modular scheme to enable interpretive decompilation of a realistic programming language to a high-level representation, namely of JBC to Prolog. We introduce two notions of optimality, which together require that decompilation does not generate code more than once for each program point. We demonstrate the impact of our modular approach and optimality issues on a series of realistic benchmarks. Decompilation times and decompiled program sizes are! linear with the size of the input bytecode program. This demonstrates empirically the scalability, of modular decompilation of JBC by partial evaluation. (C) 2009 Elsevier B.V. All rights reserved.
java is an ideal platform for implementing mobile code systems, not only because of its portability but also because it is designed with security in mind. Untrusted java programs can be statically analyzed and validat...
详细信息
java is an ideal platform for implementing mobile code systems, not only because of its portability but also because it is designed with security in mind. Untrusted java programs can be statically analyzed and validated. The program's behavior is then monitored to prevent potentially malicious operations. Static analysis of untrusted classes is carried out by a component of the java virtual machine called the verifier. The most complex part of the verification process is the dataflow analysis, which is performed on each method in order to ensure type-safety. This paper clarifies in detail one of the tricky aspects of the dataflow analysis: the verification of object initialization. We present and explain the rules that need to be enforced and we then show how verifier implementations can enforce them. Rules for object creation require, among other things, that uninitialized objects never be used before they are initialized. Constructors must properly initialize their this argument before they are allowed to return. This paper also deals with initialization failures (indicated by exceptions): the object being initialized must be discarded, and constructors must propagate initialization failures. (C) 2000 Elsevier Science B.V. All rights reserved.
Non-termination analysis proves that programs, or parts of a program, do not terminate. This is important since non-termination is often an unexpected behaviour of computer programs and exposes a bug in their code. Wh...
详细信息
Non-termination analysis proves that programs, or parts of a program, do not terminate. This is important since non-termination is often an unexpected behaviour of computer programs and exposes a bug in their code. While research has found ways of proving non-termination of logic programs and of term rewriting systems, this is hardly the case for imperative programs. In this paper, we describe and experiment with a technique for proving non-termination of imperative, bytecode programs by relating their non-termination to that of a (constraint) logic program. Moreover, we show that our non-termination test effectively helps a termination test, by avoiding expensive search for termination proofs of those portions of the code where such proofs do not exist.
Recently, we proposed a general framework for the cost analysis of java bytecode which can be used for measuring resource usage. This analysis generates, at compile-time, cost relations which define the cost of progra...
详细信息
Recently, we proposed a general framework for the cost analysis of java bytecode which can be used for measuring resource usage. This analysis generates, at compile-time, cost relations which define the cost of programs as a function of their input data size. The purpose of this paper is to assess the practicality of such cost analysis by experimentally evaluating a prototype analyzer implemented in Ciao. With this aim, we approximate the computational complexity of a set of selected benchmarks, including both well-known algorithms which have been used to evaluate existing cost analyzers in other programming paradigms, and other benchmarks which illustrate object-oriented features. In our evaluation, we first study whether the generated cost relations can be automatically solved. Our experiments show that in some cases the inferred cost relations can be automatically solved by using the Mathematica system, whereas, in other cases, some prior manipulation is required for the equations to be solvable. Moreover, we experimentally evaluated the running time of the different phases of the analysis process. Overall, we believe our experiments show that the efficiency of our cost analysis is acceptable, and that the obtained cost relations are useful in practice since, at least in our experiments, it is possible to get a closed form solution.
In an earlier work, a termination analyzer for java bytecode was developed that translates a java bytecode program into a constraint logic program and then proves the termination of the latter. An efficiency bottlenec...
详细信息
In an earlier work, a termination analyzer for java bytecode was developed that translates a java bytecode program into a constraint logic program and then proves the termination of the latter. An efficiency bottleneck of the termination analyzer is the construction of a proof of termination for the generated constraint logic program, which is often very large in size. In this paper, a set of program simplifications are presented that reduce the size of the constraint logic program without changing its termination behavior. These simplifications remove program clauses and/or predicate arguments that do not affect the termination behavior of the constraint logic program. Their effect is to reduce significantly the time needed to build the termination proof for the constraint logic program, as our experiments show.
The interpretative approach to compilation allows compiling programs by partially evaluating an interpreter w.r.t. a source program. This approach, though very attractive in principle, has not been widely applied in p...
详细信息
The interpretative approach to compilation allows compiling programs by partially evaluating an interpreter w.r.t. a source program. This approach, though very attractive in principle, has not been widely applied in practice mainly because of the difficulty in finding a partial evaluation strategy which always obtain "quality" compiled programs. In spite of this, in recent work we have performed a proof of concept of that, at least for some examples, this approach can be applied to decompile java bytecode into Prolog. This allows applying existing advanced tools for analysis of logic programs in order to verify java bytecode. However, successful partial evaluation of an interpreter for (a realistic subset of) java bytecode is a rather challenging problem. The aim of this work is to improve the performance of the decompilation process above in two respects. First, we would like to obtain quality decompiled programs, i.e., simple and small. We refer to this as the effectiveness of the decompilation. Second, we would like the decompilation process to be as efficient as possible, both in terms of time and memory usage, in order to scale up in practice. We refer to this as the efficiency of the decompilation. With this aim, we propose several techniques for improving the partial evaluation strategy. We argue that our experimental results show that we are able to improve significantly the efficiency and effectiveness of the decompilation process.
暂无评论