Grey literature is essential to software engineering research as it captures practices and decisions that rarely appear in academic venues. However, collecting and assessing it at scale remains difficult because of their heterogeneous sources, formats, and APIs that impede reproducible, large-scale synthesis. To address this issue, we present GLiSE, a prompt-driven tool that turns a research topic prompt into platform-specific queries, gathers results from common software-engineering web sources (GitHub, Stack Overflow) and Google Search, and uses embedding-based semantic classifiers to filter and rank results according to their relevance. GLiSE is designed for reproducibility with all settings being configuration-based, and every generated query being accessible. In this paper, (i) we present the GLiSE tool, (ii) provide a curated dataset of software engineering grey-literature search results classified by semantic relevance to their originating search intent, and (iii) conduct an empirical study on the usability of our tool.

Nowadays, many developers heavily rely on feedback from bug-detection tools to help ensure the quality of the code they produce. Such tools are underlain by static analysis. It is, however, critical for analysis results to be produced fast. To this end, incremental static analysis can be used. Upon a program change, an incremental analysis updates the previous results rather than recomputing the results from scratch.Incremental static analyses may suffer from cyclic reinforcement of lattice values, where the computation of some values within the analysis relies on the values themselves, due to the abstractions made by the analysis. This can cause the incremental analysis to produce less precise results, reducing its usability.In this work, we provide a solution to cyclic reinforcement of lattice values for incremental dependency-driven analyses. We compute the information flow within the analysis and show how this information flow can be used to detect cyclic reinforcements. We establish a criterion to detect when a cyclic reinforcement contains outdated information that needs to be removed, and show how precision can be regained. Our results show that using our method, an incremental analysis produces results matching a from-scratch analysis for all but one benchmark program, at the cost of a performance hit in some cases.

The WebAssembly standard aims to form a portable compilation target, enabling the cross-platform distribution of programs written in a variety of languages. This paper introduces and evaluates novel slicing approaches for WebAssembly, including dynamic and hybrid approaches. Given a program and a location in that program, a program slice is a reduced program that preserves the behavior at the given location. A static slice does so for all possible inputs, while a dynamic slice does so for a fixed set of inputs. Hybrid slicing is a combination of static and dynamic slicing. We build on Observational-Based Slicing (ORBS), where we explore the design space for instantiating ORBS for WebAssembly. For example, ORBS can be applied to the whole program or to only the function containing the slicing criterion, and it can be applied before compilation to WebAssembly or afterwards. We evaluate the slices produced using various options quantitatively and qualitatively. Our evaluation reveals that dynamic slicing at the level of a function from a WebAssembly binary finds a sweet spot in terms of slice time and slice size, and that a combination of static and dynamic slicers achieves the best trade-off in terms of slicing time and slice size.

Actor languages model concurrency as processes that communicate through asynchronous message sends. Unfortunately, as the complexity of these systems increases, it becomes more difficult to compose and integrate their components. This is because of assumptions made by components about their communication partners which may not be upheld when they remain implicit. In this paper, we bring design-by-contract programming to actor programs through a contract system that enables expressing constraints on receiver-related properties. Expressing properties about the expected receiver of a message, and about this receiver’s communication behavior, requires two novel types of contracts. Through their recursive structure, these contracts can govern entire communication chains. We implement the contract system for an actor extension of Scheme, describe it formally, and show how to assign blame in case of a contract violation. Finally, we prove our contract system and its blame assignment correct by formulating and proving a blame correctness theorem.

The recently introduced WebAssembly standard aims to form a portable compilation target, enabling the cross-platform distribution of programs written in a variety of languages. In this paper, we propose and investigate the first dynamic slicing approaches for WebAssembly. Given a program and a location in that program, a program slice is a reduced version of the program that preserves the behavior at the given location. Slicing has numerous applications in software maintenance and evolution, including reverse engineering, code comprehension, and quality assurance.Our dynamic approaches are built on Observational-Based Slicing (ORBS). We explore the design space for instantiating ORBS for WebAssembly: for example, it can be applied to the whole program or to only the function containing the slicing criterion, and it can be applied before compilation to WebAssembly or afterwards. We evaluate the slices produced quantitatively and qualitatively, and compare them to those obtained by a state-of-the-art static slicer for WebAssembly. Our evaluation reveals that dynamic slicing at the level of a function from a WebAssembly binary finds a sweet spot in terms of slice time and slice size.

