### Build LiSA from Source

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/index.md

This tutorial guides you through importing the LiSA source code from GitHub and building it locally. It is estimated to take 5 minutes to complete.

```markdown
[Build LiSA from source](building.md) <time>5 minutes</time>
| Importing LiSA source code from GitHub and build it locally
{:.tutorialtable}
```

--------------------------------

### Create Project with LiSA Dependency

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/index.md

This tutorial explains how to create a project that utilizes LiSA as an external dependency. It is estimated to take 5 minutes to complete.

```markdown
[Creating a project using LiSA](maven-dependency.md) <time>5 minutes</time>
| Create a project that uses LiSA as an external dependency
{:.tutorialtable}
```

--------------------------------

### Windows Local Build Setup (Ruby & Jekyll)

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/README.md

Commands to set up the local development environment for the Lisa Analyzer project on Windows using Ruby and Jekyll. This includes installing necessary gems and creating the project structure.

```bash
gem install bundler
gem install jekyll
echo "source 'https://rubygems.org'" > Gemfile
echo "gem 'github-pages', group: :jekyll_plugins" >> Gemfile
bundle install
bundle exec jekyll _3.3.0_ new . --force
echo "gem 'github-pages', group: :jekyll_plugins" >> Gemfile
bundle install
bundle exec jekyll serve
bundle exec jekyll serve --port 4001
```

--------------------------------

### Eclipse Setup for LiSA

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/building.md

Steps to import and configure the LiSA project within the Eclipse IDE, including installing the Gradle IDE Pack and resolving build path issues.

```eclipse
File -> Import... -> Existing Gradle project
Select the 'lisa' folder inside the cloned repository.

To resolve build errors:
Right-click on 'lisa-imp' project -> Build Path -> Configure Build Path...
In the 'Source' tab, add missing folders (e.g., 'lisa-imp/src/main/antlr', 'lisa-imp/build/generated-src/antlr/main').
Update output folders and test source configurations as per the documentation table.

To refresh Gradle configuration:
Right-click on 'lisa' project -> Gradle -> Refresh Gradle project
```

--------------------------------

### IntelliJ IDEA Setup for LiSA

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/building.md

Instructions for importing the LiSA project into IntelliJ IDEA, either from version control or a local clone, and initiating the Gradle build process.

```intellij
Option 1: File -> New Project from Version Control...
Enter URL: https://github.com/lisa-analyzer/lisa

Option 2: Clone the repository locally, then File -> Open...

Upon opening, select 'Import' when prompted for 'Gradle build script found'. The initial build may take several minutes.
```

--------------------------------

### Proxy Configuration for Commands

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/README.md

Environment variables and command-line parameters for configuring HTTP and HTTPS proxies, essential for network access during gem installation and other commands.

```bash
export http_proxy=http://user:password@host:port
export HTTP_PROXY=$http_proxy
export https_proxy=http://user:password@host:port
export HTTPS_PROXY=$https_proxy

# For gem install command:
gem install gem_name -v 'version' --source 'https://rubygems.org/' --http-proxy http://user:password@host:port
```

--------------------------------

### Gradle Execution for LiSA Setup Test

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/maven-dependency.md

The command to build and run the Java test application using Gradle, verifying the LiSA dependencies are correctly configured.

```bash
$ gradle run

> Task :run
[5, 5]
LiSA configuration:
  workdir: project-folder
  dump input cfgs: false
  infer types: false
  dump inferred types: false
  dump analysis results: false
  dump json report: false
  0 syntactic checks to execute
  0 semantic checks to execute

BUILD SUCCESSFUL in 5s
2 actionable tasks: 1 executed, 1 up-to-date
```

--------------------------------

### IF Statement Example

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Illustrates the usage of the IF statement in LISA, showing how to execute a block of code based on a conditional expression.

```java
def x = 4;
def y = 3;
if (x != 5) {
    return y;
}
```

--------------------------------

### LiSA CFG Sequence Example

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/cfg.md

Provides a LiSA Java API example for encoding a sequence of two statements: an assignment and a function call. It demonstrates adding nodes and edges to a Control Flow Graph (CFG).

