Ownership in low-level intermediate representation

• URL: http://arxiv.org/abs/2408.04043v3
• Date: Tue, 13 Aug 2024 13:31:34 GMT
• Title: Ownership in low-level intermediate representation
• Abstract summary: The concept of ownership in high level languages can aid both the programmer and the compiler to reason about the validity of memory operations. We develop ownership semantics for an LLVM like low level intermediate representation. We implement these semantics in SEABMC, a bit precise bounded model checker for LLVM.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The concept of ownership in high level languages can aid both the programmer and the compiler to reason about the validity of memory operations. Previously, ownership semantics has been used successfully in high level automatic program verification to model a reference to data by a first order logic (FOL) representation of data instead of maintaining an address map. However, ownership semantics is not used in low level program verification. We have identified two challenges. First, ownership information is lost when a program is compiled to a low level intermediate representation (e.g., in LLVM IR). Second, pointers in low level programs point to bytes using an address map (e.g., in unsafe Rust) and thus the verification condition (VC) cannot always replace a pointer by its FOL abstraction. To remedy the situation, we develop ownership semantics for an LLVM like low level intermediate representation. Using these semantics, the VC can opportunistically model some memory accesses by a direct access of a pointer cache that stores byte representation of data. This scheme reduces instances where an address map must be maintained, especially for mostly safe programs that follow ownership semantics. For unsafe functionality, memory accesses are modelled by operations on an address map and we provide mechanisms to keep the address map and pointer cache in sync. We implement these semantics in SEABMC, a bit precise bounded model checker for LLVM. For evaluation, the source programs are assumed to be written in C. Since C does not have ownership built in, suitable macros are added that introduce and preserve ownership during translation to LLVM like IR for verification. This approach is evaluated on mature open source C code. For both handcrafted benchmarks and practical programs, we observe a speedup of $1.3x-5x$ during SMT solving.

Related papers

• PTSan: A Practical Memory Safety Sanitizer for C/C++ with Pointer-Object Authority [0.0]
  PTSan makes pointer-based checking practical by an object identifier in each pointer's high bits and its bounds in a fixed-size runtime table.<n> PTSan runs at parity with the fastest published location-based sanitizer.
  arXiv  Detail & Related papers  (2026-07-21T16:16:27Z)
• Reconsidering "Reconsidering Custom Memory Allocation" [0.0]
  25 years ago, Berger et al. showed that per-class allocators provide no significant speedups over a state-of-the-art general-purpose allocator.<n>This paper revisits that work on a modern hardware platform with modern general-purpose allocators to evaluate whether their conclusions still hold.<n>It introduces a methodology to explore the effect of memory fragmentation on locality in general-purpose allocators.
  arXiv  Detail & Related papers  (2026-05-16T18:52:50Z)
• LLM4C2Rust: Large Language Models for Automated Memory-Safe Code Transpilation [1.4490522938516996]
  Rust, one of the youngest modern programming languages, offers built-in memory-safety guarantees.<n>Transpiling C/C++ code into memory-safe Rust code has become a growing area of research.<n>We propose a Retrieval-Augmented Generation (RAG)-assisted framework to perform C/C++-to-Rust transpilation.
  arXiv  Detail & Related papers  (2026-04-16T19:33:44Z)
• Memory Transfer Learning: How Memories are Transferred Across Domains in Coding Agents [56.078070829341534]
  Memory-based self-evolution has emerged as a promising paradigm for coding agents.<n>We investigate textbfMemory Transfer Learning (MTL) by harnessing a unified memory pool from heterogeneous domains.
  arXiv  Detail & Related papers  (2026-04-15T15:50:29Z)
• Fast SAM2 with Text-Driven Token Pruning [52.8350457627401]
  Segment Anything Model 2 (SAM2), a vision computation model has significantly advanced in prompt-driven video object segmentation.<n>SAM2 pipelines propagate all visual tokens produced by the image encoder through downstream temporal reasoning modules, regardless of their relevance to the target object.<n>We introduce a text-guided token pruning framework that improves inference efficiency by selectively reducing token density prior to temporal propagation.
  arXiv  Detail & Related papers  (2025-12-24T18:59:05Z)