WebAssembly has attracted great attention as a portable compilation target for programming languages. To facilitate in-depth studies about this technology, we have deployed Wasmizer, a tool that regularly mines GitHub projects and makes an up-to-date dataset of WebAssembly sources and their binaries publicly available. Presently, we have collected 2540 C and C++ projects that are highly-related to WebAssembly, and built a dataset of 8915 binaries that are linked to their source projects. To demonstrate an application of this dataset, we have investigated the presence of eight WebAssembly compilation smells in the wild.

Static analyses can be used by developers to compute properties of a program, enabling e.g., bug detection and program verification. However, reanalysing a program from scratch upon every change is time-consuming, especially in settings where code changes often, such as within IDEs. To avoid such full reanalyses, incremental analyses instead reuse parts of the previous analysis result, and reanalyse the changed code as necessary. While incrementality improves the analysis time, we introduce a complementary approach that further reduces the analysis time. A traditional incremental analysis updates previous analysis results without domain-specific knowledge. However, the effect of particular source code changes on analysis results can be predicted. Performing a traditional incremental analysis of the changed code might therefore be unnecessary. Instead, we propose to detect code change patterns of which the effect on analysis results can be predicted and to update these results accordingly, saving potentially expensive computations. In this paper, we explore the idea of adapting the analysis results for behaviour-preserving change patterns. In particular, we consider consistent renamings, inverted conditionals, and moved function definitions within Scheme programs. We implemented our approach and evaluated it on 30 programs. We show decreases in incremental analysis time between 3% and 99% on 25 programs that contain at least one behaviour-preserving change pattern.

The recently introduced WebAssembly standard aims to be a portable compilation target, enabling the cross-platform distribution of programs written in a variety of languages. We propose an approach to slice WebAssembly programs in order to enable applications in reverse engineering, code comprehension, and security among others. Given a program and a location in that program, program slicing produces a minimal version of the program that preserves the behavior at the given location. Specifically, our approach is a static, intra-procedural, backward slicing approach that takes into account WebAssembly-specific dependences to identify the instructions of the slice. To do so it must correctly overcome the considerable challenges of performing dependence analysis at the binary level. Furthermore, for the slice to be executable, the approach needs to ensure that the stack behavior of its output complies with WebAssembly's validation requirements. We implemented and evaluated our approach on a suite of 8 386 real-world WebAssembly binaries, finding that the average size of the 495 204 868 slices computed is 53% of the original code, an improvement over the 60% attained by related work slicing ARM binaries. To gain a more qualitative understanding of the slices produced by our approach, we compared them to 1 956 source-level slices of benchmark C programs. This inspection helps to illustrate the slicer's strengths and to uncover potential future improvements.

WebAssembly is a growing technology to build cross-platform applications. We aim to understand the security issues that developers encounter when adopting WebAssembly. We mined WebAssembly questions on Stack Overflow and identified 359 security-related posts. We classified these posts into 8 themes, reflecting developer intentions, and 19 topics, representing developer issues in this domain. We found that the most prevalent themes are related to bug fix support, requests for how to implement particular features, clarification questions, and setup or configuration issues. We noted that the topmost issues attribute to authentication in Blazor WebAssembly. We discuss six of them and provide our suggestions to clear these issues in practice.

Design-by-contract is a development best practice that requires the interactions between software components to be governed by precise specifications, called contracts. Contracts often take the form of pre- and post-conditions on function definitions, and are usually translated to (frequently redundant) run-time checks. So-called soft contract verifiers have been proposed to reduce the run-time overhead introduced by such contract checks by verifying parts of the contracts ahead of time, while leaving those that cannot be verified as residual run-time checks. In the state of the art, static analyses based on the Abstracting Abstract Machines (AAM) approach to abstract interpretation have been proposed for implementing such soft verifiers. However, these approaches result in whole-program analyses which are difficult to scale. In this paper, we propose a scalable summary-based compositional analysis for soft contract verification, which summarises both the correct behaviour and erroneous behaviour of all functions in the program using symbolic path conditions. Information from these summaries propagates backwards through the call graph, reducing the amount of redundant analysis states and improving the overall performance of the analysis. This backwards flow enables path constraints associated with erroneous program states to flow to call sites where they can be refuted, whereas in the state of the art they can only be refuted using the information available at the original location of the error. To demonstrate our improvements in both precision and performance compared to the state-of-the-art, we implemented our analysis in a framework called MAF (short for Modular Analysis Framework) — a framework for the analysis of higher-order dynamic programming languages. We conducted an empirical study and found an average performance improvement of 21%, and an average precision improvement of 38.15%.