```Java
CFG foo = new CFG(new CFGDescriptor("foo"));
Assignment a = new Assignment(foo, new Variable(foo, "x"), new Literal(foo, 5));
// depending on where 'print' is defined, a different instance of call can be used
Call print = new OpenCall(foo, "print", new Variable(foo, "x"));
foo.addNode(a, true);
foo.addNode(print);
foo.addEdge(new SequentialEdge(a, print));
```

--------------------------------

### LiSA Core Entry Point and Configuration

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/projects.md

Java classes for initiating and configuring LiSA analyses. LiSA.java is the main entry point, LiSAConfiguration.java is used for setup, and LiSAFactory.java provides default component instantiation.

```java
import it.unive.lisa.LiSAConfiguration;

public class LiSA {
    public static void main(String[] args) {
        LiSAConfiguration config = new LiSAConfiguration();
        // Configure LiSA analysis here
        // ...
        // LiSA.runAnalysis(config);
    }
}

// LiSAConfiguration.java
public class LiSAConfiguration {
    // Configuration options for LiSA analysis
}

// LiSAFactory.java
public class LiSAFactory {
    // Methods to instantiate analysis components
}
```

--------------------------------

### Throwing Errors Example

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Demonstrates how to raise errors using the 'throw' keyword in Java. Any object can be thrown to signal an error condition.

```java
throw countKm();
def cKm = counKm();
throw cKm;
```

--------------------------------

### LiSA Dependency Test Application

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/maven-dependency.md

A Java application that references classes from the lisa-sdk and lisa-core projects to confirm correct dependency setup. It prints an IntInterval and a LiSAConfiguration.

```java
package test.app;

import it.unive.lisa.LiSAConfiguration;
import it.unive.lisa.util.numeric.IntInterval;

public class App {
    public static void main(String[] args) {
        // this class is defined inside lisa-sdk
        System.out.println(new IntInterval(5, 5));
        
        // this class is defined inside lisa-core
        System.out.println(new LiSAConfiguration()); 
    }
}
```

--------------------------------

### Method Declaration and Return Statements in IMP

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Provides examples of method declarations in IMP, including a void method with an explicit return statement and a method that returns a value.

```IMP
foo() {
    return;
}
bar(i,w) {
    return i + w;
}
```

--------------------------------

### Assertions Example

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Shows how to use assertions in Java with the 'assert' keyword, followed by a boolean expression. Assertions are used for debugging and validating conditions.

```java
assert x == 10;
```

--------------------------------

### LiSA Analysis Configuration Defaults

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/analysis-infrastructure.md

Information about the default implementations used by LiSA when specific components are not explicitly provided during analysis setup. This includes the default CallGraph and HeapDomain.

```APIDOC
LiSA Analysis Defaults:

CallGraph:
  - Default Implementation: it.unive.lisa.callgraph.intraproc.IntraproceduralCallGraph
  - Behavior: Used if no CallGraph is explicitly set.

HeapDomain:
  - Default Implementation: it.unive.lisa.analysis.heap.MonolithicHeap
  - Behavior: This default is overwritten if either a HeapDomain or a NonRelationalHeapDomain is registered.

Note: It is recommended, but not mandatory, that the provided domain instances represent the top element of their respective domains.
```

--------------------------------

### LiSA Analysis Setup and Execution

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/analysis-infrastructure.md

This section details the Java API for configuring and running static analyses in LiSA. It covers setting the CallGraph, registering Heap and Value domains, and initiating the analysis run.

```Java
import it.unive.lisa.AnalysisSetup;
import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.nonrelational.heap.NonRelationalHeapDomain;
import it.unive.lisa.analysis.nonrelational.value.NonRelationalValueDomain;
import it.unive.lisa.analysis.value.ValueDomain;
import it.unive.lisa.interprocedural.callgraph.CallGraph;

// ... inside a class or method

// Set the CallGraph instance
AnalysisSetup.setCallGraph(callGraph);

// Register HeapDomain implementations
AnalysisSetup.addHeapDomain(domain);
AnalysisSetup.addNonRelationalHeapDomain(nonRelationalDomain);

// Register ValueDomain implementations
AnalysisSetup.addValueDomain(valueDomain);
AnalysisSetup.addNonRelationalValueDomain(nonRelationalValueDomain);

// Optionally, enable dumping analysis results in GraphViz dot format
AnalysisSetup.setDumpAnalysis(true);

// Run the analysis
AnalysisSetup.run();
```

