Code

asserting in expressions#660

Code

Closed

dewert99 wants to merge 134 commits intoviperproject:masterviperproject/silver:masterfrom dewert99:assertingdewert99/silver:assertingCopy head branch name to clipboard

+82-21

Commits

Commits on Dec 4, 2020

• adding method rewrite proof-of-concept

  

  jyoo980

  authored and

  ionathanch

  committed
  810604d

• performing rewrite

  

  jyoo980

  authored and

  ionathanch

  committed
  8e60d22

• adding rewrite utilities for Fold/Unfold

  

  jyoo980

  authored and

  ionathanch

  committed
  c3e152d

• Mostly using Strategys to traverse various AST structures.

  ionathanch

  committed
  fa6539e

• Fix expandPredicates

  ionathanch

  committed
  bd84159

• expandPredicates and removeFoldUnfold now work properly.

  Show description for 6db3d7d
  ionathanch

  committed
  6db3d7d

• Collections are monads with a join operation

  Show description for 7443e13
  ionathanch

  committed
  7443e13

• You may not like it, but *this* is peak monad

  ionathanch

  committed
  ecf747b

• fixing issue with .exists

  

  jyoo980

  authored and

  ionathanch

  committed
  f79144f

• Separated out inlining and rewriting again.

  Show description for 6cb5bd4
  ionathanch

  committed
  6cb5bd4

• Separated out getting predicate names and expanding them.

  Show description for 41a4919
  ionathanch

  committed
  41a4919

• Added infrastructure for doing parsing extensions.

  ionathanch

  committed
  de1727a

• Thread InlinePredicate names through various relevant functions.

  ionathanch

  committed
  3b1cd57

• Sprinkling in some TODOs.

  ionathanch

  committed
  5af02c3

• One more TODO.

  ionathanch

  committed
  9026c98

• adding support for checking recursive predicates

  

  jyoo980

  authored and

  ionathanch

  committed
  a0a4723

• fixing issue with .existsDefined

  

  jyoo980

  authored and

  ionathanch

  committed
  f224137

• fixing readability issues

  

  jyoo980

  authored and

  ionathanch

  committed
  fd2c0af

• adding basic tests for recursion detection

  

  jyoo980

  authored and

  ionathanch

  committed
  216f1a7

• simplifying child traversal for recursion, adding more tests

  

  jyoo980

  authored and

  ionathanch

  committed
  2bb3489

Commits on Dec 5, 2020

• adding first pass at mutual-recursion detection

  jyoo980

  committed
  96e0c95

• extracting PredicateCallGraph object for reuse

  jyoo980

  committed
  698a53e

Commits on Dec 6, 2020

• modifying access modifier for CallGraph

  jyoo980

  committed
  025117d

Commits on Dec 14, 2020

• fixing issue where fold statements were not removed

  jyoo980

  committed
  2ba559a

Commits on Dec 15, 2020

• adding lazy eval for recursive search

  jyoo980

  committed
  f86baf1

Commits on Dec 16, 2020

• adding initial implementation of permission passthrough

  jyoo980

  committed
  fd4a08a

• add documentation for function

  jyoo980

  committed
  842f6f2

• fixing doc typo

  jyoo980

  committed
  6e461b7

• adding initial implementation of permission passthrough

  jyoo980

  authored
  18292f5

Commits on Dec 17, 2020

• adding pretty-printing

  jyoo980

  committed
  3510c0a

• Merge branch 'master' into yoo/mutual-ref

  jyoo980

  authored
  39bd322

• fixing minor typos

  jyoo980

  committed
  c049944

• adding first pass at mutual-recursion detection

  jyoo980

  authored
  527dffb

• Merge branch 'master' into yoo/fix-fold-unfold-bug

  jyoo980

  authored
  4b0ffa1

Commits on Dec 18, 2020

• Make nested predicates expand properly; fixes viperproject#20

  ionathanch

  committed
  f65bbb4

• Replace .filter.map => .collect

  ionathanch

  committed
  f2d3d65

• Merge pull request viperproject#23 from jyoo980/ionathanch/nested-preds

  Show description for d8ddd25
  ionathanch

  authored
  d8ddd25

Commits on Dec 19, 2020

• pushing files

  

  jyoo980

  authored and

  ionathanch

  committed
  8891df7

• adding translateMember impl

  

  jyoo980

  authored and

  ionathanch

  committed
  d62f8d2

• adding .nonEmpty check

  

  jyoo980

  authored and

  ionathanch

  committed
  66aa162

• adding changes to PInlinePredicate

  

  jyoo980

  authored and

  ionathanch

  committed
  9720454

• Add TODO comments back in.

  ionathanch

  committed
  e4cd53b

