Lab Course SoSe2025 - Pentagon Domain#1740

Open

feniup wants to merge 209 commits intogoblint:masterfrom

Commits on May 7, 2025

For the PR; Created an initial file that differs;
Philip Feniuk
committed

Commits on May 8, 2025

Added new empty files for new pntg analysis and domain
Philip Feniuk
committed

Commits on May 13, 2025

First structure of the new pentagon domain
Philip Feniuk
committed

Commits on May 14, 2025

Added top and bot functions to both modules
Philip Feniuk
committed
Type annotations and Inequlities module
Philip Feniuk
committed
SUB leq
Philip Feniuk
committed

Commits on May 15, 2025

leq and join
Philip Feniuk
committed
rewritten leq and join to adhere to Apron Environment type
Philip Feniuk
committed
Implemented meet and widen, fixed leq in SUB

Alexander Mazur
authored and
Alexander Mazur
committed

Commits on May 19, 2025

Implementations for SUB.{top, is_top, narrow}
Philip Feniuk
committed

Commits on May 20, 2025

Commits on May 22, 2025

Unit test setup
Philip Feniuk
committed

Commits on May 27, 2025

Unfinished stuff; Fixed SUB functions to work with new environment stuff
Philip Feniuk
committed
Added first test cases
DP
committed
Fixed pentagon leq function
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
removed unnecessary comment
Philip Feniuk
committed
added narrow and meet
DP
committed
pentagon join implementation
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
added test cases for sub domain
DP
committed
Unit tests and some fixes
Philip Feniuk
committed
Added necessary dune config for pentagon unit testing
Philip Feniuk
committed

Commits on May 28, 2025

Fixed some unit tests and the sub functionality of SUB.is_bot and SUB.leq
Philip Feniuk
committed
i broke everything on purpose
Philip Feniuk
committed

Commits on May 29, 2025

Removed unit tests viable for rewriting; Added implementation for dim_add and dim_remove to PNTG;
Philip Feniuk
committed
Merge branch 'master' of github.com:goblint/analyzer
Philip Feniuk
committed
Merge pull request #2 from feniup/upstream_merge
feniup
authored
Merge branch 'master' into work
Philip Feniuk
committed
Comments
Philip Feniuk
committed
Commented out all functions to revitalize dune build
Philip Feniuk
committed
New type for SUB
Philip Feniuk
committed
adapted to lists and added environment handling
DP
committed
adapted dim_add dim_remove
DP
committed
SUB.dim_add
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
adapted dim_add dim_remove
DP
committed
constructed top elem
DP
committed
Removed SF functions
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
sub lattice functions

Alexander Mazur
authored and
Alexander Mazur
committed
Added VarManagement and ExpressionBounds modules
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
ocp-indent
Philip Feniuk
committed
meet implemenation
DP
committed
Added comments to top and bot functions
Philip Feniuk
committed
SUB.dim_add unit tests
Philip Feniuk
committed
Added comments to SUB.dim_add
Philip Feniuk
committed

Commits on Jun 3, 2025

dumb versions? of dim_remove
Alexander Mazur
committed
added widen function
DP
committed
D.join
Alexander Mazur
committed
implemented leq
DP
committed
added to_string for intervals
DP
committed
Added simple methods for creating single intervals (useful for testing)
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
2 tests for dim_add and dim_remove in both modules
Philip Feniuk
committed
added bot, top, is_bot, is_top
DP
committed
Added alias for module PentagonDomain.D in tests
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
Removed top and bot from submodules
Philip Feniuk
committed
fixed is_top
Philip Feniuk
committed
fixed is_bot
Philip Feniuk
committed
bot handling and test for D.leq
Alexander Mazur
committed
added test and to_string method
DP
committed
second D.leq test
Alexander Mazur
committed
Merged test cases; Created content equal for PNTG module; Used List.at instead of .nth; Comments
Philip Feniuk
committed
Tests for meet; Equal function for PNTG (module D)
Philip Feniuk
committed

Commits on Jun 4, 2025

forget_vars D and SUB
Alexander Mazur
committed
added forget_var of intervals
DP
committed
SUB.forget_vars: also filter rhs
Alexander Mazur
committed
First assin_texpr parsing
Philip Feniuk
committed
First assin_texpr parsing
Philip Feniuk
committed
First assin_texpr parsing
Philip Feniuk
committed
assign_texpr SUBs(x):=SUBs(y)
Alexander Mazur
committed

Commits on Jun 5, 2025

Added signatures to remaining functions
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
Changed type of numbers to have exclusive values for infinities
Philip Feniuk
committed
Added monadic type for intervals
Philip Feniuk
committed
assign_texpr BinOps Add, Sub, Mul, Div, Mod and added some helpers
Philip Feniuk
committed
Minor refactoring
Philip Feniuk
committed
Separated modules Intervals and INTV; Fixed tests;
Philip Feniuk
committed
ocp-indent and fixed Interval.div
Philip Feniuk
committed