--------------------------------

### For Loop Example

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Shows a 'for' loop in Java, comprising initialization, a condition, and a post-operation. It executes a block of code repeatedly. Curly braces can be omitted for single-instruction loops.

```java
for (def i = 0; i < 20; i = i + 1){
    y = y + 5;
}
```

--------------------------------

### While Loop Example

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Illustrates a 'while' loop in Java, which repeatedly executes a code block as long as a specified condition remains true. Curly braces can be omitted for single-instruction loops.

```java
def i = 5; 
while (i < 100) {
    i = i * 2;
}
```

--------------------------------

### SyntacticCheck Interface and CheckTool Usage

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/syntactic-checks.md

Demonstrates the implementation of the SyntacticCheck interface to create a custom syntactic check. The example shows how to use the beforeExecution, visitCFGDescriptor, and afterExecution callbacks to count methods named 'main' and issue a warning if more than one is found.

```java
public class MultipleMainCheck implements SyntacticCheck {
    private int counter;
    
    @Override
    public void beforeExecution(CheckTool tool) {
        this.counter = 0;
    }
    
    @Override
    public void visitCFGDescriptor(CheckTool tool, CFGDescriptor descriptor) {
        if (descriptor.getName().equals("main"))
            this.counter++;
    }

    @Override
    public void visitStatement(CheckTool tool, Statement statement) { }
    
    @Override
    public void visitExpression(CheckTool tool, Expression expression) { }
    
    @Override
    public void afterExecution(CheckTool tool) {
        if (this.counter > 1)
            tool.warn("Found " + this.counter + " methods with name \"main\"");
    }
}
```

--------------------------------

### Else Statement Example

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Demonstrates the use of an 'else' statement in Java. The 'else' block executes when the 'if' condition is false. Curly braces can be omitted if only one instruction is present.

```java
def x = 5;
def y = 3;
if (x != 5) {
    return y;
} else {
    y = y + 1;
}
```

--------------------------------

### LiSA CFG If Statement Example

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/cfg.md

Demonstrates encoding an if-else statement in LiSA using the Java API. It includes creating nodes for the condition and the two branches, and adding `TrueEdge` and `FalseEdge`.

```Java
CFG foo = new CFG(new CFGDescriptor("foo", new Variable("x")));
// assuming that GreaterThan is a subclass of NativeCall defined somwhere else in the frontend
Call gt = new GreaterThan(foo, new Variable(foo, "x"), new Literal(foo, 5));
// depending on where 'print' is defined, a different instance of call can be used
Call print1 = new OpenCall(foo, "print", new Literal(foo, "yes"));
Call print2 = new OpenCall(foo, "print", new Literal(foo, "no"));
foo.addNode(gt, true);
foo.addNode(print1);
foo.addNode(print2);
foo.addEdge(new TrueEdge(gt, print1));
foo.addEdge(new FalseEdge(gt, print2));
```

--------------------------------

### Create a new Java project with Gradle

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/maven-dependency.md

This snippet demonstrates the command to initialize a new Java project using Gradle and the expected interactive prompts and output.

```bash
$ gradle init

Select type of project to generate:
  1: basic
  2: application
  3: library
  4: Gradle plugin
Enter selection (default: basic) [1..4] 1

Select build script DSL:
  1: Groovy
  2: Kotlin
Enter selection (default: Groovy) [1..2] 1

Project name (default: test-app): test-app

> Task :init

BUILD SUCCESSFUL in 15s
2 actionable tasks: 2 executed
```

--------------------------------

### Eclipse Build Path Configuration Table

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/building.md

Details the required source folders, their output locations, and whether they contain test sources for the 'lisa-imp' project in Eclipse.

```APIDOC
Eclipse Build Path Configuration for lisa-imp:

| Folder                          | Output folder        | Contains test sources |
|---------------------------------|----------------------|-----------------------|
| lisa-imp/src/main/java          | lisa-imp/bin/main    | No                    |
| lisa-imp/src/main/resources     | lisa-imp/bin/main    | No                    |
| lisa-imp/src/main/antlr         | lisa-imp/bin/main    | No                    |
| lisa-imp/build/generated-src/antlr/main | lisa-imp/bin/main    | No                    |
| lisa-imp/src/test/java          | lisa-imp/bin/test    | Yes                   |
| lisa-imp/src/test/resources     | lisa-imp/bin/test    | Yes                   |
```

