Code

Runtime Verification#1202

Code

Draft

pieter-bos wants to merge 115 commits intodevutwente-fmt/vercors:devfrom 1-create-template-for-runtime-verificationutwente-fmt/vercors:1-create-template-for-runtime-verificationCopy head branch name to clipboard

+4,945-225

Commits

Commits on Oct 27, 2023

• Initial setup runtime verification

  ddjanssen

  committed
  acede73

  Copy full SHA for acede73

Commits on Nov 1, 2023

• Initial start on reconstructing constructors and removing unnecessary generated code

  ddjanssen

  committed
  86dff78

  Copy full SHA for 86dff78

Commits on Nov 2, 2023

• Trying to use Java AST

  ddjanssen

  committed
  0154bb7

  Copy full SHA for 0154bb7

Commits on Nov 3, 2023

• Revert "Trying to use Java AST"

  Show description for 326b797
  ddjanssen

  committed
  326b797

  Copy full SHA for 326b797

• Creating constructor works

  ddjanssen

  committed
  7d3717f

  Copy full SHA for 7d3717f

Commits on Nov 6, 2023

• Start on automated testing

  ddjanssen

  committed
  f6b8954

  Copy full SHA for f6b8954

• Created CodeString declaration to insert code directly, without having to create a very complicated ast for it

  ddjanssen

  committed
  09d7dbc

  Copy full SHA for 09d7dbc

• Created block structure to perform permission checks

  ddjanssen

  committed
  82e8abb

  Copy full SHA for 82e8abb

Commits on Nov 7, 2023

• clean up of CreateBlocksMethods.scala

  ddjanssen

  committed
  4bea70b

  Copy full SHA for 4bea70b

Commits on Nov 8, 2023

• clean up

  ddjanssen

  committed
  ef0a747

  Copy full SHA for ef0a747

• clean up

  ddjanssen

  committed
  1b18062

  Copy full SHA for 1b18062

• Created permission checks on blocks in methods

  ddjanssen

  committed
  a6e008c

  Copy full SHA for a6e008c

• Updated desciption of block permissions

  ddjanssen

  committed
  1bb38de

  Copy full SHA for 1bb38de

• Add: Pre post condition permission checking

  ddjanssen

  committed
  ce2378b

  Copy full SHA for ce2378b

Commits on Nov 9, 2023

• Start: creating array permission fields

  ddjanssen

  committed
  7dc578e

  Copy full SHA for 7dc578e

Commits on Nov 10, 2023

• Creating ideas on how to do the passes for the Transformation

  ddjanssen

  committed
  e9eddd5

  Copy full SHA for e9eddd5

Commits on Nov 13, 2023

• Fix bug: duplication error while origin is different

  Show description for 5b4f8e6
  ddjanssen

  committed
  5b4f8e6

  Copy full SHA for 5b4f8e6

• Fix: found bug with method reference and refactored permissions blocks method

  ddjanssen

  committed
  656526c

  Copy full SHA for 656526c

• Fix bug: objects dereferenced fields can now also be checked in blocks

  ddjanssen

  committed
  60a2cc6

  Copy full SHA for 60a2cc6

• Fix bug: post conditions before return statements

  ddjanssen

  committed
  d0ccabd

  Copy full SHA for d0ccabd

Commits on Nov 14, 2023

• Fix permission checking blocks for if statements and loops

  ddjanssen

  committed
  217e9fc

  Copy full SHA for 217e9fc

• Fix bug post condition checking at all return statements

  ddjanssen

  committed
  56299a1

  Copy full SHA for 56299a1

• Fix bug inner object references

  ddjanssen

  committed
  6e9e821

  Copy full SHA for 6e9e821

• Remove todo

  ddjanssen

  committed
  1feb682

  Copy full SHA for 1feb682

Commits on Nov 23, 2023

• pc change

  ddjanssen

  committed
  0f8befe

  Copy full SHA for 0f8befe

Commits on Nov 27, 2023

• add test cases

  ddjanssen

  committed
  a1caaab

  Copy full SHA for a1caaab

• Changed field permission to do both normal fields and arrays. Changed it so that it can create ledgers dynamically

  ddjanssen

  committed
  ce8c9bf

  Copy full SHA for ce8c9bf

Commits on Nov 29, 2023

