arXiv subjects

Roberto Bagnara

Publications and source records attributed to Roberto Bagnara.

At least 19 recordsLinked to original sources

arXiv2024

The ACPATH Metric: Precise Estimation of the Number of Acyclic Paths in C-like Languages

NPATH is a metric introduced by Brian A. Nejmeh in [13] that is aimed at overcoming some important limitations of McCabe's cyclomatic complexity. Despite the fact that the declared NPATH objective is to count the number of acyclic execution paths through a function, the definition given for the C language in [13] fails to do so even for very simple programs. We show that counting the number of acyclic paths in CFG is unfeasible in general. Then we define a new metric for C-like languages, called ACPATH, that allows to quickly compute a very good estimation of the number of acyclic execution paths through the given function. We show that, if the function body does not contain backward gotos and does not contain jumps into a loop from outside the loop, then such estimation is actually exact.

cs.SE↗

arXiv2023

C-rusted: The Advantages of Rust, in C, without the Disadvantages

C-rusted is an innovative technology whereby C programs can be (partly) annotated so as to express: ownership, exclusivity and shareability of language, system and user-defined resources; dynamic properties of objects and the way they evolve during program execution; nominal typing and subtyping. The (partially) annotated C programs can be translated with unmodified versions of any compilation toolchain capable of processing ISO C code. The annotated C program parts can be validated by static analysis: if the static analyzer flags no error, then the annotations are provably coherent among themselves and with respect to annotated C code, in which case said annotated parts are provably exempt from a large class of logic, security, and run-time errors.

cs.PL↗

arXiv2022

Coding Guidelines and Undecidability

The C and C++ programming languages are widely used for the implementation of software in critical systems. They are complex languages with subtle features and peculiarities that might baffle even the more expert programmers. Hence, the general prescription of language subsetting, which occurs in most functional safety standards and amounts to only using a "safer" subset of the language, is particularly applicable to them. Coding guidelines are the preferred way of expressing language subsets. Some guidelines are formulated in terms of the programming language and its implementation only: in this case they are amenable to automatic checking. However, due to fundamental limitations of computing, some guidelines are undecidable, that is, they are based on program properties that no current and future algorithm can capture in all cases. The most mature and widespread coding standards, the MISRA ones, explicitly tag guidelines with undecidable or decidable. It turns out that this information is not of secondary nature and must be taken into account for a full understanding of what the guideline is asking for. As a matter of fact, undecidability is a common source of confusion affecting many users of coding standards and of the associated checking tools. In this paper, we recall the notions of decidability and undecidability in terms that are understandable to any C/C++ programmer. The paper includes a systematic study of all the undecidable MISRA C:2012 guidelines, discussing the reasons for the undecidability and its consequences. We pay particular attention to undecidable guidelines that have decidable approximations whose enforcement would not overly constrain the source code. We also discuss some coding guidelines for which compliance is hard, if not impossible, to prove, even beyond the issue of decidability.

cs.PL↗

arXiv2021

A Rationale-Based Classification of MISRA C Guidelines

MISRA C is the most authoritative language subset for the C programming language that is a de facto standard in several industry sectors where safety and security are of paramount importance. While MISRA C is currently encoded in 175 guidelines (coding rules and directives), it does not coincide with them: proper adoption of MISRA C requires embracing its preventive approach (as opposed to the "bug finding" approach) and a documented development process where justifiable non-compliances are authorized and recorded as deviations. MISRA C guidelines are classified along several axes in the official MISRA documents. In this paper, we add to these an orthogonal classification that associates guidelines with their main rationale. The advantages of this new classification are illustrated for different kinds of projects, including those not (yet) having MISRA compliance among their objectives.

cs.PL↗

arXiv2021

Correct Approximation of IEEE 754 Floating-Point Arithmetic for Program Verification

Verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities of floating-point arithmetic: rounding errors, infinities, non-numeric objects (NaNs), signed zeroes, denormal numbers, different rounding modes, etc. One possibility to reason about floating-point arithmetic is to model a program computation path by means of a set of ternary constraints of the form z = x op y and use constraint propagation techniques to infer new information on the variables' possible values. In this setting, we define and prove the correctness of algorithms to precisely bound the value of one of the variables x, y or z, starting from the bounds known for the other two. We do this for each of the operations and for each rounding mode defined by the IEEE 754 binary floating-point standard, even in the case the rounding mode in effect is only partially known. This is the first time that such so-called filtering algorithms are defined and their correctness is formally proved. This is an important slab for paving the way to formal verification of programs that use floating-point arithmetics.

cs.PL↗

arXiv2020

A Practical Approach to Interval Refinement for math.h/cmath Functions

Verification of C++ programs has seen considerable progress in several areas, but not for programs that use these languages' mathematical libraries. The reason is that all libraries in widespread use come with no guarantees about the computed results. This would seem to prevent any attempt at formal verification of programs that use them: without a specification for the functions, no conclusion can be drawn statically about the behavior of the program. We propose an alternative to surrender. We introduce a pragmatic approach that leverages the fact that most math.h/cmath functions are almost piecewise monotonic: as we discovered through exhaustive testing, they may have glitches, often of very small size and in small numbers. We develop interval refinement techniques for such functions based on a modified dichotomic search, that enable verification via symbolic execution based model checking, abstract interpretation, and test data generation. Our refinement algorithms are the first in the literature to be able to handle non-correctly rounded function implementations, enabling verification in the presence of the most common implementations. We experimentally evaluate our approach on real-world code, showing its ability to detect or rule out anomalous behaviors.

cs.PL↗

arXiv2020

BARR-C:2018 and MISRA C:2012: Synergy Between the Two Most Widely Used C Coding Standards

The Barr Group's Embedded C Coding Standard (BARR-C:2018, which originates from the 2009 Netrino's Embedded C Coding Standard) is, for coding standards used by the embedded system industry, second only in popularity to MISRA C. However, the choice between MISRA C:2012 and BARR-C:2018 needs not be a hard decision since they are complementary in two quite different ways. On the one hand, BARR-C:2018 has removed all the incompatibilities with respect to MISRA C:2012 that were present in the previous edition (BARR-C:2013). As a result, disregarding programming style, BARR-C:2018 defines a subset of C that, while preventing a significant number of programming errors, is larger than the one defined by MISRA C:2012. On the other hand, concerning programming style, whereas MISRA C leaves this to individual organizations, BARR-C:2018 defines a programming style aimed primarily at minimizing programming errors. As a result, BARR-C:2018 can be seen as a first, dramatically useful step to C language subsetting that is suitable for all kinds of projects; critical projects can then evolve toward MISRA C:2012 compliance smoothly while maintaining the BARR-C programming style. In this paper, we introduce BARR-C:2018, we describe its relationship with MISRA C:2012, and we discuss the parallel and serial adoption of the two coding standards.

cs.PL↗

arXiv2019

That's C, baby. C!

Hardly a week goes by at BUGSENG without having to explain to someone that almost any piece of C text, considered in isolation, means absolutely nothing. The belief that C text has meaning in itself is so common, also among seasoned C practitioners, that I thought writing a short paper on the subject was a good time investment. The problem is due to the fact that the semantics of the C programming language is not fully defined: non-definite behavior, predefined macros, different library implementations, peculiarities of the translation process, . . . : all these contribute to the fact that no meaning can be assigned to source code unless full details about the build are available. The paper starts with an exercise that admits a solution. The existence of this solution will hopefully convince anyone that, in general, unless the toolchain and the build procedure are fully known, no meaning can be assigned to any nontrivial piece of C code.

cs.PL↗

arXiv2018

The MISRA C Coding Standard and its Role in the Development and Analysis of Safety- and Security-Critical Embedded Software