--------------------------------

### Build LiSA Analyzer (Windows)

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/building.md

Executes the Gradle build task for the LiSA Analyzer project on a Windows command line. This command navigates to the project directory and then runs the Gradle wrapper script to build the project.

```batch
cd lisa
.\gradlew.bat build
```

--------------------------------

### Build LiSA Analyzer (Mac/Linux)

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/building.md

Executes the Gradle build task for the LiSA Analyzer project on a Mac or Linux command line. This command navigates to the project directory and then runs the Gradle wrapper script to build the project.

```bash
cd lisa
./gradlew build
```

--------------------------------

### Cloning LiSA Repository

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/building.md

This command retrieves the LiSA source code from its GitHub repository using Git.

```git
git clone https://github.com/lisa-analyzer/lisa.git
```

--------------------------------

### SEO and Site Information (HTML)

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/_layouts/default.html

Includes SEO meta tags and displays the site title and description. It also provides links to the LiSA repository and the LiSA Analyzer GitHub page.

```html
{% seo %}

[![{{ site.title }}]({{ site.baseurl }}/white-title-no-bg-cropped.png)]({{ site.baseurl }}) {{ site.description }}

  [LiSA Repository]({{ site.github.repository_url }})  [LiSA Analyzer GitHub]({{ site.github.owner_url }})
```

--------------------------------

### Add LiSA dependency to Gradle build file

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/getting-started/maven-dependency.md

This snippet shows how to configure your `build.gradle` file to include LiSA's core library as a project dependency. It specifies the repository and the dependency coordinates.

```groovy
plugins {
    // tell Gradle that this is a Java command line application
    id 'application'
}

repositories {
    // use the maven central server to resolve dependencies
    mavenCentral()
}

dependencies {
    // add a depenency to LiSA
    implementation 'io.github.lisa-analyzer:lisa-core:0.1b2'
}

application {
    // tell Gradle which class is contains the main method
    mainClass = 'test.app.App'
}
```

--------------------------------

### Javadoc Documentation Links

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/releases/index.md

Links to Javadoc documentation for various modules (sdk, core, imp) across different release versions of the lisa-analyzer project.

```APIDOC
Release 0.1b4:
  sdk: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa-sdk/0.1b4/index.html
  core: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa-core/0.1b4/index.html
  imp: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa-imp/0.1b4/index.html

Release 0.1b3:
  sdk: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa-sdk/0.1.1/index.html
  core: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa-core/0.1.1/index.html
  imp: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa-imp/0.1.1/index.html

Release 0.1b2:
  sdk: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa-sdk/0.1b2/index.html
  core: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa-core/0.1b2/index.html
  imp: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa-imp/0.1b2/index.html

Release 0.1b1:
  lisa: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa/0.1b1/index.html

Release 0.1a4:
  lisa: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa/0.1a4/index.html

Release 0.1a3:
  lisa: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa/0.1a3/index.html

Release 0.1a2:
  lisa: https://www.javadoc.io/doc/io.github.lisa-analyzer/lisa/0.1a2/index.html
```

--------------------------------

### Gradle Dependency for GitHub Packages

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/releases/index.md

Configuration for Gradle to resolve dependencies from GitHub Packages. Requires authentication with a GitHub username and personal access token.

```Gradle
repositories {
    maven {
        name 'GitHubPackages'
        url "https://maven.pkg.github.com/lisa-analyzer/lisa"
        credentials {
            username System.getenv('GITHUB_ACTOR')
            password System.getenv('GITHUB_TOKEN')
        }
    }
}

dependencies {
    implementation 'io.github.lisa-analyzer:lisa-sdk:LATEST_VERSION'
}
```

--------------------------------

### Spotless Configuration

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/projects.md

Configuration for the Spotless plugin, used to enforce coding style consistency within the LiSA project, specifically adhering to an Eclipse-like coding style.

```xml
spotless-formatting.xml
```

--------------------------------

### AbstractState Structure

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/analysis-infrastructure.md

