Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Declarative Specification of Intraprocedural Control-flow and Dataflow Analysis

Riouak, Idriss LU orcid (2023)
Abstract
Static program analysis plays a crucial role in ensuring the quality and security of software applications by detecting and fixing bugs, and potential security vulnerabilities in the code. The use of declarative paradigms in dataflow analysis as part of static program analysis has become increasingly popular in recent years. This is due to its enhanced expressivity and modularity, allowing for a higher-level programming approach, resulting in easy and efficient development.

The aim of this thesis is to explore the design and implementation of control-flow and dataflow analyses using the declarative Reference Attribute Grammars formalism. Specifically, we focus on the construction of analyses directly on the source code rather than... (More)
Static program analysis plays a crucial role in ensuring the quality and security of software applications by detecting and fixing bugs, and potential security vulnerabilities in the code. The use of declarative paradigms in dataflow analysis as part of static program analysis has become increasingly popular in recent years. This is due to its enhanced expressivity and modularity, allowing for a higher-level programming approach, resulting in easy and efficient development.

The aim of this thesis is to explore the design and implementation of control-flow and dataflow analyses using the declarative Reference Attribute Grammars formalism. Specifically, we focus on the construction of analyses directly on the source code rather than on an intermediate representation.

The main result of this thesis is our language-agnostic framework, called IntraCFG. IntraCFG enables efficient and effective dataflow analysis by allowing the construction of precise and source-level control-flow graphs. The framework superimposes control-flow graphs on top of the abstract syntax tree of the program. The effectiveness of IntraCFG is demonstrated through two case studies, IntraJ and IntraTeal. These case studies showcase the potential and flexibility of IntraCFG in diverse contexts, such as bug detection and education. IntraJ supports the Java programming language, while IntraTeal is a tool designed for teaching program analysis for an educational language, Teal.

IntraJ has proven to be faster than and as precise as well-known industrial tools. The combination of precision, performance, and on-demand evaluation in IntraJ leads to low latency in querying the analysis results. This makes IntraJ a suitable tool for use in interactive tools. Preliminary experiments have also been conducted to demonstrate how IntraJ can be used to support interactive bug detection and fixing.

Additionally, this thesis presents JFeature, a tool for automatically extracting and summarising the features of a Java corpus, including the use of different Java features (e.g., use of Lambda Expressions) across different Java versions. JFeature provides researchers and developers with a deeper understanding of the characteristics of corpora, enabling them to identify suitable benchmarks for the evaluation of their tools and methodologies. (Less)
Please use this url to cite or link to this publication:
author
supervisor
organization
publishing date
type
Thesis
publication status
published
subject
keywords
Static program analysis, Declarative paradigms, Reference Attribute Grammars, Control flow analysis, Data flow analysis, IntraCFG framework, Bug detection, IntraJ Static Analyser, Interactive bug detection and fixing, JFeature Static Analyser
pages
109 pages
publisher
Lund University
ISBN
978-91-8039-587-8
978-91-8039-586-1
project
Explainable Declarative Programming Analysis
language
English
LU publication?
yes
id
9a49a9e6-ab68-4c67-af67-6963782a128d
date added to LUP
2023-02-13 16:39:58
date last changed
2023-02-23 14:47:33
@misc{9a49a9e6-ab68-4c67-af67-6963782a128d,
  abstract     = {{Static program analysis plays a crucial role in ensuring the quality and security of software applications by detecting and fixing bugs, and potential security vulnerabilities in the code. The use of declarative paradigms in dataflow analysis as part of static program analysis has become increasingly popular in recent years. This is due to its enhanced expressivity and modularity, allowing for a higher-level programming approach, resulting in easy and efficient development.<br/><br/>The aim of this thesis is to explore the design and implementation of control-flow and dataflow analyses using the declarative Reference Attribute Grammars formalism. Specifically, we focus on the construction of analyses directly on the source code rather than on an intermediate representation.<br/><br/>The main result of this thesis is our language-agnostic framework, called IntraCFG. IntraCFG enables efficient and effective dataflow analysis by allowing the construction of precise and source-level control-flow graphs. The framework superimposes control-flow graphs on top of the abstract syntax tree of the program. The effectiveness of IntraCFG is demonstrated through two case studies, IntraJ and IntraTeal. These case studies showcase the potential and flexibility of IntraCFG in diverse contexts, such as bug detection and education. IntraJ supports the Java programming language, while IntraTeal is a tool designed for teaching program analysis for an educational language, Teal.<br/><br/>IntraJ has proven to be faster than and as precise as well-known industrial tools. The combination of precision, performance, and on-demand evaluation in IntraJ leads to low latency in querying the analysis results. This makes IntraJ a suitable tool for use in interactive tools. Preliminary experiments have also been conducted to demonstrate how IntraJ can be used to support interactive bug detection and fixing.<br/><br/>Additionally, this thesis presents JFeature, a tool for automatically extracting and summarising the features of a Java corpus, including the use of different Java features (e.g., use of Lambda Expressions) across different Java versions. JFeature provides researchers and developers with a deeper understanding of the characteristics of corpora, enabling them to identify suitable benchmarks for the evaluation of their tools and methodologies.}},
  author       = {{Riouak, Idriss}},
  isbn         = {{978-91-8039-587-8}},
  keywords     = {{Static program analysis; Declarative paradigms; Reference Attribute Grammars; Control flow analysis; Data flow analysis; IntraCFG framework; Bug detection; IntraJ Static Analyser; Interactive bug detection and fixing; JFeature Static Analyser}},
  language     = {{eng}},
  month        = {{02}},
  note         = {{Licentiate Thesis}},
  publisher    = {{Lund University}},
  title        = {{Declarative Specification of Intraprocedural Control-flow and Dataflow Analysis}},
  url          = {{https://lup.lub.lu.se/search/files/138416191/2023_IdrissRiouak_Lic.pdf}},
  year         = {{2023}},
}