Lab Course SoSe2025 - Pentagon Domain #1740
Conversation
michael-schwarz
added
student-job
relational
…nagment or Apron stuff.
…ther investigations
There was a problem hiding this comment.
Pull request overview
This PR implements the pentagon domain for the Goblint static analyzer as part of a lab course. The pentagon domain combines interval analysis with symbolic relational constraints of the form x < y, offering greater precision than traditional interval analysis while maintaining lower complexity than more expressive domains like octagons.
Changes:
- Implemented core pentagon domain modules (ZExt, Intv, Subs, Boxes, Pntg) for managing extended integers, intervals, strict upper bounds, and the pentagon structure
- Added pentagonDomain and pentagonAnalysis modules with Apron integration
- Created regression test suite with 8 test cases covering various pentagon domain scenarios
- Added configuration files for pentagon analysis
Reviewed changes
Copilot reviewed 23 out of 24 changed files in this pull request and generated 20 comments.
Show a summary per file
| File | Description |
|---|---|
| wrong_verdicts.md | Documentation of known incorrect analysis verdicts |
| tests/unit/mainTest.ml | Whitespace cleanup |
| tests/regression/89-pentagon/*.c | Regression test suite for pentagon domain functionality |
| src/goblint_lib.ml | Module exports for pentagon domain components |
| src/dune | Build configuration for pentagon modules with Apron selection |
| src/cdomains/pentagon/zExt.ml | Extended integer type with infinity support |
| src/cdomains/pentagon/intv.ml | Interval arithmetic operations |
| src/cdomains/pentagon/subs.ml | Strict upper bounds management |
| src/cdomains/pentagon/boxes.ml | Collections of intervals |
| src/cdomains/pentagon/pntg.ml | Main pentagon structure |
| src/cdomains/pentagon/stringUtils.ml | String formatting utilities |
| src/cdomains/apron/pentagonDomain.*.ml | Pentagon domain implementation with Apron integration |
| src/analyses/apron/pentagonAnalysis.*.ml | Analysis specification using pentagon domain |
| conf/pentagon*.json | Configuration files for pentagon analysis |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| module VarSet = struct | ||
| module IdxSet = BatSet.Make(Idx) | ||
| include IdxSet | ||
| let hash t = IdxSet.fold (fun idx acc -> acc lxor (19 * idx + 0x9e3779b9)) t 0 |
There was a problem hiding this comment.
The hash function implementation using a custom fold with XOR and magic number (0x9e3779b9) is non-standard and potentially problematic. The magic number appears to be added/xored incorrectly for combining hash values. Consider using a more standard approach like "IdxSet.fold (fun idx acc -> acc * 31 + idx) t 0" or similar established hash combination methods.
| let hash t = IdxSet.fold (fun idx acc -> acc lxor (19 * idx + 0x9e3779b9)) t 0 | |
| let hash t = IdxSet.fold (fun idx acc -> acc * 31 + idx) t 0 |
| if dim_change.realdim != 0 then | ||
| failwith "Pentagons are defined over integers: \ | ||
| extension with real domain is nonsensical" |
There was a problem hiding this comment.
Inconsistent comparison operator usage. The code uses "!=" for comparing with 0, but throughout the rest of the codebase, "<>" is the standard OCaml inequality operator. For consistency, use "dim_change.realdim <> 0".
| | z1, PosInfty when sign z1 < 0 -> failwith "ZExt.pow: Cannot determine whether result is NegInfty or PosInfty (or -1 or 1 for z1 = -1) -> depends on the side of the interval" | ||
| | PosInfty, _ | _, PosInfty -> PosInfty | ||
| | NegInfty, Arb z -> if Z.is_even z then PosInfty else NegInfty | ||
| | _, NegInfty -> failwith "This shouldn't happen (caught in second line of ZExt.pow)" |
There was a problem hiding this comment.
The comment contains inline code that uses backticks instead of proper inline code delimiters, and includes an unclear reference to "(caught in second line of ZExt.pow)". This error message should be more specific about what the actual issue is and provide actionable guidance.
| | _, NegInfty -> failwith "This shouldn't happen (caught in second line of ZExt.pow)" | |
| | _, NegInfty -> | |
| failwith "ZExt.pow: exponent must be a finite, non-negative value; negative infinity as an exponent is not supported." |
| in | ||
| (** Counts the number of empty sets to prepend at the current index. *) | ||
| let append_count = | ||
| Array.count_matching (fun k -> k == i) dim_change.dim |
There was a problem hiding this comment.
The comparison uses "==" instead of the structural equality operator "=". In OCaml, "==" tests physical equality (same memory location), while "=" tests structural equality (same value). For integer comparison, you should use "=" instead. This applies to both comparisons on this line.
| if lb_correction_term = PosInfty then (const_lb, [y]) else (ZExt.add const_lb lb_correction_term, [y]) | ||
| | l -> ( | ||
| if lb_correction_term = PosInfty then | ||
| failwith "This should not happen." |
There was a problem hiding this comment.
The error message "This should not happen." is vague and provides no context for debugging. Consider replacing with something more specific like "Internal error: Unexpected PosInfty in correction term when lower bound infinity list has length >= 2" to help with debugging.
| let lt ((_, ub1):t) ((lb2, _):t) = | ||
| ub1 < lb2 | ||
|
|
||
| let gt ((lb1, _):t) ((_, ub2):t) = | ||
| lb1 > ub2 |
There was a problem hiding this comment.
The comparison operators (lt and gt) use OCaml's built-in comparison operators (<, >) directly on ZExt.t values without using the custom comparison operators defined in ZExtOps. This is inconsistent with the rest of the codebase which uses (<), (>), etc. Consider using "ub1 <* lb2" and "lb1 >* ub2" for consistency.
| let lt ((_, ub1):t) ((lb2, _):t) = | |
| ub1 < lb2 | |
| let gt ((lb1, _):t) ((_, ub2):t) = | |
| lb1 > ub2 | |
| let lt ((_, ub1):t) ((lb2, _):t) = | |
| ub1 <* lb2 | |
| let gt ((lb1, _):t) ((_, ub2):t) = | |
| lb1 >* ub2 |
| if dim_change.realdim != 0 then | ||
| failwith "Pentagons are defined over integers: \ | ||
| extension with real domain is nonsensical" |
There was a problem hiding this comment.
Inconsistent comparison operator usage. The code uses "!=" for comparing with 0, but throughout the rest of the codebase, "<>" is the standard OCaml inequality operator. For consistency, use "dim_change.realdim <> 0".
| Array.count_matching (fun k -> k == i) dim_change.dim | ||
| in | ||
| (** Prepends n many empty sets to the accumulator. *) | ||
| let rec prepend_dim n acc = | ||
| if n == 0 then |
There was a problem hiding this comment.
The comparison uses "==" instead of the structural equality operator "=". In OCaml, "==" tests physical equality (same memory location), while "=" tests structural equality (same value). For integer comparison, you should use "=" instead.
| Array.count_matching (fun k -> k == i) dim_change.dim | |
| in | |
| (** Prepends n many empty sets to the accumulator. *) | |
| let rec prepend_dim n acc = | |
| if n == 0 then | |
| Array.count_matching (fun k -> k = i) dim_change.dim | |
| in | |
| (** Prepends n many empty sets to the accumulator. *) | |
| let rec prepend_dim n acc = | |
| if n = 0 then |
| if ub_correction_term = NegInfty then (const_ub, [y]) else (ZExt.add const_ub ub_correction_term, [y]) | ||
| | l -> ( | ||
| if ub_correction_term = NegInfty then | ||
| failwith "This should not happen." |
There was a problem hiding this comment.
The error message "This should not happen." is vague and provides no context for debugging. Consider replacing with something more specific like "Internal error: Unexpected NegInfty in correction term when upper bound infinity list has length >= 2" to help with debugging.
| failwith "This should not happen." | |
| failwith "Internal error: Unexpected NegInfty in correction term when upper bound infinity list has length >= 2" |
|
|
||
| let to_yojson t = failwith "TODO" | ||
|
|
There was a problem hiding this comment.
The to_yojson function is not implemented and just contains "failwith TODO". This is a placeholder that should either be implemented or removed before merging. If JSON serialization is not required for this domain, consider removing this function or documenting why it's intentionally unimplemented.
| let to_yojson t = failwith "TODO" | |
| (* JSON serialization uses the textual representation of the domain element. *) | |
| let to_yojson (t:t) = `String (show t) |
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
|
What is the plan with this? Is it in working order and is the goal to still have it merged? |
|
There are a few wrong verdicts still in there. This is on my list of things to fix, but for now we should not merge this. |
4 participants
Lab Course: Static Analysis with Goblint
In this lab course we try to actively contribute to the Goblint codebase by integrating new abstract domain.
In the current iteration, the focus is on the development of the pentagon domain (Pntg), which combines interval analysis with symbolic relational constraints of the form$x < y$ . This hybrid approach offers greater precision than traditional interval analysis while maintaining lower complexity compared to more expressive domains like the octagon domain.