The abstract state of LiSA's analysis, parametric on HeapDomain (H) and ValueDomain (V). It implements Lattice<AbstractState<H, V>> and SemanticDomain<AbstractState<H, V>, SymbolicExpression, Identifier>. Semantic operations delegate to the heap and value domains.

```APIDOC
AbstractState<H, V> implements Lattice<AbstractState<H, V>>, SemanticDomain<AbstractState<H, V>, SymbolicExpression, Identifier>
  // Semantic operations are implemented by invoking corresponding operations on heap and value domains.
```

--------------------------------

### Constructor Declaration in IMP

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Illustrates the declaration of a constructor in IMP, which is preceded by a tilde (~). Constructors are used for object initialization and cannot be overridden.

```IMP
class Motorbike extends Vehicle {
   ~Motorbike(){}
}
```

--------------------------------

### Project Status Badges (HTML)

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/_layouts/default.html

Displays various GitHub badges indicating the project's license, workflow status, latest release version, and last commit date. These badges provide a quick overview of the project's health and activity.

```html
![GitHub License](https://img.shields.io/github/license/lisa-analyzer/lisa?color=brightgreen)
![GitHub Workflow Status (master)](https://img.shields.io/github/workflow/status/lisa-analyzer/lisa/Gradle%20Build/master)
![GitHub Latest Release](https://img.shields.io/github/v/release/lisa-analyzer/lisa?display_name=release&color=brightgreen)
![GitHub Last Commit Date](https://img.shields.io/github/last-commit/lisa-analyzer/lisa)
```

--------------------------------

### Using NoOp Statements in LiSA for Control Flow

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/cfg.md

Demonstrates the use of `NoOp` (No Operation) statements in LiSA to manage multiple exit points in control flow structures, such as conditional statements. It shows how `NoOp` nodes are added and connected, and how `foo.simplify()` can be used to remove them later.

```LiSA
CFG foo = new CFG(new CFGDescriptor("foo", new Variable("x")));
Call gt = new GreaterThan(foo, new Variable(foo, "x"), new Literal(foo, 5));
Call print1 = new OpenCall(foo, "print", new Literal(foo, "yes"));
Call print2 = new OpenCall(foo, "print", new Literal(foo, "no"));
NoOp noop = new NoOp(foo);
foo.addNode(gt);
foo.addNode(print1);
foo.addNode(print2);
foo.addNode(noop);
foo.addEdge(new TrueEdge(gt, print1));
foo.addEdge(new FalseEdge(gt, print2));
foo.addEdge(new SequentialEdge(print1, noop));
foo.addEdge(new SequentialEdge(print2, noop));
```

--------------------------------

### Field Declaration and Initialization in IMP

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Shows the correct way to declare and initialize fields within a class in IMP. Fields are declared without initial values, and initialization occurs within the constructor.

```IMP
class Vehicle {
    brand;
    ~Vehicle() {
	this.brand = "Audi"; 
    }
}
```

--------------------------------

### LiSA Built-in Type Implementations

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/cfg.md

Lists and describes the three concrete implementations of the `Type` interface provided by LiSA, which are intended to be unique across all languages. These include `NullType` for the null constant, `VoidType` for methods that do not return a value, and `Untyped` as a special type token for statically undefined constructs, serving as the root of the type lattice.

```APIDOC
NullType:
  - Represents the type of the `null` constant.
  - Located at: https://github.com/lisa-analyzer/lisa/blob/master/lisa/lisa-sdk/src/main/java/it/unive/lisa/type/NullType.java

VoidType:
  - Represents the `void` type.
  - Primarily used as the return type for methods that do not return a value.
  - Located at: https://github.com/lisa-analyzer/lisa/blob/master/lisa/lisa-sdk/src/main/java/it/unive/lisa/type/VoidType.java

Untyped:
  - A special type token used to model variables, parameters, and method return types that are not statically defined.
  - It is the root of the type lattice and the default type for all typed constructs in LiSA.
  - Enables modeling of non-statically typed languages without requiring type inference at parse time.
  - Located at: https://github.com/lisa-analyzer/lisa/blob/master/lisa/lisa-sdk/src/main/java/it/unive/lisa/type/Untyped.java
```

