arXiv subjects

Qirun Zhang

Publications and source records attributed to Qirun Zhang.

6 recordsLinked to original sources

arXiv2025

Trajectory Densification and Depth from Perspective-based Blur

In the absence of a mechanical stabilizer, the camera undergoes inevitable rotational dynamics during capturing, which induces perspective-based blur especially under long-exposure scenarios. From an optical standpoint, perspective-based blur is depth-position-dependent: objects residing at distinct spatial locations incur different blur levels even under the same imaging settings. Inspired by this, we propose a novel method that estimate metric depth by examining the blur pattern of a video stream and dense trajectory via joint optical design algorithm. Specifically, we employ off-the-shelf vision encoder and point tracker to extract video information. Then, we estimate depth map via windowed embedding and multi-window aggregation, and densify the sparse trajectory from the optical algorithm using a vision-language model. Evaluations on multiple depth datasets demonstrate that our method attains strong performance over large depth range, while maintaining favorable generalization. Relative to the real trajectory in handheld shooting settings, our optical algorithm achieves superior precision and the dense reconstruction maintains strong accuracy.

cs.CV↗

arXiv2025

CRYPTONITE: Scalable Accelerator Design for Cryptographic Primitives and Algorithms

Cryptographic primitives, consisting of repetitive operations with different inputs, are typically implemented using straight-line C code due to traditional execution on CPUs. Computing these primitives is necessary for secure communication; thus, dedicated hardware accelerators are required in resource and latency-constrained environments. High-Level Synthesis (HLS) generates hardware from high-level implementations in languages like C, enabling the rapid prototyping and evaluation of designs, leading to its prominent use in developing dedicated hardware accelerators. However, directly synthesizing the straight-line C implementations of cryptographic primitives can lead to large hardware designs with excessive resource usage or suboptimal performance. We introduce Cryptonite, a tool that automatically generates efficient, synthesizable, and correct-by-design hardware accelerators for cryptographic primitives directly from straight-line C code. Cryptonite first identifies high-level hardware constructs through verified rewriting, emphasizing resource reuse. The second stage automatically explores latency-oriented implementations of the compact design. This enables the flexible scaling of a particular accelerator to meet the hardware requirements. We demonstrate Cryptonite's effectiveness using implementations from the Fiat Cryptography project, a library of verified and auto-generated cryptographic primitives for elliptic-curve cryptography. Our results show that Cryptonite achieves scalable designs with up to 88.88\% reduced resource usage and a 54.31\% improvement in latency compared to naively synthesized designs.

cs.AR↗

arXiv2024

A Note on Dynamic Bidirected Dyck-Reachability with Cycles

Recently, Li et al. [2022] presented a dynamic Dyck-reachability algorithm for bidirected graphs. The basic idea is based on updating edge weights in a data structure called the merged graph $G_m$. As noted in Krishna et al. [2023], the edge deletion procedure described in the algorithm of Li et al. [2022] cannot properly update the weights in the presence of cycles in $G_m$. This note discusses the cycle case and the time complexity.

cs.PL↗

arXiv2022

Static Inference Meets Deep Learning: A Hybrid Type Inference Approach for Python

Type inference for dynamic programming languages such as Python is an important yet challenging task. Static type inference techniques can precisely infer variables with enough static constraints but are unable to handle variables with dynamic features. Deep learning (DL) based approaches are feature-agnostic, but they cannot guarantee the correctness of the predicted types. Their performance significantly depends on the quality of the training data (i.e., DL models perform poorly on some common types that rarely appear in the training dataset). It is interesting to note that the static and DL-based approaches offer complementary benefits. Unfortunately, to our knowledge, precise type inference based on both static inference and neural predictions has not been exploited and remains an open challenge. In particular, it is hard to integrate DL models into the framework of rule-based static approaches. This paper fills the gap and proposes a hybrid type inference approach named HiTyper based on both static inference and deep learning. Specifically, our key insight is to record type dependencies among variables in each function and encode the dependency information in type dependency graphs (TDGs). Based on TDGs, we can easily integrate type inference rules in the nodes to conduct static inference and type rejection rules to inspect the correctness of neural predictions. HiTyper iteratively conducts static inference and DL-based prediction until the TDG is fully inferred. Experiments on two benchmark datasets show that HiTyper outperforms state-of-the-art DL models by exactly matching 10% more human annotations. HiTyper also achieves an increase of more than 30% on inferring rare types. Considering only the static part of HiTyper, it infers 2x ~ 3x more types than existing static type inference tools.