• Updated default value for expected plugins

  alison-li

  committed
  cdf7601

• adding initial attempt for inhale expansion

  

  jyoo980

  authored and

  ionathanch

  committed
  dcd2a91

• simplifying code

  

  jyoo980

  authored and

  ionathanch

  committed
  6160e63

• Also expand exhales; use expandPredicates for expandInhaleExhales.

  ionathanch

  committed
  6585e37

• adding test files

  jyoo980

  committed
  97434ce

• adding test files

  jyoo980

  authored
  1bd62ef

• adding more test files

  jyoo980

  committed
  c4913d4

Commits on Dec 20, 2020

• Implemented expanding asserts and invariants.

  ionathanch

  committed
  57aae7a

• Update doc comment for expandStatements.

  ionathanch

  committed
  250422a

• Initial attempt at rewriting functions.

  ionathanch

  committed
  7be242f

• Finished rewriting functions.

  ionathanch

  committed
  dcf505a

• In hindsight, when you expand statements, you always want to remove folds and unfolds anyway.

  ionathanch

  committed
  4bc3698

• adding doc typo fix

  

  jyoo980

  authored and

  ionathanch

  committed
  b81574f

• Added test for function expansions.

  ionathanch

  committed
  2c5b341

Commits on Dec 21, 2020