WebAssembly is increasingly used as the compilation target for cross-platform applications. In this paper, we investigate whether one can rely on the security measures enforced by existing C compilers when compiling C programs to WebAssembly. We compiled 4,469 C programs with known buffer overflow vulnerabilities to x86 code and to WebAssembly, and observed the outcome of the execution of the generated code to differ for 1,088 programs. Through manual inspection, we identified that the root cause for these is the lack of security measures such as stack canaries in the generated WebAssembly: while x86 code crashes upon a stack-based buffer overflow, the corresponding WebAssembly continues to be executed. We conclude that compiling an existing C program to WebAssembly without additional precautions may hamper its security, and we encourage more research in this direction.

Program slicing aims to reduce a program to a minimal form that produces the same output for a given slicing criterion. Program slicing approaches divide into static and dynamic approaches: whereas static approaches generate an over-approximation of the slice that is valid for all possible program inputs, dynamic approaches rely on executing the program and thus generate an under-approximation of the slice that is valid for only a subset of the inputs. An important limitation of static approaches is that they often do not generate an executable program, but rather identify only those program components upon which the slicing criterion depends (referred to as a closure slice). In order to overcome this limitation, we propose a novel approach that combines static and dynamic slicing. We rely on observation-based slicing, a dynamic approach, but protect all statements that have been identified as part of the static slice by the static slicer CodeSurfer. As a result, we obtain slices that cover at least the behavior of the static slice, but that can be compiled and executed. We evaluated this new approach on a set of 57 C programs and report our preliminary findings.

A modular static analysis decomposes a program's analysis into analyses of its parts, or components. An intercomponent analysis instructs an intra-component analysis to analyse each component independently of the others. Additional analyses are scheduled for newly discovered components, and for dependent components that need to account for newly discovered component information. Modular static analyses are scalable, can be tuned to a high precision, and support the analysis of programs that are highly dynamic, featuring e.g., higher-order functions or dynamically allocated processes.In this paper, we present the engineering aspects of MAF, a static analysis framework for implementing modular analyses for higher-order languages. For any such modular analysis, the framework provides a reusable inter-component analysis and it suffices to implement its intra-component analysis. The intracomponent analysis can be composed from several interdependent and reusable Scala traits. This design facilitates changing the analysed language, as well as the analysis precision with minimal effort. We illustrate the use of MAF through its instantiation for several different analyses of Scheme programs.

One way to speed up static program analysis is to make use of today's multi-core CPUs by parallelising the analysis. Existing work on parallel analysis usually targets traditional data-How analyses for static, first-order languages such as C. Less attention has been given so far to the parallelisation of more general analyses that can also target dynamic, higherorder languages such as JavaScript. These are significantly more challenging to parallelise, as dependencies between analysis results are only discovered during the analysis itself. State-ofthe-art parallel analyses for such languages are therefore usually limited, both in their applicability and performance gains. In this work, we propose the parallelisation of modular analyses. Modular analyses compute different parts of the analysis in isolation of one another, and therefore offer inherent opportunities for parallelisation that have not been explored so far. In addition, they can be used to develop a general class of analysers for dynamic, higher-order languages. We present a parallel variant of the worklist algorithm that is used to drive such modular analyses. To further speed up its convergence, we show how this algorithm can exploit the monotonicity of the analysis. Existing modular analyses can be parallelised without additional effort by instead employing this parallel worklist algorithm. We demonstrate this for MODF, an inter-procedural modular analysis, and for MODCONC, an inter-process modular analysis. For MODCONC, we reveal an additional opportunity to exploit even more parallelism in the analysis. Our parallel worklist algorithm is implemented and integrated into MAF, a framework for modular program analysis. Using a set of Scheme benchmarks for MODF, we usually observe speedups between 3× and 8× when using 4 workers, and speedups between 8× and 32× when using 16 workers. For MODCONC, we achieve a maximum speedup of 15×.