• SK2Decompile: LLM-based Two-Phase Binary Decompilation from Skeleton to Skin [17.843213826367343]
  We introduce SK2Decompile, a novel two-phase approach to decompile from the skeleton (semantic structure) to the skin (identifier) of programs.<n>Specifically, we first apply a Structure Recovery model to translate a program's binary code to an Intermediate Representation (IR) as deriving the program's "skeleton"<n>We apply reinforcement learning to reward the model for producing program structures that adhere to the syntactic and semantic rules expected by compilers.
  arXiv  Detail & Related papers  (2025-09-26T09:35:46Z)
• Tracing Errors, Constructing Fixes: Repository-Level Memory Error Repair via Typestate-Guided Context Retrieval [9.737526306478598]
  This paper introduces LTFix, a novel approach that harnesses the potential of Large Language Models (LLMs) for automated memory error repair.<n>Our approach utilizes a finite typestate automaton to guide the tracking of error-propagation paths and context trace, capturing both spatial (memory states) and temporal (execution history) dimensions of error behavior.
  arXiv  Detail & Related papers  (2025-06-23T08:30:00Z)
• Unlocking the Power of SAM 2 for Few-Shot Segmentation [54.562050590453225]
  Few-Shot (FSS) aims to learn class-agnostic segmentation on few classes to segment arbitrary classes, but at the risk of overfitting.<n>Recently, SAM 2 has extended SAM by supporting video segmentation, whose class-agnostic matching ability is useful to FSS.<n>We design Pseudo Prompt Generator to encode pseudo query memory, matching with query features in a compatible way.<n>We further design Iterative Memory Refinement to fuse more query FG features into the memory, and devise a Support-Calibrated Memory Attention to suppress the unexpected query BG features in memory.
  arXiv  Detail & Related papers  (2025-05-20T09:02:53Z)
• MIB: A Mechanistic Interpretability Benchmark [77.35046700898326]
  We propose MIB, a benchmark with two tracks spanning four tasks and five models. Using MIB, we find that attribution and mask optimization methods perform best on circuit localization. For causal variable localization, we find that the supervised DAS method performs best, while SAE features are not better than neurons.
  arXiv  Detail & Related papers  (2025-04-17T17:55:45Z)
• EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
  We introduce EquiBench, a new benchmark for evaluating large language models (LLMs)<n>This task directly tests a model's ability to reason about program semantics.<n>We evaluate 19 state-of-the-art LLMs and find that in the most challenging categories, the best accuracies are 63.8% and 76.2%, only modestly above the 50% random baseline.
  arXiv  Detail & Related papers  (2025-02-18T02:54:25Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  The goal of decompilation is to convert compiled low-level code (e.g., assembly code) back into high-level programming languages. This task supports various reverse engineering applications, such as vulnerability identification, malware analysis, and legacy software migration.
  arXiv  Detail & Related papers  (2025-02-17T12:38:57Z)
• FUSELOC: Fusing Global and Local Descriptors to Disambiguate 2D-3D Matching in Visual Localization [57.59857784298536]
  Direct 2D-3D matching algorithms require significantly less memory but suffer from lower accuracy due to the larger and more ambiguous search space. We address this ambiguity by fusing local and global descriptors using a weighted average operator within a 2D-3D search framework. We consistently improve the accuracy over local-only systems and achieve performance close to hierarchical methods while halving memory requirements.
  arXiv  Detail & Related papers  (2024-08-21T23:42:16Z)
• Host-Based Allocators for Device Memory [1.2289361708127877]
  We pose a model where the allocation algorithm runs on host memory but allocates device memory and so incur the following constraint: the allocator can't read the memory it is allocating. This means we are unable to use boundary tags, which is a concept that has been ubiquitous in nearly every allocation algorithm. In this paper, we propose alternate algorithms to work around this constraint, and discuss in general the implications of this system model.
  arXiv  Detail & Related papers  (2024-05-11T19:28:37Z)
• Enabling Memory Safety of C Programs using LLMs [5.297072277460838]
  Memory safety violations in low-level code, written in languages like C, continue to remain one of the major sources of software vulnerabilities. One method of removing such violations by construction is to port C code to a safe C dialect. Such dialects rely on programmer-supplied annotations to guarantee safety with minimal runtime overhead. This porting is a manual process that imposes significant burden on the programmer and hence, there has been limited adoption of this technique.
  arXiv  Detail & Related papers  (2024-04-01T13:05:54Z)
• SeMalloc: Semantics-Informed Memory Allocator [18.04397502953383]
  Use-after-free (UAF) is a critical and prevalent problem in memory unsafe languages. We show one way to balance the trinity by passing more semantics about the heap object to the allocator. In SeMalloc, only heap objects allocated from the same call site and via the same function call stack can possibly share a virtual memory address.
  arXiv  Detail & Related papers  (2024-02-02T21:02:15Z)
• A Semantic Space is Worth 256 Language Descriptions: Make Stronger Segmentation Models with Descriptive Properties [53.177550970052174]
  ProLab is a novel approach using property-level label space for creating strong interpretable segmentation models. It uses descriptive properties grounded in common sense knowledge for supervising segmentation models.
  arXiv  Detail & Related papers  (2023-12-21T11:43:41Z)
• CRIL: A Concurrent Reversible Intermediate Language [0.0]
  We present a reversible intermediate language with composing for translating a high-level concurrent programming language to another lower-level concurrent programming language, keeping reversibility. We propose CRIL as an extension of RIL used by Mogensen for a functional reversible language, incorporating a multi-thread process invocation and the synchronization primitives based on the P-V operations.
  arXiv  Detail & Related papers  (2023-09-13T20:52:54Z)
• rCanary: Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust [4.616001680122352]
  Rust is a system programming language that guarantees memory safety via compile-time verifications. We present rCanary, a static, non-automated, and fully automated model checker to detect leaks across semiautomated boundary.
  arXiv  Detail & Related papers  (2023-08-09T08:26:04Z)
• Side Adapter Network for Open-Vocabulary Semantic Segmentation [69.18441687386733]
  This paper presents a new framework for open-vocabulary semantic segmentation with the pre-trained vision-language model, named Side Adapter Network (SAN) A side network is attached to a frozen CLIP model with two branches: one for predicting mask proposals, and the other for predicting attention bias. Our approach significantly outperforms other counterparts, with up to 18 times fewer trainable parameters and 19 times faster inference speed.
  arXiv  Detail & Related papers  (2023-02-23T18:58:28Z)
• Learning Implicit Feature Alignment Function for Semantic Segmentation [51.36809814890326]
  Implicit Feature Alignment function (IFA) is inspired by the rapidly expanding topic of implicit neural representations. We show that IFA implicitly aligns the feature maps at different levels and is capable of producing segmentation maps in arbitrary resolutions. Our method can be combined with improvement on various architectures, and it achieves state-of-the-art accuracy trade-off on common benchmarks.
  arXiv  Detail & Related papers  (2022-06-17T09:40:14Z)
• How could Neural Networks understand Programs? [67.4217527949013]
  It is difficult to build a model to better understand programs, by either directly applying off-the-shelf NLP pre-training techniques to the source code, or adding features to the model by theshelf. We propose a novel program semantics learning paradigm, that the model should learn from information composed of (1) the representations which align well with the fundamental operations in operational semantics, and (2) the information of environment transition.
  arXiv  Detail & Related papers  (2021-05-10T12:21:42Z)
• Kanerva++: extending The Kanerva Machine with differentiable, locally block allocated latent memory [75.65949969000596]
  Episodic and semantic memory are critical components of the human memory model. We develop a new principled Bayesian memory allocation scheme that bridges the gap between episodic and semantic memory. We demonstrate that this allocation scheme improves performance in memory conditional image generation.
  arXiv  Detail & Related papers  (2021-02-20T18:40:40Z)

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.