The MISRA project started in 1990 with the mission of providing world-leading best practice guidelines for the safe and secure application of both embedded control systems and standalone software. MISRA C is a coding standard defining a subset of the C language, initially targeted at the automotive sector, but now adopted across all industry sectors that develop C software in safety- and/or security-critical contexts. In this paper, we introduce MISRA C, its role in the development of critical software, especially in embedded systems, its relevance to industry safety standards, as well as the challenges of working with a general-purpose programming language standard that is written in natural language with a slow evolution over the last 40+ years. We also outline the role of static analysis in the automatic checking of compliance with respect to MISRA C, and the role of the MISRA C language subset in enabling a wider application of formal methods to industrial software written in C.

cs.PL↗

arXiv2017

MISRA C, for Security's Sake!

A third of United States new cellular subscriptions in Q1 2016 were for cars. There are now more than 112 million vehicles connected around the world. The percentage of new cars shipped with Internet connectivity is expected to rise from 13% in 2015 to 75% in 2020, and 98% of all vehicles will likely be connected by 2025. Moreover, the news continuously report about "white hat" hackers intruding on car software. For these reasons, security concerns in automotive and other industries have skyrocketed. MISRA C, which is widely respected as a safety-related coding standard, is equally applicable as a security-related coding standard. In this presentation, we will show that security-critical and safety-critical software have the same requirements. We will then introduce the new documents MISRA C:2012 Amendment 1 (Additional security guidelines for MISRA C:2012) and MISRA C:2012 Addendum 2 (Coverage of MISRA C:2012 against ISO/IEC TS 17961:2013 "C Secure Coding Rules"). We will illustrate the relationship between MISRA C, CERT C and ISO/IEC TS 17961, with a particular focus on the objective of preventing security vulnerabilities (and of course safety hazards) as opposed to trying to eradicate them once they have been inserted in the code.

cs.SE↗

arXiv2015

Exploiting Binary Floating-Point Representations for Constraint Propagation: The Complete Unabridged Version

Floating-point computations are quickly finding their way in the design of safety- and mission-critical systems, despite the fact that designing floating-point algorithms is significantly more difficult than designing integer algorithms. For this reason, verification and validation of floating-point computations is a hot research topic. An important verification technique, especially in some industrial sectors, is testing. However, generating test data for floating-point intensive programs proved to be a challenging problem. Existing approaches usually resort to random or search-based test data generation, but without symbolic reasoning it is almost impossible to generate test inputs that execute complex paths controlled by floating-point computations. Moreover, as constraint solvers over the reals or the rationals do not natively support the handling of rounding errors, the need arises for efficient constraint solvers over floating-point domains. In this paper, we present and fully justify improved algorithms for the propagation of arithmetic IEEE 754 binary floating-point constraints. The key point of these algorithms is a generalization of an idea by B. Marre and C. Michel that exploits a property of the representation of floating-point numbers.

cs.AI↗

arXiv2013

Eventual Linear Ranking Functions

Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for programming languages such as C and Java with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of declarative constraint programming. In this paper, we first recall an algorithm based on Farkas' Lemma for discovering linear ranking functions proving termination of a certain class of loops. Then we propose an extension of this method for showing the existence of eventual linear ranking functions, i.e., linear functions that become ranking functions after a finite unrolling of the loop. We show correctness and completeness of this algorithm.

cs.PL↗

arXiv2013

Proceedings of the 12th International Colloquium on Implementation of Constraint and LOgic Programming Systems