Static analyses are used to gain more confidence in changes made by developers. To be of most use, such analyses must deliver feedback fast. Therefore, incremental static analyses update previous results rather than entirely recompute them. This reduces the analysis time upon a program change, and makes the analysis well-suited for environments where the code base is frequently updated, such as in IDEs and CI pipelines.In this work, we present a general approach to render a modular static analysis for highly dynamic programs incremental, by exploiting dependencies between intermediate analysis results. Modular analyses divide a program in interdependent parts that are analysed in isolation. The dependencies between these parts stem, for example, from the use of shared variables within the program. Our incrementalisation approach leverages the modularity of the analysis together with the dependencies that it reifies to compute and bound the impact of changes. This way, only the affected parts of the result need to be reanalysed, and unnecessary recomputations are avoided.We apply our approach to both a function-modular and a thread-modular analysis and evaluate it by comparing an incremental update of an existing result to a full reanalysis. We find reductions of the analysis time from 6% to 99% on 14 out of 16 benchmark programs, and on most programs the impact on precision is limited. On 7 of the programs, reanalysis time is reduced by more than 75%, showing that our approach results in fast incremental updates.

WebAssembly is a new W3C standard, providing a portable target for compilation for various languages. All major browsers can run WebAssembly programs, and its use extends beyond the web: there is interest in compiling cross-platform desktop applications, server applications, IoT and embedded applications to WebAssembly because of the performance and security guarantees it aims to provide. Indeed, WebAssembly has been carefully designed with security in mind. In particular, WebAssembly applications are sandboxed from their host environment. However, recent works have brought to light several limitations that expose WebAssembly to traditional attack vectors. Visitors of websites using WebAssembly have been exposed to malicious code as a result. In this paper, we propose an automated static program analysis to address these security concerns. Our analysis is focused on information flow and is compositional. For every WebAssembly function, it first computes a summary that describes in a sound manner where the information from its parameters and the global program state can flow to. These summaries can then be applied during the subsequent analysis of function calls. Through a classical fixed-point formulation, one obtains an approximation of the information flow in the WebAssembly program. This results in the first compositional static analysis for WebAssembly. On a set of 34 benchmark programs spanning 196kLOC of WebAssembly, we compute at least 64% of the function summaries precisely in less than a minute in total.

Modern programming languages support concurrent programming based on channels and processes. Channels enable synchronous and asynchronous message-passing between independent light-weight processes making it easy to express common concurrency patterns. The implementation of channels and processes in compilers and language runtimes is a difficult task that relies heavily on traditional and error-prone low-level concurrency primitives, raising concerns about correctness and reliability. In this paper, we present an automatic program generation technique to test such programming language implementations. We define a type and effect system for programs that communicate over channels and where every execution is guaranteed to eventually terminate. We can generate and run such programs, and if a program fails to terminate, we have found a bug in the programming language implementation. We implement such an automatic program generator and apply it to Go, Kotlin, Crystal, and Flix. We find two new bugs in Flix, and reproduce two bugs; one in Crystal and one in Kotlin.

Abstract garbage collection is the application of garbage collection to an abstract interpreter. Existing work has shown that abstract garbage collection can improve both the interpreter’s precision and performance. Current approaches rely on heuristics to decide when to apply abstract garbage collection. Garbage will build up and impact precision and performance when the collection is applied infrequently, while too frequent applications will bring about their own performance overhead. A balance between these tradeoffs is often difficult to strike. We propose a new approach to cope with the buildup of garbage in the results of an abstract interpreter. Our approach is able to eliminate all garbage, therefore obtaining the maximum precision and performance benefits of abstract garbage collection. At the same time, our approach does not require frequent heap traversals, and therefore adds little to the interpreters’s running time. The core of our approach uses reference counting to detect and eliminate garbage as soon as it arises. However, reference counting cannot deal with cycles, and we show that cycles are much more common in an abstract interpreter than in its concrete counterpart. To alleviate this problem, our approach detects cycles and employs reference counting at the level of strongly connected components. While this technique in general works for any system that uses reference counting, we argue that it works particularly well for an abstract interpreter. In fact, we show formally that for the continuation store, where most of the cycles occur, the cycle detection technique only requires O(1) amortized operations per continuation push. We present our approach formally, and provide a proof-of-concept implementation in the Scala-AM framework. We empirically show our approach achieves both the optimal precision and significantly better performance compared to existing approaches to abstract garbage collection.

Properties such as the absence of errors or bounds on mailbox sizes are hard to deduce statically for actor-based programs. This is because actor-based programs exhibit several sources of unboundedness, in addition to the non-determinism that is inherent to the concurrent execution of actors. We developed a static technique based on abstract interpretation to soundly reason in a finite amount of time about the possible executions of an actor-based program. We use our technique to statically verify the absence of errors in actor-based programs, and to compute upper bounds on the actors' mailboxes. Sound abstraction of these mailboxes is crucial to the precision of any such technique. We provide several mailbox abstractions and categorize them according to the extent to which they preserve message ordering and multiplicity of messages in a mailbox. We formally prove the soundness of each mailbox abstraction, and empirically evaluate their precision and performance trade-offs on a corpus of benchmark programs. The results show that our technique can statically verify the absence of errors for more benchmark programs than the state-of-the-art analysis.

