SPARSE FUNCTIONAL STORES FOR IMPERATIVE PROGRAMS

被引:0
|
作者
STEENSGAARD, B
机构
来源
SIGPLAN NOTICES | 1995年 / 30卷 / 03期
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
In recent years, the trend in program representations for imperative programs has been to make them more functional, or to make them more sparse. However, new sparse representations have been non-functional, and new functional representations have not been sparse in the presence of pointer operations. In this paper, are present a functional representation that is sparse even in the presence of pointer operations. Conventionally, a store is represented in a functional program representation by a single object-typically a mapping from locations to values. We show how such a store object may be fragmented into several objects, each representing part of the store. The result is a sparser representation, which has not only the usual benefit of directly linking producers to consumers, but which also for static program analysis often leads to smaller domains of abstract Values for store objects. Store fragmentation corresponds to assignment factored SSA form (a factorization of SSA form introduced in this paper). We report on experiments with a thorough fragmentation based on a data flow points-to analysis and an intermediate level fragmentation based on an almost linear time complexity points-to analysis by type inference.
引用
收藏
页码:62 / 70
页数:9
相关论文
共 50 条
  • [31] An Integrated Proof Language for Imperative Programs
    Zee, Karen
    Kuncak, Viktor
    Rinard, Martin C.
    [J]. ACM SIGPLAN NOTICES, 2009, 44 (06) : 338 - 351
  • [32] Replicated Synchronization for Imperative BSP Programs
    Jakobsson, Arvid
    Dabrowski, Frederic
    Bousdira, Wadoud
    Loulergue, Frederic
    Hains, Gaetan
    [J]. INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE (ICCS 2017), 2017, 108 : 535 - 544
  • [33] Reasoning About Imperative Quantum Programs
    Chadha, R.
    Mateus, P.
    Sernadas, A.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 158 : 19 - 39
  • [34] On the representation of imperative programs in a logical framework
    Nistal, Jose Luis Freire
    Branas, Enrique Freire
    Ferro, Antonio Blanco
    Souto, David Cabrero
    [J]. COMPUTER AIDED SYSTEMS THEORY- EUROCAST 2007, 2007, 4739 : 202 - 209
  • [35] Rewriting of imperative programs into logical equations
    Ponsini, O
    Fédèle, C
    Kounalis, E
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2005, 56 (03) : 363 - 401
  • [36] Logical synthesis of imperative OO programs
    Bellot, P
    Robinet, B
    [J]. LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 1999, 1559 : 316 - 318
  • [37] Characteristic Formulae for the Verification of Imperative Programs
    Chargueraud, Arthur
    [J]. ACM SIGPLAN NOTICES, 2011, 46 (09) : 418 - 430
  • [38] Generation of correctness conditions for imperative programs
    N. V. Shilov
    I. S. Anureev
    E. V. Bodin
    [J]. Programming and Computer Software, 2008, 34 : 307 - 321
  • [39] Generation of Correctness Conditions for Imperative Programs
    Shilov, N. V.
    Anureev, I. S.
    Bodin, E. V.
    [J]. PROGRAMMING AND COMPUTER SOFTWARE, 2008, 34 (06) : 307 - 321
  • [40] A Theory of Slicing for Imperative Probabilistic Programs
    Amtoft, Torben
    Banerjee, Anindya
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2020, 42 (02):