• PC change

  ddjanssen

  committed
  671fb31

  Copy full SHA for 671fb31

Commits on Nov 30, 2023

• Pc change

  ddjanssen

  committed
  3df2f7b

  Copy full SHA for 3df2f7b

Commits on Dec 1, 2023

• Add: finding bounds of a quantifier is now possible

  Show description for fa2bb84
  ddjanssen

  committed
  fa2bb84

  Copy full SHA for fa2bb84

• Found mistake for quantifier

  ddjanssen

  committed
  8eb53c5

  Copy full SHA for 8eb53c5

Commits on Dec 4, 2023

• Quantifier work correctly, starall needs to be checked that the values are taken together, find a way to do this

  ddjanssen

  committed
  fbc8e7d

  Copy full SHA for fbc8e7d

Commits on Dec 5, 2023

• Quantifier in quantifier works and naming is now done for the newly created quantifiers

  ddjanssen

  committed
  fcf979c

  Copy full SHA for fcf979c

Commits on Dec 7, 2023

• Quantifier calls are now also possible

  ddjanssen

  committed
  1aee7c4

  Copy full SHA for 1aee7c4

• clean up and refactoring

  ddjanssen

  committed
  0d852fc

  Copy full SHA for 0d852fc

Commits on Dec 12, 2023

• pc switch

  ddjanssen

  committed
  60f861c

  Copy full SHA for 60f861c

Commits on Dec 13, 2023

• Pc change

  ddjanssen

  committed
  2413957

  Copy full SHA for 2413957

Commits on Dec 21, 2023

• Start on predicates

  ddjanssen

  committed
  f89a77c

  Copy full SHA for f89a77c

• pc switch

  ddjanssen

  committed
  a1f0248

  Copy full SHA for a1f0248

• Predicates and quantifiers remove errors

  ddjanssen

  committed
  d08e5bf

  Copy full SHA for d08e5bf

Commits on Jan 3, 2024

• Fix bug: nested quantifiers prev look up works again

  ddjanssen

  committed
  67a177a

  Copy full SHA for 67a177a

• Fix bug: equals method returns correct boolean value and .equals is not used on primitive types

  ddjanssen

  committed
  599611d

  Copy full SHA for 599611d

• Fix bug: arguments of the getpredicate method work now

  ddjanssen

  committed
  7b4cbdf

  Copy full SHA for 7b4cbdf

Commits on Jan 8, 2024

• Removed: unnecessary node for PredicateEquals and created an equals expr

  ddjanssen

  committed
  00de3cc

  Copy full SHA for 00de3cc

• Change: Made AbstractQuantifierRewriter to easily create new quantifiers for transferring permissions

  ddjanssen

  committed
  ad731fa

  Copy full SHA for ad731fa

Commits on Jan 10, 2024

• ADD: it is now possible to generate permission transfer on fork

  ddjanssen

  committed
  358a1b3

  Copy full SHA for 358a1b3

Commits on Jan 11, 2024

• Start on joining

  ddjanssen

  committed
  42cdd33

  Copy full SHA for 42cdd33

• ADD: postJoin to the grammar and lexer as a built in method

  ddjanssen

  committed
  7200cab

  Copy full SHA for 7200cab

Commits on Jan 15, 2024

• Changed join token to only have 1 expression instead of having multiple

  ddjanssen

  committed
  f5f5398

  Copy full SHA for f5f5398

• ADD: join and forking possible

  ddjanssen

  committed
  d2f2999

  Copy full SHA for d2f2999

• Refactor of ForkJoinPermissionTransfer

  ddjanssen

  committed
  db9a52d

  Copy full SHA for db9a52d

Commits on Jan 16, 2024

• PC switch

  ddjanssen

  committed
  914e7b6

  Copy full SHA for 914e7b6

• Resolved bug with loops creating duplicate statements

  ddjanssen

  committed
  82b33f7

  Copy full SHA for 82b33f7

• Add: loop invariants can now be tested

  ddjanssen

  committed
  8211038

  Copy full SHA for 8211038

Commits on Jan 17, 2024

• Start on transfferring permissions in quantifiers

  ddjanssen

  committed
  52805e7

  Copy full SHA for 52805e7

Commits on Jan 18, 2024

• Fix bug with inner reference for transmission transfer in arrays

  ddjanssen

  committed
  9fdef9f

  Copy full SHA for 9fdef9f