This paper presents the implementation of an efficient interpreter for a Scheme-like language using manually written asm.js code. The asm.js specification defines an optimizable subset of JavaScript that has already served well as a compilation target for web applications where performance is critical. However, its usage as a human-writable language that can be integrated into existing projects to improve performance has remained largely unexplored. We therefore apply this strategy to optimize the implementation of an interpreter. We also discuss the feasibility of this approach, as writing asm.js by hand is generally not its recommended use-case. We therefore present a macro system to solve the challenges we encounter. The resulting interpreter is compared to the original C implementation and its compiled equivalent in asm.js. This way, we evaluate whether manual integration with asm.js provides the necessary performance to bring larger applications and runtimes to the web. We also refactor our implementation to assess how more JavaScript code can cohabit with asm.js code, improving maintainability of the implementation while preserving near-native performance. In the case of our interpreter, this improved maintainability enables adding more complex optimizations. We investigate the addition of function inlining , for which we validate the performance gain.

Abstract We present a static analysis for determining whether and to what extent functions in JavaScript programs are pure. To this end, the analysis classifies functions as pure functions, observers, or procedures. A function is pure if none of its executions generate or depend upon externally observable side effects. A function is an observer as soon as one of its executions depends on an external side effect, but none of its executions generate observable side effects. Otherwise, the function is classified as a procedure. Function executions and associated callers are found by traversing all reachable function execution contexts on the call stack at the point where an effect occurs. Our approach is based on a flow analysis that, in addition to computing traditional control and value flow, keeps track of read and write effects. To increase the precision of our purity analysis, we combine it with an intraprocedural analysis that determines freshness of variables and objects. We formalize the core aspects of our technique and discuss its implementation and results on common JavaScript benchmarks. Results show that our approach is capable of determining function purity in the presence of higher‐order functions, dynamic property expressions, and prototypal inheritance. When compared with existing purity analyses, we find that our approach is as precise or more precise than the existing analyses.

We present Scala-AM, a modular framework for static analysis based on systematic abstraction of abstract machines. Scala-AM achieves modularity by separating operational semantics, abstract values and machine abstraction concerns via actions, thus enabling language designers, static analysis developers and machine abstraction experts to combine their efforts. This modularity enables us to support semantics for multiple languages, and to include multiple machine abstractions in our framework. Different operational semantics and machine abstractions can then be combined with minimal effort. We evaluate our framework by demonstrating how it enables implementing machine abstractions independently of the operational semantics, and by instantiating the framework for a static taint analysis of Scheme.

Few static analyses support concurrent higher-order programs. Tools for detecting concurrency bugs such as deadlocks and race conditions are nonetheless invaluable to developers. Concurrency can be implemented using a variety of models, each supported by different synchronization primitives. Using this poster, we present an approach for analyzing concurrent higher-order programs in a precise manner through abstract interpretation. We instantiate the approach for two static analyses that are capable of detecting deadlocks and race conditions in programs that rely either on compare-and-swap (cas), or on conventional locks for synchronization. We observe few false positives and false negatives on a corpus of small concurrent programs, with better results for the lock-based analyses. We also observe that these programs lead to a smaller state space to be explored by the analyses. Our results show that the choice of synchronization primitives supported by an abstract interpreter has an important impact on the complexity of the static analyses performed with this abstract interpreter.

Manually detecting bugs in concurrent programs is hard due to the myriad of thread interleavings that needs to be accounted for. Higher-order programming features only exacerbate this difficulty. The need for tool support therefore increases as these features become more widespread. We investigate the P(CEK*)S abstract machine as the foundation for tool support for detecting concurrency bugs. This abstract interpreter analyzes multi-threaded, higher-order programs with shared-store concurrency and a compare-and-swap synchronization primitive. In this paper, we evaluate two different approaches to reduce the size of the state space explored by the abstract interpreter. First, we integrate abstract garbage collection into the abstract interpreter, and we observe that it does not reduce the state space as expected. We then evaluate the impact of adding first-class support for locks on the machine's client analyses. To this end, we compare a cas-based and a lock-based formulation of race condition and deadlock detection analyses. We show that adding first-class support for locks not only significantly reduces the number of abstract program states that need to be explored, but also simplifies formulating the client analyses.