Commits on Jun 10, 2025

Unfinished assign_texpr
Philip Feniuk
committed
Interval.pow finished + added comments

Alexander Mazur
authored and
Alexander Mazur
committed
Separated modules into different files
Philip Feniuk
committed

Commits on Jun 11, 2025

added assign_parallell
DP
committed
simple cases of assert_constraint
Philip Feniuk
committed
added more information to intervals at assert_constraint
Philip Feniuk
committed
Interval.pow: combined two cases

Alexander Mazur
authored and
Alexander Mazur
committed
D.assert_constraint: Fixes in interval_helper

Alexander Mazur
authored and
Alexander Mazur
committed

Commits on Jun 12, 2025

assert_constraint simple cases fixed
Philip Feniuk
committed

Commits on Jun 17, 2025

Broken pentagon analysis
Philip Feniuk
committed
Added running command to c file
Philip Feniuk
committed
ZExt ops
Philip Feniuk
committed
adapted comparision operators
DP
committed
ZExt comparison in module D
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
equality and dis-equality with zero :)
Philip Feniuk
committed
Still broken analysis but a little bit better :,)
Philip Feniuk
committed
changed config
Philip Feniuk
committed
Compute bound_texpr solely with information of Boxes
Philip Feniuk
committed
pretty
Philip Feniuk
committed
Some pretty printing
Philip Feniuk
committed

Commits on Jun 18, 2025

pretty print debugging
Alexander Mazur
committed
boxes naming
Alexander Mazur
committed
Some more special cases of assertions
Philip Feniuk
committed

Commits on Jun 19, 2025

Equalized the string representations of boxes and sub
Philip Feniuk
committed
Tracing for assert_constraint and assign_texpr
Philip Feniuk
committed
Tracing for assert_constraint, assign_texpr, dim_add and dim_remove
Philip Feniuk
committed
Fixed merge
Philip Feniuk
committed
Fixed tracing output for dim_remove
Philip Feniuk
committed
assert_constraint: EQMOD

Alexander Mazur
authored and
Alexander Mazur
committed
Changed tracing for assign_texpr to show variable
Philip Feniuk
committed
Added ZExtOps where missing
Philip Feniuk
committed
config with pentagon
Philip Feniuk
committed
Simple regression test for pentagons
Philip Feniuk
committed
Merge pull request #3 from goblint/master
feniup
authored
Merge branch 'master' into work
Philip Feniuk
committed
Merge pull request #1 from feniup/work
feniup
authored
Fix semgrep findings
Philip Feniuk
committed

Commits on Jun 20, 2025

new Intv.rem, changed assert_constraint/EQMOD

Alexander Mazur
authored and
Alexander Mazur
committed

Commits on Jun 23, 2025

deleted print debugging from lin2vareq

Alexander Mazur
authored and
Alexander Mazur
committed
Intv.rem sign handling

Alexander Mazur
authored and
Alexander Mazur
committed

Commits on Jun 24, 2025

Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
Pentagon regression tests with confusion
Philip Feniuk
committed
Pentagon regression tests with confusion
Philip Feniuk
committed
Delete unnecessary config file
Philip Feniuk
committed
Pentagon regression tests with confusion
Philip Feniuk
committed

Commits on Jun 25, 2025

assign_texpr with texpr to monomial conversion
Philip Feniuk
committed
assign_texpr with texpr to monomial conversion
Philip Feniuk
committed

Commits on Jun 26, 2025

Comments for assign_texpr: x = ay + b

Alexander Mazur
authored and
Alexander Mazur
committed
assign_texpr x=ay+b: SUBs(x) deletion

Alexander Mazur
authored and
Alexander Mazur
committed
Fixed build error: unbound t
Philip Feniuk
committed
added updates for sub
DP
committed
adapted conditionals
DP
committed
Fixed build error AGAIN
Philip Feniuk
committed
Basic structure of new assert_constraint
Philip Feniuk
committed
to_string now also replaces the variable indices in subs by their names
Philip Feniuk
committed
simple test

Alexander Mazur
authored and
Alexander Mazur
committed
to_string now also replaces the variable indices in subs by their names
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
Removed old unit tests
Philip Feniuk
committed
to_string now also replaces the variable indices in subs by their names
Philip Feniuk
committed
Use deleted subs in assign_texpr

Alexander Mazur
authored and
Alexander Mazur
committed
Refactored to_string
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
Renamed Sub to Subs
Philip Feniuk
committed
Unit test for string
Philip Feniuk
committed
Separated Pentagons child-modules to different files
Philip Feniuk
committed
Minor refactoring
Philip Feniuk
committed
Actually assert something in the unit test
Philip Feniuk
committed