Commits on Jan 21, 2024

• Fix bug that breaks for normal methods

  ddjanssen

  committed
  5856df7

  Copy full SHA for 5856df7

• Major rework, in order to do variables properly. Transferring permissions almost work correctly for quantifiers now

  ddjanssen

  committed
  998e957

  Copy full SHA for 998e957

Commits on Jan 22, 2024

• Bug fix, this keyword correctly changed to offset. And remove of old code

  ddjanssen

  committed
  c65782c

  Copy full SHA for c65782c

• Reformat and code clean up

  ddjanssen

  committed
  ea4d335

  Copy full SHA for ea4d335

• Clean up and better template to add new functions to the predicate and some comments to better understand the code

  ddjanssen

  committed
  ece7a4c

  Copy full SHA for ece7a4c

• Removed old code

  ddjanssen

  committed
  dca73f4

  Copy full SHA for dca73f4

• Created a EnhancedLoop to recreate the getpredicate method

  ddjanssen

  committed
  d8c6612

  Copy full SHA for d8c6612

Commits on Jan 23, 2024

• PC switch

  ddjanssen

  committed
  a56023a

  Copy full SHA for a56023a

Commits on Jan 24, 2024

• quantifiers are now translated as for loops instead of function. This is syntactically easier but less clean code generation

  ddjanssen

  committed
  e40567e

  Copy full SHA for e40567e

• Fixed nested assertion checks

  ddjanssen

  committed
  2900a2b

  Copy full SHA for 2900a2b

• Loops without a body will not be created for quantifiers

  ddjanssen

  committed
  3f90a8a

  Copy full SHA for 3f90a8a

• Fixed offset for assertion checking in quantifiers

  ddjanssen

  committed
  6da5d5b

  Copy full SHA for 6da5d5b

• Add unfold method to the predicates

  ddjanssen

  committed
  0671a98

  Copy full SHA for 0671a98

• Clean up and bug fix op CreatePredicates

  ddjanssen

  committed
  4acebac

  Copy full SHA for 4acebac

Commits on Jan 25, 2024

• Node implementations for runtime put in own package

  ddjanssen

  committed
  09a46d1

  Copy full SHA for 09a46d1

• it is now possible to check if the thread holds a predicate with these paramaters

  ddjanssen

  committed
  af21cb4

  Copy full SHA for af21cb4

• Removed unused RewriteQuantifier.scala

  ddjanssen

  committed
  8b47bd7

  Copy full SHA for 8b47bd7

• Transferring predicates between threads work

  ddjanssen

  committed
  f075939

  Copy full SHA for f075939

• Clean up of the CheckPermissionsBlocksMethod

  ddjanssen

  committed
  d008f7c

  Copy full SHA for d008f7c

• Permissions are now initialized and locking is implemented as well

  ddjanssen

  committed
  d2908a8

  Copy full SHA for d2908a8

• Finalizing

  ddjanssen

  committed
  cecac30

  Copy full SHA for cecac30

Commits on Jan 26, 2024

• Add ledger example

  ddjanssen

  committed
  bd4f1c1

  Copy full SHA for bd4f1c1

• Add ledger transformer

  ddjanssen

  committed
  8881f20

  Copy full SHA for 8881f20

• Create template for CreateLedger

  ddjanssen

  committed
  ff61e18

  Copy full SHA for ff61e18

Commits on Jan 30, 2024

• Using a ledger it is possible to store permissions

  ddjanssen

  committed
  332d0be

  Copy full SHA for 332d0be

Commits on Jan 31, 2024

• ADD: Ledger locations for PrimitiveTypes can now be inserted.

  Show description for cc8b1e1
  ddjanssen

  committed
  cc8b1e1

  Copy full SHA for cc8b1e1

• Add join token to ledger

  ddjanssen

  committed
  5da6406

  Copy full SHA for 5da6406

• Predicates can now be folded and unfolded

  ddjanssen

  committed
  a6eaa70

  Copy full SHA for a6eaa70

• Fix bug in checking permissions per blocks, if the final statement has an invocation, the hasinvocation statement is not reset, not it is

  ddjanssen

  committed
  9ef71e0

  Copy full SHA for 9ef71e0

• Arrays permissions are now also being initialized

  ddjanssen

  committed
  3587688

  Copy full SHA for 3587688