This volume contains the papers presented at CICLOPS'12: 12th International Colloquium on Implementation of Constraint and LOgic Programming Systems held on Tueseday September 4th, 2012 in Budapest. The program included 1 invited talk, 9 technical presentations and a panel discussion on Prolog open standards (open.pl). Each programme paper was reviewed by 3 reviewers. CICLOPS'12 continues a tradition of successful workshops on Implementations of Logic Programming Systems, previously held in Budapest (1993) and Ithaca (1994), the Compulog Net workshops on Parallelism and Implementation Technologies held in Madrid (1993 and 1994), Utrecht (1995) and Bonn (1996), the Workshop on Parallelism and Implementation Technology for (Constraint) Logic Programming Languages held in Port Jefferson (1997), Manchester (1998), Las Cruces (1999), and London (2000), and more recently the Colloquium on Implementation of Constraint and LOgic Programming Systems in Paphos (2001), Copenhagen (2002), Mumbai (2003), Saint Malo (2004), Sitges (2005), Seattle (2006), Porto (2007), Udine (2008), Pasadena (2009), Edinburgh (2010) - together with WLPE, Lexington (2011). We would like to thank all the authors, Tom Schrijvers for his invited talk, the programme committee members, and the ICLP 2012 organisers. We would like to also thank arXiv.org for providing permanent hosting.

cs.PL↗

arXiv2012

The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version

The classical technique for proving termination of a generic sequential computer program involves the synthesis of a ranking function for each loop of the program. Linear ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers.

cs.PL↗

arXiv2011

Coding Guidelines for Prolog

Coding standards and good practices are fundamental to a disciplined approach to software projects, whatever programming languages they employ. Prolog programming can benefit from such an approach, perhaps more than programming in other languages. Despite this, no widely accepted standards and practices seem to have emerged up to now. The present paper is a first step towards filling this void: it provides immediate guidelines for code layout, naming conventions, documentation, proper use of Prolog features, program development, debugging and testing. Presented with each guideline is its rationale and, where sensible options exist, illustrations of the relative pros and cons for each alternative. A coding standard should always be selected on a per-project basis, based on a host of issues pertinent to any given programming project; for this reason the paper goes beyond the mere provision of normative guidelines by discussing key factors and important criteria that should be taken into account when deciding on a fully-fledged coding standard for the project.

cs.PL↗

arXiv2009

Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions

Deciding whether the union of two convex polyhedra is itself a convex polyhedron is a basic problem in polyhedral computations; having important applications in the field of constrained control and in the synthesis, analysis, verification and optimization of hardware and software systems. In such application fields though, general convex polyhedra are just one among many, so-called, numerical abstractions, which range from restricted families of (not necessarily closed) convex polyhedra to non-convex geometrical objects. We thus tackle the problem from an abstract point of view: for a wide range of numerical abstractions that can be modeled as bounded join-semilattices --that is, partial orders where any finite set of elements has a least upper bound--, we show necessary and sufficient conditions for the equivalence between the lattice-theoretic join and the set-theoretic union. For the case of closed convex polyhedra --which, as far as we know, is the only one already studied in the literature-- we improve upon the state-of-the-art by providing a new algorithm with a better worst-case complexity. The results and algorithms presented for the other numerical abstractions are new to this paper. All the algorithms have been implemented, experimentally validated, and made available in the Parma Polyhedra Library.

cs.CG↗

arXiv2008

Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems

Convex polyhedra are the basis for several abstractions used in static analysis and computer-aided verification of complex and sometimes mission critical systems. For such applications, the identification of an appropriate complexity-precision trade-off is a particularly acute problem, so that the availability of a wide spectrum of alternative solutions is mandatory. We survey the range of applications of polyhedral computations in this area; give an overview of the different classes of polyhedra that may be adopted; outline the main polyhedral operations required by automatic analyzers and verifiers; and look at some possible combinations of polyhedra with other numerical abstractions that have the potential to improve the precision of the analysis. Areas where further theoretical investigations can result in important contributions are highlighted.

cs.CG↗

arXiv2007

A Prolog-based Environment for Reasoning about Programming Languages (Extended abstract)

ECLAIR is a Prolog-based prototype system aiming to provide a functionally complete environment for the study, development and evaluation of programming language analysis and implementation tools. In this paper, we sketch the overall structure of the system, outlining the main methodologies and technologies underlying its components. We also discuss the appropriateness of Prolog as the implementation language for the system: besides highlighting its strengths, we also point out a few potential weaknesses, hinting at possible solutions.

cs.PL↗