Lab Course SoSe2025 - Pentagon Domain

conf/pentagon-svcomp25.json

@@ -0,0 +1,114 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless",
+      "pentagon"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "reduceAnalyses",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

conf/pentagon.json

@@ -0,0 +1,19 @@
+{
+  "ana": {
+    "activated": [
+      "assert",
+      "pentagon"
+    ]
+  },
+  "result": "none",
+  "solver": "td3",
+  "solvers": {
+    "td3": {
+      "term": true,
+      "space": false,
+      "space_cache": true,
+      "space_restore": true
+    }
+  },
+  "verify": true
+}

scripts/creduce/simple.sh

@@ -0,0 +1,18 @@
+#!/bin/bash
+
+# Run creduce like:
+# creduce --timeout 900 ./scripts/creduce/incremental.sh /home/feniuk/University-Coding/bench/coreutils/cksum_comb.minimized.c
+
+
+GOBLINTDIR="/home/feniuk/University-Coding/analyzer-pentagon/goblint"
+INPUTFILE="/home/feniuk/University-Coding/bench/coreutils/cut_comb.minimized.c"
+OUTPUTFILE="fe8f7af3a.out"
+PARAMS="--set ana.activated[+] pentagon --enable allglobs --enable dbg.timing.enabled"
+
+$GOBLINTDIR $INPUTFILE $PARAMS -v &> out.txt;
+if [ $? -eq 2 ]; then
+    gcc $INPUTFILE -o $OUTPUTFILE  && rm $OUTPUTFILE &> /dev/null &&
+    grep "Fatal error: exception IntDomain0.ArithmeticOnIntegerBot(\"Error int op 8\")" "out.txt" >/dev/null 2>&1
+else
+    exit 5
+fi

src/analyses/apron/pentagonAnalysis.apron.ml

@@ -0,0 +1,32 @@
+(** Analysis using the pentagon domain (pntg) 
+    @see <https://doi.org/10.1016/j.scico.2009.04.004>
+    "Pentagons: A weakly relational abstract domain for the efficient validation of array accesses"
+    -- Francesco Logozzo, Manuel Fähndrich (2010) *)
+
+open Analyses
+include RelationAnalysis
+
+let spec_module: (module MCPSpec) Lazy.t =
+  lazy (
+    let module AD = PentagonDomain.D2
+    in
+    let module Priv = (val RelationPriv.get_priv ()) in
+    let module Spec =
+    struct
+      include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil)
+      let name () = "pentagon"
+    end
+    in
+    (module Spec)
+  )
+
+let get_spec (): (module MCPSpec) =
+  Lazy.force spec_module
+
+let after_config () =
+  let module Spec = (val get_spec ()) in
+  MCP.register_analysis (module Spec : MCPSpec);
+  GobConfig.set_string "ana.path_sens[+]"  (Spec.name ())
+
+let _ =
+  AfterConfig.register after_config

src/analyses/apron/pentagonAnalysis.no-apron.ml

@@ -0,0 +1,3 @@
+(* This analysis is empty on purpose. It serves only as an alternative dependency
+   in cases where the actual domain can't be used because of a missing library.
+   It was added because we don't want to fully depend on Apron. *)

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

@@ -703,7 +703,7 @@ struct
 
   let substitute_exp ask t var exp no_ov = Timing.wrap "substitution" (substitute_exp ask t var exp) no_ov
 
-
+  
   (** Assert a constraint expression.
       The overflow is completely handled by the flag "no_ov",
       which is set in relationAnalysis.ml via the function no_overflow.
@@ -780,7 +780,7 @@ struct
   let assert_constraint ask d e negate (no_ov: bool Lazy.t) =
     match Convert.tcons1_of_cil_exp ask d d.env e negate no_ov with
     | tcons1 -> meet_tcons ask d tcons1 e no_ov
-    | exception Convert.Unsupported_CilExp _ -> d
+    | exception Convert.Unsupported_CilExp _ -> Printf.printf "failed to convert cil expression\n"; d
 
   let assert_constraint ask d e negate no_ov = Timing.wrap "assert_constraint" (assert_constraint ask d e negate) no_ov