Skip to content

HW4 ‐ Advanced static analysis tools

Jump to bottom
Daniel Szekeres edited this page Nov 13, 2024 · 5 revisions

The goal of this homework is to try out advanced static analysis tools.

Environment setup

Setup a VM with Ubuntu 22.04. If you do not want to install the OS yourself, there are ready-made VMs available to download on OSboxes.

This homework will require Java 17, Infer and CPAChecker. These can be installed via:

sudo apt update
sudo apt install openjdk-17-jdk

Follow the instructions of Infer and CPAchecker.

Infer

Infer can be run in different ways depending on the build system of your project. For more information, take a quick look at the workflow section of the documentation.

Simple example (1p)

If you are only analyzing a few files (without a project), Infer can be executed based on the javac command.

  • Try Infer on the simple example files located in the Java examples folder of the Infer repository!
    infer run -- javac Hello.java Pointers.java Resources.java
    Remark: by default, you have to type the full path to the infer binary (~/tools/<infer_directory>/bin/infer on the VM). Alternatively you can add the bin folder to the PATH or create an alias.
  • The results of the analysis are displayed in the console and also in the file infer-out/report.txt. Examine the results!

CHECK: Provide a screenshot of the output of the tool. Explain the issues found by the tool.

Algorithms Project (1p)

Infer supports various build systems, including Maven (see full list).

  • Clone the Algorithms project located on GitHub!
  • The configuration of the project is a bit outdated; add the following to the pom.xml:
<properties>
    <maven.compiler.target>1.8</maven.compiler.target>
    <maven.compiler.source>1.8</maven.compiler.source>
</properties>
  • Check if the project can be compiled with mvn compile!
  • Make sure that the project is clean (mvn clean) before running Infer!
  • Run Infer by infer run -- mvn compile! Note that the first run might take some minutes.
  • Examine the results!
    • Classify the bugs found! Are there any false alarms? If yes, was it trivial to detect that it was a false alarm?
    • Are there any potential bugs?

CHECK: Create a screenshot of the list of bugs. Write next to each bug whether it is a false alarm or a potential bug. Hint: you can open the infer-out/report.txt file and write below/above each bug.

  • If there are potential bugs, fix one of them! Run Infer again and examine the results!

CHECK: Create a screenshot of the list of bugs after you have fixed one of them.*

JodaTime project (1p)

  • Clone the JodaTime project located on GitHub! This project also uses the maven build system.
  • This project is also a bit outdated now -- you will have to open the pom.xml file at the root of the project and find the lines
<maven.compiler.source>1.5</maven.compiler.source>
<maven.compiler.target>1.5</maven.compiler.target>

around the end of it. Change 1.5 to 1.8 in both lines.

  • Check if the project can be compiled with mvn compile!
  • Make sure that the project is clean (mvn clean) before running Infer!
  • Run Infer by infer run -- mvn compile!
  • Note, that this will take quite a few minutes (~10-15 minutes), as this project is larger than the last one.
    • If you don't have anything else to do while waiting for Infer and want to have a good laugh, you can check out this article about why time/date libraries (such as this project) are important and not worth to reinvent.
    • You can also start the next (CPAChecker) exercise while waiting for Infer.
  • Examine the results!
    • In this case, Infer finds a lot more issues, but it truncates the output in the terminal. Check out infer-out/report.txt!
    • What is the type of issue Infer reported the highest number of? Is it easy to detect if the issue is a false alarm or not in these cases? Is it easy to find this type of issue without a static analyzer?
    • Find this type of issue on this page of the Infer documentation to understand it better.

CHECK: Create a screenshot showing this type of issue in the Infer output. Based on what conditions was this type of issue checked and reported in this case and not in the Algorithms project? Explain this in your answer. (Hint: the answer is in the Infer documentation you just checked out above.)

CPAchecker (2p)

  • The commands for CPAchecker should be executed from its own directory.

  • Run CPAchecker on the example program (this will run CPAchecker in the default configuration):

    ./scripts/cpa.sh -default doc/examples/example.c

  • The result of the verification appears on the console, and additional files are generated in the ./output folder. Examine the results, starting with the html file (Report.html or Counterexample.html depending on the result)!

    • The CFA (Control Flow Automata) tab contains the graphical representation of the program.
    • The ARG tab contains the abstract reachability graph, which represents the possible states of the program.
    • The Source tab shows the original code.

  • Introduce an error in the program, e.g., by replacing a = 0 with a = 5 in the initialization!

  • Run CPAchecker again! Make sure to remove the ./output folder first.

  • Examine the result again! CPAchecker should highlight the counterexample in the Control Flow Automata.

CHECK: Create a screenshot of the modified program and the counterexample on the CFA tab.

Clone this wiki locally