Runtime Complexity Analysis - unexpected result

[ghost]

Infer version: 0.17.0 OS: MacOS High Sierra

I tried to reproduce the example from the documentation given here: https://fbinfer.com/docs/checker-cost/

File.java

import java.util.ArrayList;

class File {
    public void loop(ArrayList<Integer> list){
        for (int i = 0; i <= list.size(); i++){
        }
    }
}

Invoking infer --cost-only -- javac File.java yields to the ouput:

Capturing in javac mode...
Found 1 source file to analyze in /Users/test/Desktop/src/main/java/infer-out

Analysis finished in 1.376ss

/infer-out/costs-report.json

[
  {
    "hash": "0e09b8a8456e044344a39eba6ed1bd16",
    "loc": {
      "file": "File.java",
      "lnum": 3,
      "cnum": -1,
      "enum": -1
    },
    "procedure_name": "<init>",
    "procedure_id": "File.<init>()",
    "alloc_cost": {
      "polynomial": "hJWmvgAAAAQAAAACAAAABQAAAAWQoEBA",
      "hum": {
        "hum_polynomial": "0",
        "hum_degree": "0",
        "big_o": "O(1)"
      }
    },
    "exec_cost": {
      "polynomial": "hJWmvgAAAAQAAAACAAAABQAAAAWQoENA",
      "hum": {
        "hum_polynomial": "3",
        "hum_degree": "0",
        "big_o": "O(1)"
      }
    }
  },
  {
    "hash": "e4dae82706c01f400f611162f2437196",
    "loc": {
      "file": "File.java",
      "lnum": 4,
      "cnum": -1,
      "enum": -1
    },
    "procedure_name": "loop",
    "procedure_id": "File.loop(java.util.ArrayList):void",
    "alloc_cost": {
      "polynomial": "hJWmvgAAAAQAAAACAAAABQAAAAWQoEBA",
      "hum": {
        "hum_polynomial": "0",
        "hum_degree": "0",
        "big_o": "O(1)"
      }
    },
    "exec_cost": {
      "polynomial": "hJWmvgAAABMAAAAHAAAAEgAAABGRkJCQsEUA/5IpRmlsZS5qYXZh",
      "hum": {
        "hum_polynomial": "⊤",
        "hum_degree": "Top",
        "big_o": "Top"
      }
    }
  }
]

Why exec_cost of the loop method is O(Top)? I was expecting O(|list|).

[jvillard]

I think this is because you are using an old version of infer. In the latest version the cost is O(list.length(u)) as expected.

[ghost]

Hi,

thanks for your reply.

Unfortunately, I still get the same (wrong) result with infer built from source (v1.0.0-55871dd2):

[
  {
    "hash": "0e09b8a8456e044344a39eba6ed1bd16",
    "loc": {
      "file": "File.java",
      "lnum": 3,
      "cnum": -1,
      "enum": -1
    },
    "procedure_name": "<init>",
    "procedure_id": "File.<init>()",
    "is_on_ui_thread": false,
    "exec_cost": {
      "polynomial_version": 10,
      "polynomial": "hJWmvgAAAAYAAAADAAAACAAAAAiSoKBCQEA=",
      "degree": 0,
      "hum": {
        "hum_polynomial": "2",
        "hum_degree": "0",
        "big_o": "O(1)"
      },
      "trace": []
    },
    "autoreleasepool_size": {
      "polynomial_version": 10,
      "polynomial": "hJWmvgAAAAYAAAADAAAACAAAAAiSoKBAQEA=",
      "degree": 0,
      "hum": {
        "hum_polynomial": "0",
        "hum_degree": "0",
        "big_o": "O(0)"
      },
      "trace": []
    }
  },
  {
    "hash": "e4dae82706c01f400f611162f2437196",
    "loc": {
      "file": "File.java",
      "lnum": 4,
      "cnum": -1,
      "enum": -1
    },
    "procedure_name": "loop",
    "procedure_id": "File.loop(java.util.ArrayList):void",
    "is_on_ui_thread": false,
    "exec_cost": {
      "polynomial_version": 10,
      "polynomial": "hJWmvgAAABMAAAAHAAAAEgAAABGRkJCQsEUA/5IpRmlsZS5qYXZh",
      "hum": {
        "hum_polynomial": "⊤",
        "hum_degree": "Top",
        "big_o": "Top"
      },
      "trace": [
        {
          "level": 0,
          "filename": "File.java",
          "line_number": 5,
          "column_number": -1,
          "description": "Unbounded loop"
        },
        {
          "level": 0,
          "filename": "File.java",
          "line_number": 5,
          "column_number": -1,
          "description": "Loop"
        }
      ]
    },
    "autoreleasepool_size": {
      "polynomial_version": 10,
      "polynomial": "hJWmvgAAAAYAAAADAAAACAAAAAiSoKBAQEA=",
      "degree": 0,
      "hum": {
        "hum_polynomial": "0",
        "hum_degree": "0",
        "big_o": "O(0)"
      },
      "trace": []
    }
  }
]

[jvillard]

This is very strange! I just tried and get the right complexity. What's your version of Java? javac -version Mine is Java 8. It could be that the models don't work properly with higher versions of Java.

[ghost]

My Java version is 13.0.2.

When I switch to Java 8, the result is as expected. So you are right, it does not seem to work with higher Java versions.

Moreover, I realised that Java 13 is also causing problems when using a for each loop (results in O(Top)), ie,

import java.util.*;

public class File {
    public void loop(ArrayList<Integer> list){
        for (int i:
             list) {
        }
    }
}

and also when using Iterable.foreach() (results in O(1)), ie,

import java.util.*;

public class File {
    public void loop(ArrayList<Integer> list){
        list.forEach(__ -> {});
    }
}

Is infer only supposed to work with Java 8 or is it actually intended to work with newer Java versions, too?

[rrd1]

I'm facing same issue analyzing a C file with prebuilt infer release 1.1.0 and gcc 9.3.0. [Update] Just built Infer from latest sources (Infer version v1.1.0-e1baad36) with gcc 10.2.1 but still same issue[/UPDATE]

It's an iterative implementation of Merge Sort algorithm that compiles and works fine. void sort(int arr[], int n);

Additionally, I gave it a try with iterative implementation of Quick Sort using same interface. Analysis returns complexity of "Top" for both:

"loc":{"file":"mergeSort.c",
"lnum":11,
"cnum":1,
"enum":-1},
"procedure_name":"sort",
"procedure_id":"sort",
"is_on_ui_thread":false,
"exec_cost":{"polynomial_version":10,
"polynomial":"hJWmvgAAABQAAAAHAAAAEgAAABGRkJCQsGtDkittZXJnZVNvcnQuYw==",
"hum":{"hum_polynomial":"⊤",
"hum_degree":"Top",
"big_o":"Top"},
"trace":[{"level":0,
"filename":"mergeSort.c",
"line_number":43,
"column_number":3,
"description":"Unbounded loop"},
{"level":0,
"filename":"mergeSort.c",
"line_number":43,
"column_number":3,
"description":"Loop"}]},
"autoreleasepool_size":{"polynomial_version":10,
"polynomial":"hJWmvgAAAAYAAAADAAAACAAAAAiSoKBAQEA=",
"degree":0,
"hum":{"hum_polynomial":"0",
"hum_degree":"0",
"big_o":"O(0)"},
"trace":[]}}

Other functions return proper complexity.

Any support would be appreciated! Thanks in advance!