--------------------------------

### Default isBottom() and isTop() Implementations

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/analysis-infrastructure.md

Default implementations for checking if a lattice instance represents the bottom or top element using reference equality against unique bottom() and top() instances.

```java
public default boolean isBottom() {
	return this == bottom();
}

public default boolean isTop() {
	return this == top();
}
```

--------------------------------

### ValueDomain Interface

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/analysis-infrastructure.md

An interface for value abstractions, parametric on the concrete type V. It extends Lattice<V> and SemanticDomain<V, ValueExpression, Identifier>. It must also handle substitutions provided by the heap abstraction via the applySubstitution method.

```APIDOC
ValueDomain<V> extends Lattice<V>, SemanticDomain<V, ValueExpression, Identifier>
  applySubstitution(List<MaterializationOrSummarization> substitution): V
    Applies a substitution to the value domain.
```

--------------------------------

### Lattice Interface Methods

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/analysis-infrastructure.md

Defines methods for lattice operations such as join (lub), meet (glb), and checking for bottom or top elements. It is a generic interface parametric to the concrete instance L.

```APIDOC
Lattice<L extends Lattice<L>>:
  // Represents elements of a lattice.

  // Returns the least upper bound (join) of this lattice element and another.
  lub(L other: L): L

  // Returns the greatest lower bound (meet) of this lattice element and another.
  glb(L other: L): L

  // Checks if this lattice element represents the bottom element.
  isBottom(): boolean

  // Checks if this lattice element represents the top element.
  isTop(): boolean

  // Returns the unique bottom element of the lattice.
  bottom(): L

  // Returns the unique top element of the lattice.
  top(): L
```

--------------------------------

### Maven Dependency for GitHub Packages

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/releases/index.md

Configuration for Maven to resolve dependencies from GitHub Packages. Requires authentication with a GitHub username and personal access token.

```Maven
<repositories>
    <repository>
        <id>github</id>
        <url>https://maven.pkg.github.com/lisa-analyzer/lisa</url>
        <releases>
            <enabled>true</enabled>
        </releases>
        <snapshots>
            <enabled>true</enabled>
        </snapshots>
    </repository>
</repositories>

<dependencies>
    <dependency>
        <groupId>io.github.lisa-analyzer</groupId>
        <artifactId>lisa-sdk</artifactId>
        <version>LATEST_VERSION</version>
    </dependency>
</dependencies>
```

--------------------------------

### Cookie Consent Initialization (JavaScript)

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/_layouts/default.html

Initializes the cookie consent banner using JavaScript. It configures the banner type, consent type, color palette, language, and website name. It also sets up an event listener to run the consent configuration when the DOM is loaded.

```javascript
window.dataLayer = window.dataLayer || [];
function gtag(){
  dataLayer.push(arguments);
}

gtag('js', new Date());
gtag('config', '{{ site.google_analytics }}');

document.addEventListener('DOMContentLoaded', function () {
  cookieconsent.run({
    "notice_banner_type": "interstitial",
    "consent_type": "express",
    "palette": "light",
    "language": "en",
    "website_name": "LiSA",
    "change_preferences_selector": "#cookiePrefs"
  });
});
```

--------------------------------

### Multi-line Comments in IMP

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Shows the syntax for multi-line comments in IMP, enclosed by /* and */.

```IMP
/* this is a multi line
comment */
```

--------------------------------

### Variable Declaration and Scope

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Demonstrates the declaration of fields and local variables in LISA, illustrating their scope within classes and methods.

```java
def x;

class Vehicle {
    brand; // this is a field
    countKm() {
        def y = true; // this is a local variable visible until the end of the method
        if (y) {
            def x = 5; // this is a local variable visible until the end of the if block
        }
    }
}
```

--------------------------------

### ANTLR Grammar Generation

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/projects.md

This snippet illustrates the use of ANTLR for generating lexer and parser from a grammar file. The generated sources are stored in a specific build directory and used within the project.