• adding fix for nested non-recursive pred calls in recursive preds (viperproject#36)

  jyoo980

  authored
  4b53b23

• Fix incorrect permission propagation (should be multiplicative)

  ionathanch

  committed
  406441d

• Check if predicate body is defined in cond.

  ionathanch

  committed
  4806d6b

• making warnings more visible

  jyoo980

  committed
  15fd894

• merging with master

  jyoo980

  committed
  24f318a

• making warnings more visible (viperproject#41)

  jyoo980

  authored
  b6886a7

• merging with master

  jyoo980

  committed
  ff1e086

• making warnings yellow

  jyoo980

  committed
  3bdf449

• Check for recursive predicates using /all/ existing predicates.

  ionathanch

  committed
  b2e6b30

• Turn fold/unfold statements into assert statements.

  ionathanch

  committed
  97f4ec9

Commits on Dec 22, 2020

• Recursively call expandPredicate on current node.

  ionathanch

  committed
  0ef6104

• adding bugfix for recursion detection (viperproject#45)

  jyoo980

  authored
  b0e7d91

• Fix prettyPrint colours.

  ionathanch

  committed
  af0678d

• Expand unfoldings in all places.

  ionathanch

  committed
  e7a0b57

• Turns out Seqns have scope (local variables). Thread those through during expandStatement for use in expandExpression.

  ionathanch

  committed
  3d34a76

Commits on Dec 11, 2021

• Update README.rst

  Show description for 180fae4
  dewert99

  authored
  180fae4

• Added an easy way to check the output of inlining

  dewert99

  committed
  a5f2460

• Added inline keyword, so that only predicates marked with the inline keyword would be inlined

  dewert99

  committed
  f65d8d6

• Switched recursion breaking strategy to only find a subset of mutually recursive preds to avoid inlining

  dewert99

  committed
  20d764c

• Switched testing strategy to use test files and improved loop-breaker choosing strategy

  dewert99

  committed
  7792f46

• Added test sure all tests are still valid after inlining

  dewert99

  committed
  c537b34

• Modified handling of none permission

  dewert99

  committed
  606da87

• Improved inlining of unfolding expressions

  dewert99

  committed
  0d6db63

• Revert "Update README.rst"

  Show description for ffd32f9
  dewert99

  committed
  ffd32f9

Commits on Dec 13, 2021

• Cleaned (p)ast extensions

  dewert99

  committed
  ac15547

• Merge tag 'v.21.07-release' into pred-inline

  Show description for 57ee5cf
  dewert99

  committed
  57ee5cf

• Modified inlined plugin to work with newer versions of dependencies.

  dewert99

  committed
  ff408fa

Commits on Dec 14, 2021

• Added error transformer for unfolding errors

  dewert99

  committed
  54dc70c

Commits on Dec 19, 2021

• Fixed incorrect use of caching and error when unfolding with non-write permission

  dewert99

  committed
  a4c86aa

Commits on Apr 29, 2022

• Replaced __second__ with let

  dewert99

  committed
  2d6af40

• Stopped using deprecated conversions

  dewert99

  committed
  f493363

Commits on May 1, 2022

• Created simpler program rewriter

  dewert99

  committed
  d81a8b3

• Improved constant folding

  dewert99

  committed
  de4a2cd

• Optimizations

  dewert99

  committed
  63078c9

Commits on May 6, 2022

• Started error rewriting + other fixes

  dewert99

  committed
  a70c39d

Commits on May 9, 2022

• Simplified errTs

  dewert99

  committed
  e96dc57

• Switched parser modification to force inline predicates to have bodies

  dewert99

  committed
  ce374e4

• Made each dummy let variable have a different name

  dewert99

  committed
  abd62f4

Commits on May 19, 2022

• Added option to control where folds and unfolds generate assertions

  dewert99

  committed
  49961c4

• overrided mapVerificationResult

  dewert99

  committed
  e9cce49

• Moved passing pred inline tests to pass

  dewert99

  committed
  a2ce014

• Cleaned up unused methods

  dewert99

  committed
  f479e1e

• Merge branch 'master' into pred-inline

  dewert99

  committed
  4e3cda6

Commits on May 20, 2022

• Fixed issue handling pred's in pred's

  dewert99

  committed
  f888f53

• Fixed selection_sort test to pass injectivity checks

  dewert99

  committed
  90f407e

• Fixed issue with errors missing pos

  dewert99

  committed
  30c953f

• Fixed issue with quantified permissions

  dewert99

  committed
  f11eef8

• Fixed issue where error-transformers wouldn't work on preds with conjunctions in there bodies

  dewert99

  committed
  47555cb

Commits on May 24, 2022

• Added asserting-in expression

  dewert99

  committed
  03d01e5

Commits on May 25, 2022

• Extracted super trait HintExp for Unfolding, Applying, and Asserting

  dewert99

  committed
  43ddcc3

Commits on May 26, 2022

• Merge branch 'asserting-in' into pred-inline

  dewert99

  committed
  9e9e65e

• Added option to compile the unfolding of inline predicates to asserting in

  dewert99

  committed
  d46adf6

Commits on May 27, 2022

• Added option to compile the unfolding of inline predicates to asserting in

  dewert99

  committed
  30a1bd7

Commits on May 31, 2022

• Fixed Inline CLI

  dewert99

  committed
  04a22fd

Commits on Jun 1, 2022

• Fixed issue where regex used to detect files to group together was overly permissive causeing issue for tests that had "file" in there name

  dewert99

  committed
  c90412a

• Merge branch 'testinput-fileregex-fix' into pred-inline-config

  dewert99

  committed
  394f4b1

Commits on Jun 2, 2022

• Added an option to make StatisticalTestSuite resumable

  dewert99

  committed
  657bb8d

• Merge branch 'resumable-statistical-test' into pred-inline-config

  dewert99

  committed
  9eafa2b

Commits on Jun 7, 2022

• Merge branch 'wand-let-old' into pred-inline-config

  dewert99

  committed
  bca253a

Commits on Jun 9, 2022

• Added intentionally failings test for new cases discovered by running the base carbon test suite with inlining on

  dewert99

  committed
  7a96318

• Improved error message for ill-formed inline predicates

  dewert99

  committed
  2223411

• Switched to generating auto triggers before desugaring predicate body

  dewert99

  committed
  01117d0

Commits on Jun 10, 2022

• Fixed test case to use inline predicate

  dewert99

  committed
  39cec76

• Added basic support for wildcard permissions

  dewert99

  committed
  b0a6a9f

• Made unfolding check functions only monomorphize to wildcards as needed

  dewert99

  committed
  b6ca018

Commits on Jun 11, 2022

• Switched to useing a name generator

  dewert99

  committed
  2a00d77

Commits on Jun 13, 2022

• Used domain functions to handle inline predicates being used in triggers

  dewert99

  committed
  ce014b2

• Switched to checking auto triggers as well in case a generated trigger includes an inline pred

  dewert99

  committed
  4ec2bc2

• Made using a perm expression with an inline predicate a consistency error

  dewert99

  committed
  92eb2a1

• Undo

  dewert99

  committed
  a30fdee

• Merge branch 'pred-inline' into pred-inline-config

  Show description for 7b3ba16
  dewert99

  committed
  7b3ba16

• Fixed merge

  dewert99

  committed
  31eccb7

Commits on Nov 3, 2022

• Update Transformer.scala

  Show description for 52893e4
  dewert99

  authored
  52893e4

Commits on Mar 7, 2023

• Merge remote-tracking branch 'origin/asserting-in' into pred-inline-config

  dewert99

  committed
  ca6510a

Commits on Mar 8, 2023

• Merge branch 'master' into pred-inline-config

  Show description for 1fea9e0
  dewert99

  committed
  1fea9e0

• Moved tests

  dewert99

  committed
  ba8807a

Commits on Mar 14, 2023

• Reverted non asserting changes

  dewert99

  committed
  c1908eb

• Added failing test for Carbon

  dewert99

  committed
  1358158