cs.SE↗

arXiv2021

Conditional Lower Bound for Inclusion-Based Points-to Analysis

Inclusion-based (i.e., Andersen-style) points-to analysis is a fundamental static analysis problem. The seminal work of Andersen gave a worst-case cubic $O(n^3)$ time points-to analysis algorithm for C, where $n$ is proportional to the number of program variables. An algorithm is truly subcubic if it runs in $O(n^{3-δ})$ time for some $δ> 0$. Despite decades of extensive effort on improving points-to analysis, the cubic bound remains unbeaten. The best combinatorial analysis algorithms have a "slightly subcubic" $O(n^3 / \text{log } n)$ complexity. It is an interesting open problem whether points-to analysis can be solved in truly subcubic time. In this paper, we prove that a truly subcubic $O(n^{3-δ})$ time combinatorial algorithm for inclusion-based points-to analysis is unlikely: a truly subcubic combinatorial points-to analysis algorithm implies a truly subcubic combinatorial algorithm for Boolean Matrix Multiplication (BMM). BMM is a well-studied problem, and no truly subcubic combinatorial BMM algorithm has been known. The fastest combinatorial BMM algorithms run in time $O(n^3/ \text{log}^4 n)$. Our result includes a simplified proof of the BMM-hardness of Dyck-reachability. The reduction is interesting in its own right. First, it is slightly stronger than the existing BMM-hardness results because our reduction only requires one type of parenthesis in Dyck-reachability ($D_1$-reachability). Second, we formally attribute the "cubic bottleneck" to the need to solve $D_1$-reachability, which captures the semantics of pointer references/dereferences. This new perspective enables a more general reduction that applies to programs with arbitrary pointer statements types. Last, our reduction based on $D_1$-reachability shows that demand-driven points-to analysis is as hard as the exhaustive counterpart.

cs.PL↗

arXiv2017

Skeletal Program Enumeration for Rigorous Compiler Testing

A program can be viewed as a syntactic structure P (syntactic skeleton) parameterized by a collection of the identifiers V (variable names). This paper introduces the skeletal program enumeration (SPE) problem: Given a fixed syntactic skeleton P and a set of variables V , enumerate a set of programs P exhibiting all possible variable usage patterns within P. It proposes an effective realization of SPE for systematic, rigorous compiler testing by leveraging three important observations: (1) Programs with different variable usage patterns exhibit diverse control- and data-dependence information, and help exploit different compiler optimizations and stress-test compilers; (2) most real compiler bugs were revealed by small tests (i.e., small-sized P) --- this "small-scope" observation opens up SPE for practical compiler validation; and (3) SPE is exhaustive w.r.t. a given syntactic skeleton and variable set, and thus can offer a level of guarantee that is absent from all existing compiler testing techniques. The key challenge of SPE is how to eliminate the enormous amount of equivalent programs w.r.t. $α$-conversion. Our main technical contribution is a novel algorithm for computing the canonical (and smallest) set of all non-$α$-equivalent programs. We have realized our SPE technique and evaluated it using syntactic skeletons derived from GCC's testsuite. Our evaluation results on testing GCC and Clang are extremely promising. In less than six months, our approach has led to 217 confirmed bug reports, 104 of which have already been fixed, and the majority are long latent bugs despite the extensive prior efforts of automatically testing both compilers (e.g., Csmith and EMI). The results also show that our algorithm for enumerating non-$α$-equivalent programs provides six orders of magnitude reduction, enabling processing the GCC test-suite in under a month.

cs.PL↗