Code

Counter Example generation#652

Code

Draft

RobinWebbers wants to merge 35 commits intoucsd-progsys:developucsd-progsys/liquid-fixpoint:developfrom RobinWebbers:developRobinWebbers/liquid-fixpoint:developCopy head branch name to clipboard

+1,979-63

Commits

Commits on Apr 20, 2023

• WIP counter example generation

  RobinWebbers

  committed
  8f574a1

  Copy full SHA for 8f574a1

Commits on May 3, 2023

• BFS Counter example generator

  RobinWebbers

  committed
  61fa746

  Copy full SHA for 61fa746

Commits on May 11, 2023

• Fixed typing issues of counter examples. Fixed issue of running multiple bodies, causing no counter example to be generated. Actually fetches counter examples from the smt solve now.

  RobinWebbers

  committed
  9914197

  Copy full SHA for 9914197

Commits on May 12, 2023

• Put counter example in output result. Only runs tests for failing clauses (if any). Put feature gate behind counter example generation.

  RobinWebbers

  committed
  0cb062b

  Copy full SHA for 0cb062b

Commits on May 25, 2023

• Now tracks counter examples per constraint id. Added a max depth to avoid infinite recursion on cyclic kvars.

  RobinWebbers

  committed
  37d9405

  Copy full SHA for 37d9405

• Removed dead code previously introduced

  RobinWebbers

  committed
  57e55b8

  Copy full SHA for 57e55b8

• Added some comments and reduced exports for CounterExample.hs

  RobinWebbers

  committed
  4188204

  Copy full SHA for 4188204

• Solved hlint warnings

  RobinWebbers

  committed
  8548f4c

  Copy full SHA for 8548f4c

Commits on Jun 13, 2023

• WIP Counterexample depth first run with location info

  RobinWebbers

  committed
  9d79fda

  Copy full SHA for 9d79fda

Commits on Jul 5, 2023

• Merge branch 'ucsd-progsys:develop' into develop

  RobinWebbers

  authored
  5fdd8d8

  Copy full SHA for 5fdd8d8

Commits on Jul 7, 2023

• Modified to depth first counter example search. Added stack traces to counterexample.

  RobinWebbers

  committed
  a2d8fee

  Copy full SHA for a2d8fee

• Split counterexample build and check

  RobinWebbers

  committed
  13dabbc

  Copy full SHA for 13dabbc

Commits on Nov 2, 2023

• Improved readback from SMT. Added back recursion limit

  RobinWebbers

  committed
  705a2ce

  Copy full SHA for 705a2ce

Commits on Nov 14, 2023

• Fixed issues with duplicate naming and SMT model parsing

  RobinWebbers

  committed
  8702a1c

  Copy full SHA for 8702a1c

Commits on Feb 15, 2024

• Counterexamples now include Result generic, symbol and type. Moved counterexample files with incorrect spelling

  RobinWebbers

  committed
  82ca427

  Copy full SHA for 82ca427

Commits on Feb 19, 2024

• Changed name scheme in counterexample to use BindId as a path instead of Symbol

  RobinWebbers

  committed
  9f91f76

  Copy full SHA for 9f91f76

• Changed the format of counterexamles. The extension to full counterexample now uses the local bind environment to get accurate types.

  RobinWebbers

  committed
  876804d

  Copy full SHA for 876804d

• Removed obsolete where binding from toFullCex

  RobinWebbers

  committed
  3b84915

  Copy full SHA for 3b84915

Commits on Feb 28, 2024

• Obsolete environments are now deleted from the counterexample

  RobinWebbers

  committed
  558306f

  Copy full SHA for 558306f

• Split SMT interface of counterexamples from checker

  RobinWebbers

  committed
  3a656bc

  Copy full SHA for 3a656bc

• Squashed calls to not incorrectly unfold multiple kvars if they were conjuncted in Counterexample checker

  RobinWebbers

  committed
  f0f0967

  Copy full SHA for f0f0967

Commits on Mar 7, 2024

• Changed counterexample SMT scope to just include top level subcid. Added JSON output for Counterexample

  RobinWebbers

  committed
  bca8208

  Copy full SHA for bca8208

Commits on Mar 8, 2024

• Solved issue where counterexamples were not correctly inserted. Solved issue where head constraint was removed from the environment.

  RobinWebbers

  committed
  2852c27

  Copy full SHA for 2852c27

Commits on Mar 14, 2024

• Used internal location information for producing spans in a counterexample

  RobinWebbers

  committed
  3b43016

  Copy full SHA for 3b43016

• Merged with latest branch of main repo

  RobinWebbers

  committed
  63211db

  Copy full SHA for 63211db

Commits on Mar 19, 2024

• Removed spurous counterexamples from declarations after assume/call/assert and underconstraint kvars when recursion depth was reached

  RobinWebbers

  committed
  bb27151

  Copy full SHA for bb27151

Commits on Mar 20, 2024

• Fixed wrong naming on 'fix$' names. Fixed wrong recursion limit, that caused the checker to do nothing

  RobinWebbers

  committed
  f50e50c

  Copy full SHA for f50e50c

Commits on Mar 24, 2024

• Added define axioms to counterexample constraints, such that we generate lists of the correct length. Renamed counterexample SMT functions.

  RobinWebbers

  committed
  72ac0fa

  Copy full SHA for 72ac0fa

• Removed debug print

  RobinWebbers

  committed
  d308c7e

  Copy full SHA for d308c7e

Commits on Mar 25, 2024

• Added support for SMT Sequence theory

  RobinWebbers

  committed
  d8049fb

  Copy full SHA for d8049fb

• Definitions as quantified axioms proved too slow, so for now I removed it from the counterexample generation.

  RobinWebbers

  committed
  d1cec55

  Copy full SHA for d1cec55

Commits on Apr 1, 2024

• Resolved issue where the counterexample build would ignore other refinements if it included kvars

  RobinWebbers

  committed
  b504b47

  Copy full SHA for b504b47

Commits on Apr 2, 2024

• Added early pruning of paths and removal of duplicate kvars (i.e. identical module transitively equivalent variables)

  RobinWebbers

  committed
  b5bbb84

  Copy full SHA for b5bbb84

• Changed search strategy from DFS to iterative deepening DFS

  RobinWebbers

  committed
  2e88e2c

  Copy full SHA for 2e88e2c

• Removed obsolete import

  RobinWebbers

  committed
  677d322

  Copy full SHA for 677d322