```java
Project: /lisa-analyzer/lisa-analyzer.github.io
Content:
### lisa-imp

`lisa-imp` contains the IMP frontend that is used for demos and internal testing (mostly for cron tests in `lisa-core`). The project uses [antlr](https://www.antlr.org/) for generating a lexer and a parser starting from a grammar defined in `src/main/antlr`. Outputs of the generation are stored under `build/generated-src/antlr/main` and are used as additional sources for the project. The IMP frontend mostly uses expressions and types from the base ones present in `lisa-sdk`. For a documentation about the language, see the dedicated page [here]({{ site.baseurl }}/imp/).

## Releases 0.1b1 and older

LiSA was composed by one monolithic project that can be found [here](https://search.maven.org/search?q=a:lisa). The IMP frontend was all contained in the test source folder.
```

```antlr
Grammar definition in src/main/antlr
```

--------------------------------

### HeapDomain Interface

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/analysis-infrastructure.md

An interface for heap abstractions, parametric on the concrete type H. It extends Lattice<H> and SemanticDomain<H, SymbolicExpression, Identifier>, and HeapSemanticOperation. It handles heap-related expression rewriting and substitutions.

```APIDOC
HeapDomain<H> extends Lattice<H>, SemanticDomain<H, SymbolicExpression, Identifier>, HeapSemanticOperation
  getRewrittenExpressions(): Collection<SymbolicExpression>
    Provides rewritten expressions after heap abstraction.
  getSubstitution(): List<MaterializationOrSummarization>
    Yields a list of materializations and summarizations of heap identifiers.
```

--------------------------------

### Variable Declaration and Dynamic Typing in IMP

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Demonstrates IMP's dynamic typing where variables can be declared without a type and reassigned to different types. Each instruction must end with a semicolon, and 'def' precedes variable declarations.

```IMP
def x;
x = -5.2;
x = "Static Analysis is Amazing!";
```

--------------------------------

### LiSA Build Targets

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/projects.md

Custom Gradle tasks added to the LiSA build for managing different build and testing phases. These include executing cron tests, all tests, checking code style, and performing a complete build.

```gradle
build
    cron: executes tests under all packages like it.unive.lisa.cron.*
    allTests: executes both normal and cron tests
    checkCodeStyle: runs both checkstyle and spotless to ensure coding style is respected
    completeBuild: builds the project, runs normal and cron tests, and checks coding style
```

--------------------------------

### CheckTool Class Methods

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/syntactic-checks.md

Describes the CheckTool class, which provides methods for syntactic checks to interact with the LiSA analysis framework, primarily for issuing warnings.

```APIDOC
CheckTool Class:
  warn(String message)
    Issues a warning, automatically extracting the program point where the warning should be issued.
```

--------------------------------

### Encoding While Loops in LiSA

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/cfg.md

Demonstrates how to represent a Java while loop using LiSA's Control Flow Graph (CFG) constructs. It shows the mapping of the loop condition, body, and exit to LiSA's `Call`, `Assignment`, `GreaterThan`, `Sub`, `Literal`, `OpenCall`, `TrueEdge`, `SequentialEdge`, and `FalseEdge` classes.

```java
void foo(x) {
  while (x > 5)
    x = x - 1;
  print(x);
}
```

```LiSA
CFG foo = new CFG(new CFGDescriptor("foo", new Variable("x")));
// assuming that GreaterThan and Sub are subclasses of NativeCall defined somwhere else in the frontend
Call gt = new GreaterThan(foo, new Variable(foo, "x"), new Literal(foo, 5));
Assignment a = new Assignment(foo, new Variable(foo, "x"), new Sub(foo, new Variable(foo, "x"), new Literal(foo, 1)));
// depending on where 'print' is defined, a different instance of call can be used
Call print = new OpenCall(foo, "print", new Variable(foo, "x"));
foo.addNode(gt, true);
foo.addNode(a);
foo.addNode(print);
foo.addEdge(new TrueEdge(gt, a));
foo.addEdge(new SequentialEdge(a, gt));
foo.addEdge(new FalseEdge(gt, print));
```

--------------------------------

### Single Line Comments in IMP

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Illustrates how to write single-line comments in the IMP language using double forward slashes.

```IMP
// this is a single line comment
```

--------------------------------

### Encoding For Loops in LiSA

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/cfg.md

Illustrates the translation of a Java for loop into LiSA's CFG representation. This includes initializing the loop variable, the condition check, the update step, and the loop body, all mapped to corresponding LiSA classes and edges.

