C Analyzer : A Static Program Analysis Tool for C Programs
- URL: http://arxiv.org/abs/2403.12973v1
- Date: Sun, 28 Jan 2024 11:43:16 GMT
- Title: C Analyzer : A Static Program Analysis Tool for C Programs
- Authors: Rajendra Kumar Solanki,
- Abstract summary: C Analyzer is a tool developed for static analysis of C programs.
This project work tries to leverage Abstract Interpretation techniques for static analysis of C programs.
- Score: 0.0
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: In our times, when the world is increasingly becoming more dependent on software programs, writing bug-free, correct programs is crucial. Program verification based on formal methods can guarantee this by detecting run-time errors in safety-critical systems to avoid possible adverse impacts on human life and save time and money. This project work tries to leverage Abstract Interpretation techniques for static analysis of C programs. C Analyzer is a tool developed for static analysis of C programs. This implementation of C Analyzer provides a plug-and-play domain architecture for multiple abstract domains to be used. C Analyzer supports four abstract domains - Interval, Octagon, Polyhedra, and Bit Vector. We use these different domains for required precision in program verification. C Analyzer tool uses LLVM C/C++ compiler frontend Clang API to generate and traverse the Control Flow Graph (CFG) of a given C program. This tool generates invariants in different abstract domains for statements in basic blocks of CFG during CFG traversal. Using these invariants, some properties of a program, such as dividing by zero, modulus zero, arithmetic overflow, etc., can be analyzed. We also use a source-to-source transformation tool, CIL (Common Intermediate language), to transform some C constructs into simpler constructs, such as transforming logical operators, switch statements, and conditional operators into if-else ladders and transforming do-while and for loops into while loops. Using C Analyzer, C program constructs such as declarations, assignments, binary operations (arithmetic, relational, bitwise shift, etc.), conditions (if-else), loops (while, do while, for loop), nested conditions, and nested loops can be analyzed. Currently, this tool does not support arrays, structures, unions, pointers, or function calls.
Related papers
- FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
We propose a novel framework called FoC to Figure out the Cryptographic functions in stripped binaries.
FoC-BinLLM outperforms ChatGPT by 14.61% on the ROUGE-L score.
FoC-Sim outperforms the previous best methods with a 52% higher Recall@1.
arXiv Detail & Related papers (2024-03-27T09:45:33Z) - Accurate Coverage Metrics for Compiler-Generated Debugging Information [0.0]
Many tools rely on compiler-produced metadata to present a source-language view of program states.
Current approaches for measuring the extent of coverage of local variables are based on crude assumptions.
We propose some new metrics, computable by our tools, which could serve as motivation for language implementations to improve debug quality.
arXiv Detail & Related papers (2024-02-07T13:01:28Z) - LLVM Static Analysis for Program Characterization and Memory Reuse
Profile Estimation [0.0]
This paper presents an LLVM-based probabilistic static analysis method.
It accurately predicts different program characteristics and estimates the reuse distance profile of a program.
The results show that our approach can predict application characteristics accurately compared to another LLVM-based dynamic code analysis tool, Byfl.
arXiv Detail & Related papers (2023-11-20T23:05:06Z) - A Compiler from Array Programs to Vectorized Homomorphic Encryption [1.6216324006136673]
Homomorphic encryption (HE) is a practical approach to secure computation over encrypted data.
We present Viaduct-HE, a compiler generates efficient vectorized HE programs.
Viaduct-HE can generate both the operations and complex data layouts required for efficient HE programs.
arXiv Detail & Related papers (2023-11-10T16:00:00Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
Learned transpilation offers an alternative to manual re-writing and engineering efforts.
Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness.
Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
arXiv Detail & Related papers (2023-09-25T15:42:18Z) - C-rusted: The Advantages of Rust, in C, without the Disadvantages [0.0]
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.
The (partially) annotated C programs can be translated with unmodified versions of any compilation toolchain capable of processing ISO C code.
arXiv Detail & Related papers (2023-02-10T15:48:09Z) - Structural Analysis of Branch-and-Cut and the Learnability of Gomory
Mixed Integer Cuts [88.94020638263467]
The incorporation of cutting planes within the branch-and-bound algorithm, known as branch-and-cut, forms the backbone of modern integer programming solvers.
We conduct a novel structural analysis of branch-and-cut that pins down how every step of the algorithm is affected by changes in the parameters defining the cutting planes added to the input integer program.
Our main application of this analysis is to derive sample complexity guarantees for using machine learning to determine which cutting planes to apply during branch-and-cut.
arXiv Detail & Related papers (2022-04-15T03:32:40Z) - Searching for More Efficient Dynamic Programs [61.79535031840558]
We describe a set of program transformations, a simple metric for assessing the efficiency of a transformed program, and a search procedure to improve this metric.
We show that in practice, automated search can find substantial improvements to the initial program.
arXiv Detail & Related papers (2021-09-14T20:52:55Z) - Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
We introduce a technique for representing partially written programs in a program synthesis engine.
We learn an approximate execution model implemented as a modular neural network.
We show that these hybrid neuro-symbolic representations enable execution-guided synthesizers to use more powerful language constructs.
arXiv Detail & Related papers (2020-12-23T20:40:18Z) - Deep Data Flow Analysis [14.583644439728895]
ProGraML is a portable representation of whole-program semantics for deep learning.
We benchmark current and future learning techniques for compiler analyses.
We show that, using ProGraML, standard analyses can be learned and improved performance on downstream compiler optimization tasks.
arXiv Detail & Related papers (2020-11-21T03:29:14Z) - Extending C++ for Heterogeneous Quantum-Classical Computing [56.782064931823015]
qcor is a language extension to C++ and compiler implementation that enables heterogeneous quantum-classical programming, compilation, and execution in a single-source context.
Our work provides a first-of-its-kind C++ compiler enabling high-level quantum kernel (function) expression in a quantum-language manner.
arXiv Detail & Related papers (2020-10-08T12:49:07Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.