Commits on Feb 7, 2024

• REMOVE: unnecessary code

  ddjanssen

  committed
  e176a75

  Copy full SHA for e176a75

• Merge remote-tracking branch 'origin/1-create-template-for-runtime-verification' into 1-create-template-for-runtime-verification

  Show description for 33e3641
  ddjanssen

  committed
  33e3641

  Copy full SHA for 33e3641

• FIX: small bugs that are occurring while executing the tests

  ddjanssen

  committed
  5365dc3

  Copy full SHA for 5365dc3

Commits on Feb 12, 2024

• FIX: new array dimensions

  ddjanssen

  committed
  058932e

  Copy full SHA for 058932e

• ADD: optional static to instanceMethod

  ddjanssen

  committed
  5e63190

  Copy full SHA for 5e63190

• ADD: optional static to instanceMethod

  ddjanssen

  committed
  aae5600

  Copy full SHA for aae5600

• ADD: optional static to instanceMethod

  ddjanssen

  committed
  c79a902

  Copy full SHA for c79a902

• FIX: bug for library fraction

  ddjanssen

  committed
  12616e4

  Copy full SHA for 12616e4

• FIX: bug naming for classes, procedure is now not taking the name anymore and is removed completely in the final step

  ddjanssen

  committed
  0ac2e35

  Copy full SHA for 0ac2e35

• FIX: offset in quantifiers condition

  ddjanssen

  committed
  d7e53af

  Copy full SHA for d7e53af

• FIX: bug permission on other fields of object

  Show description for fbd0f6a
  ddjanssen

  committed
  fbd0f6a

  Copy full SHA for fbd0f6a

Commits on Feb 13, 2024

• Change: predicates are now also in the ledger

  ddjanssen

  committed
  3400ceb

  Copy full SHA for 3400ceb

• Fix bug loop invariant

  ddjanssen

  committed
  c752ea8

  Copy full SHA for c752ea8

Commits on Feb 19, 2024

• Fix final bugs

  ddjanssen

  committed
  b64b25f

  Copy full SHA for b64b25f

• Fix final bugs

  ddjanssen

  committed
  d7d9406

  Copy full SHA for d7d9406

• Fix final bugs

  ddjanssen

  committed
  207b857

  Copy full SHA for 207b857

Commits on Feb 22, 2024

• Fixed bugs and moved the GenerateJava to the codegeneration step to transform the program to an as close as possible executable file

  ddjanssen

  committed
  4fb25be

  Copy full SHA for 4fb25be

• Fix injectivitymap check for duplicates

  ddjanssen

  committed
  717eba9

  Copy full SHA for 717eba9

Commits on Feb 26, 2024

• Update message with line numbers

  ddjanssen

  committed
  24a1755

  Copy full SHA for 24a1755

Commits on Feb 27, 2024

• Fixed bugs (un)fold

  ddjanssen

  committed
  a7bac02

  Copy full SHA for a7bac02

• Add comments to the code

  ddjanssen

  committed
  a819229

  Copy full SHA for a819229

Commits on Mar 14, 2024

• Fixed tiny bug in code

  ddjanssen

  committed
  822e74d

  Copy full SHA for 822e74d

Commits on Mar 25, 2024

• Loopinvariant only check on continue keyword and not return or break keywords

  ddjanssen

  committed
  56fe703

  Copy full SHA for 56fe703

• Loopinvariant only check on continue or break keywords and not return keyword

  ddjanssen

  committed
  5f3811f

  Copy full SHA for 5f3811f

Commits on Apr 3, 2024

• Should only be continue, checked again, also at other languages

  ddjanssen

  committed
  17bce44

  Copy full SHA for 17bce44

Commits on May 21, 2024

• Merge branch 'dev' into 1-create-template-for-runtime-verification

  pieter-bos

  committed
  d138138

  Copy full SHA for d138138

Commits on May 22, 2024

• fixes up to needing new-style constructors

  pieter-bos

  committed
  a81bbc2

  Copy full SHA for a81bbc2

• Merge branch 'dev' into 1-create-template-for-runtime-verification

  pieter-bos

  committed
  e4a5f97

  Copy full SHA for e4a5f97

Commits on May 23, 2024

• clean up some nodes

  pieter-bos

  committed
  cf52842

  Copy full SHA for cf52842