```java
void foo() {
  for (x = 10; x > 5; x = x - 1)
    print(x);
  print("done");
}
```

```LiSA
CFG foo = new CFG(new CFGDescriptor("foo"));
// assuming that GreaterThan and Sub are subclasses of NativeCall defined somwhere else in the frontend
Assignment a1 = new Assignment(foo, new Variable(foo, "x"), new Literal(foo, 10));
Call gt = new GreaterThan(foo, new Variable(foo, "x"), new Literal(foo, 5));
Assignment a2 = new Assignment(foo, new Variable(foo, "x"), new Sub(foo, new Variable(foo, "x"), new Literal(foo, 1)));
// depending on where 'print' is defined, a different instance of call can be used
Call print1 = new OpenCall(foo, "print", new Variable(foo, "x"));
Call print2 = new OpenCall(foo, "print", new Literal(foo, "done"));
foo.addNode(a1, true);
foo.addNode(gt);
foo.addNode(print1);
foo.addNode(a2);
foo.addNode(print2);
foo.addEdge(new SequentialEdge(a1, gt));
foo.addEdge(new TrueEdge(gt, print1));
foo.addEdge(new SequentialEdge(print1, a2));
foo.addEdge(new SequentialEdge(a2, gt));
foo.addEdge(new FalseEdge(gt, print2));
```

--------------------------------

### Navigation and Content Inclusion (HTML)

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/_layouts/default.html

Includes navigation components like a toggle menu, simple menu, and breadcrumbs. It conditionally includes breadcrumbs based on the page's 'notoc' front matter. The main content of the page is also rendered here.

```html
{% include toggle-menu.html %}
{% include simple-menu.html %}

{% unless page.notoc %}
  {% include breadcrumbs.html %}
{% endunless %}

{{ content }}
```

--------------------------------

### Encoding Do-While Loops in LiSA

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/cfg.md

Explains the LiSA representation of a Java do-while loop. It details how the loop body, condition check, and subsequent iterations are modeled using LiSA's CFG components and edge types.

```java
void foo(x) {
  do
    x = x - 1;
  while (x > 5);
  print(x);
}
```

```LiSA
CFG foo = new CFG(new CFGDescriptor("foo", new Variable("x")));
// assuming that GreaterThan and Sub are subclasses of NativeCall defined somwhere else in the frontend
Assignment a = new Assignment(foo, new Variable(foo, "x"), new Sub(foo, new Variable(foo, "x"), new Literal(foo, 1)));
Call gt = new GreaterThan(foo, new Variable(foo, "x"), new Literal(foo, 5));
// depending on where 'print' is defined, a different instance of call can be used
Call print = new OpenCall(foo, "print", new Variable(foo, "x"));
foo.addNode(a, true);
foo.addNode(gt);
foo.addNode(print);
foo.addEdge(new SequentialEdge(a, gt));
foo.addEdge(new TrueEdge(gt, a));
foo.addEdge(new FalseEdge(gt, print));
```

--------------------------------

### Class Inheritance in IMP

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/imp/index.md

Demonstrates how a subclass ('Motorbike') inherits from a superclass ('Vehicle') in IMP using the 'extends' keyword.

```IMP
class Motorbike extends Vehicle {}
```

--------------------------------

### Cross-Language Type Compatibility Check

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/cfg.md

Illustrates a scenario within LiSA's call graph implementation where type compatibility between different language frontends is checked. It highlights the importance of the `canBeAssignedTo()` method relying on interface properties (e.g., `NumericType`, `is32Bit()`) rather than concrete class checks (`instanceof`) to ensure correct assignment checks when dealing with types from different language contexts, such as Java and C.

```java
// inside java frontend
class JIntType implements NumericType { ... }

// inside c frontend
class CIntType implements NumericType { ... }

// inside one of LiSA's call graph implementations
if (t1.canBeAssignedTo(t2)) {
    // do stuff
}
```

--------------------------------

### Python Array Access Instrumentation

Source: https://github.com/lisa-analyzer/lisa-analyzer.github.io/blob/master/structure/cfg.md

Shows how a Python frontend would instrument code to achieve Java-like semantics for array access, including checking for negative indices and adjusting the index.

```Python
if index < 0:
    index = array.length - index
array[index]
```