Commits on Jul 1, 2025

assign_texpr: general case

Alexander Mazur
authored and
Alexander Mazur
committed
Special case for Modulo
Philip Feniuk
committed

Commits on Jul 2, 2025

Fixed modulo special case
Philip Feniuk
committed
Renamed some local variables to better match our thinking
Philip Feniuk
committed
added first structure of assert_constraint
DP
committed

Commits on Jul 3, 2025

Fixed build error at assert_constraint
Philip Feniuk
committed
Work in progress
Philip Feniuk
committed

Commits on Jul 7, 2025

bug fixes, commenting in assign + assert

Alexander Mazur
authored and
Alexander Mazur
committed

Commits on Jul 8, 2025

Work in progress
Philip Feniuk
committed
very difficult bug fix
Alexander Mazur
committed

Commits on Jul 9, 2025

Added regression test
Alexander Mazur
committed
Work in progress
Philip Feniuk
committed

Commits on Jul 10, 2025

work in progress

Alexander Mazur
authored and
Alexander Mazur
committed
Finished clever implementation mentioned by Miné
Philip Feniuk
committed
Merge pull request #4 from feniup/work
feniup
authored
Merge remote-tracking branch 'upstream/master'
Philip Feniuk
committed
Merge branch 'master' of github.com:feniup/analyzer-pentagon
Philip Feniuk
committed
Added regression test

Alexander Mazur
authored and
Alexander Mazur
committed
First draft of the invariant function
Philip Feniuk
committed
Merge branch 'work' of github.com:feniup/analyzer-pentagon into work
Philip Feniuk
committed
Merge branch 'master' into work
Philip Feniuk
committed

Commits on Jul 16, 2025

simple creduce script
Philip Feniuk
committed
Moved regression tests; Added TODOs; Added svcomp config for pentagon; Some timing wraps;
Philip Feniuk
committed
ocp-indent changes
Philip Feniuk
committed
Merge pull request #5 from feniup/work
feniup
authored
Deriving hash and eq function; Verify in config set to true; removed ';;'
Philip Feniuk
committed
Add a todo to bound_texpr
Philip Feniuk
committed
Printing texpr and intv for bound_texpr
Philip Feniuk
committed

Commits on Jul 17, 2025

work in progress
Alexander Mazur
committed
added consistency check between linearized and non-linearized interval evaluation
Alexander Mazur
committed
adapted narrowing for intb
DP
committed
adapted boses
DP
committed
Fixed conversion from scalar to zext; Fixed narrowing for Pntg; Added some explaining comments; Minor performance stuff;
Philip Feniuk
committed

Commits on Jul 22, 2025

Add gcc to creduce script
Philip Feniuk
committed

Commits on Jul 23, 2025

Remove narrow for Subs; Timing.wrap for dim_add and dim_remove;
Philip Feniuk
committed
Merge pull request #6 from feniup/work
feniup
authored
Merge remote-tracking branch 'origin/master' into work
Philip Feniuk
committed
Added sub usage in bound_texpr and assign_texpr
Alexander Mazur
committed
Adapted regression test because of added functionality
Alexander Mazur
committed
Merge pull request #7 from feniup/work
feniup
authored
Merge remote-tracking branch 'upstream/master'
Philip Feniuk
committed

Commits on Jul 25, 2025

Fixed pentagon memory issue
Philip Feniuk
committed
Reverted printing in Lin2Var assert_constraint
Philip Feniuk
committed
Remove double semicolons
Philip Feniuk
committed

Commits on Jul 26, 2025

Renamed eval_monoms_to_intv_infty_list
Philip Feniuk
committed
sign bug fix

Alexander Mazur
authored and
Alexander Mazur
committed

Commits on Jul 29, 2025

PR suggested changes
Philip Feniuk
committed
Removed pentagon from unit test dune file
Philip Feniuk
committed
Reverted removing include_dir unqualified
Philip Feniuk
committed
Merge upstream/master to origin/master
Philip Feniuk
committed
Add Pentagon Modules to goblint_lib.ml to satisfy docs/api-build github action
Philip Feniuk
committed
Fixed failure reason of benchmarks
Philip Feniuk
committed
running commands in regression tests

Alexander Mazur
authored and
Alexander Mazur
committed

Commits on Jul 30, 2025

Removed unnecessary todos.
Philip Feniuk
committed
Merge branch 'master' of github.com:feniup/analyzer-pentagon
Philip Feniuk
committed
Merge remote-tracking branch 'upstream/master'
Philip Feniuk
committed
Moved pentagon regression tests; Added wrong_verdicts.md file for further investigations
Philip Feniuk
committed