Code

Adding Memory Regions to IR#231

Code

Merged

l-kent merged 73 commits intomainUQ-PAC/BASIL:mainfrom

yousif-fixMemoryInjectionUQ-PAC/BASIL:yousif-fixMemoryInjectionCopy head branch name to clipboard

Oct 30, 2024

Commits

Commits on May 1, 2024

• Injecting memory regions into IR

  yousifpatti

  committed
  5bd765a

  Copy full SHA for 5bd765a

Commits on May 17, 2024

• Loop handling in MRA (using depth for now)

  yousifpatti

  committed
  e878a76

  Copy full SHA for e878a76

Commits on Jun 17, 2024

• Initial Works on VSA

  yousifpatti

  committed
  d23172d

  Copy full SHA for d23172d

Commits on Jun 26, 2024

• Changes to partial region accesses

  yousifpatti

  committed
  c0be95b

  Copy full SHA for c0be95b

Commits on Aug 13, 2024

• Adding regions into IR

  yousifpatti

  committed
  55f9bd8

  Copy full SHA for 55f9bd8

• Merging only region injection files

  yousifpatti

  committed
  834f34e

  Copy full SHA for 834f34e

• Fixed Small Bugs

  yousifpatti

  committed
  f607fdf

  Copy full SHA for f607fdf

• Dont ignore regions

  yousifpatti

  committed
  5a20e37

  Copy full SHA for 5a20e37

Commits on Aug 19, 2024

• Changes to consider local variables and initial offsets of a procedure

  yousifpatti

  committed
  f798374

  Copy full SHA for f798374

Commits on Aug 20, 2024

• Adding condition to disable stackIdentification

  yousifpatti

  committed
  65e6ff7

  Copy full SHA for 65e6ff7

• Fixed not loaded data regions

  yousifpatti

  committed
  20f9cf6

  Copy full SHA for 20f9cf6

Commits on Aug 21, 2024

• Fixed duplicate addresses causing tests to fail

  yousifpatti

  committed
  ac906b9

  Copy full SHA for ac906b9

Commits on Aug 22, 2024

• Initial VSA work

  yousifpatti

  committed
  89cf1c7

  Copy full SHA for 89cf1c7

• Injecting memory regions into IR

  yousifpatti

  committed
  5ec6d7c

  Copy full SHA for 5ec6d7c

• Loop handling in MRA (using depth for now)

  yousifpatti

  committed
  cee69a2

  Copy full SHA for cee69a2

• Initial Works on VSA

  yousifpatti

  committed
  aee3d46

  Copy full SHA for aee3d46

• Changes to partial region accesses

  yousifpatti

  committed
  12df143

  Copy full SHA for 12df143

• Adding regions into IR

  yousifpatti

  committed
  5c0619e

  Copy full SHA for 5c0619e

• Initial VSA work

  yousifpatti

  committed
  f623faa

  Copy full SHA for f623faa

Commits on Aug 23, 2024

• Merge fixes

  yousifpatti

  committed
  6ac45fc

  Copy full SHA for 6ac45fc

• Merge branch 'yousif-VSA' of https://github.com/UQ-PAC/bil-to-boogie-translator into yousif-VSA

  yousifpatti

  committed
  0e47d64

  Copy full SHA for 0e47d64

• Merge branch 'yousif-fixMemoryInjection' into yousif-VSA

  yousifpatti

  committed
  b0853bc

  Copy full SHA for b0853bc

• Fixed MRA loop bug

  yousifpatti

  committed
  6e1b51d

  Copy full SHA for 6e1b51d

• Merge branch 'main' into yousif-VSA

  yousifpatti

  committed
  90c1b36

  Copy full SHA for 90c1b36

• ReEnabled shared regions

  yousifpatti

  committed
  745245d

  Copy full SHA for 745245d

Commits on Sep 3, 2024

• Handling negatives and using BigInts instead

  yousifpatti

  committed
  5a8d5e3

  Copy full SHA for 5a8d5e3

Commits on Sep 5, 2024

• Added sub-accesses to approximate stack region sizes

  yousifpatti

  committed
  6a74737

  Copy full SHA for 6a74737

• Corrected negative addresses

  yousifpatti

  committed
  0e0a98c

  Copy full SHA for 0e0a98c

Commits on Sep 8, 2024

• Added sizes to global regions

  yousifpatti

  committed
  250fdee

  Copy full SHA for 250fdee

Commits on Sep 9, 2024

• A fix for global accesses

  yousifpatti

  committed
  a873a06

  Copy full SHA for a873a06

Commits on Sep 12, 2024

• faster MMM and heap support

  yousifpatti

  committed
  3df153a

  Copy full SHA for 3df153a

• Heap region tracking using points-to

  yousifpatti

  committed
  40074fd

  Copy full SHA for 40074fd

Commits on Sep 16, 2024

• Merging regions at start

  yousifpatti

  committed
  52e0bb7

  Copy full SHA for 52e0bb7

• Update UtilMethods.scala

  yousifpatti

  committed
  fb2aa27

  Copy full SHA for fb2aa27

Commits on Sep 17, 2024

• Using simple constantProp

  yousifpatti

  committed
  a791d5f

  Copy full SHA for a791d5f

Commits on Sep 18, 2024

• Merge branch 'main' into memory-region-boogie

  Show description for c8537c0
  

  l-kent

  committed
  c8537c0

  Copy full SHA for c8537c0

Commits on Sep 20, 2024

• Fixed regression bug for jumptable2

  yousifpatti

  committed
  79b6259

  Copy full SHA for 79b6259

Commits on Sep 26, 2024

• cleanup analyses + remove unused 'sharedVariable' in Variable

  

  l-kent

  committed
  4b634c3

  Copy full SHA for 4b634c3

• zero out bss sections

  

  l-kent

  committed
  cd9fe8b

  Copy full SHA for cd9fe8b

• replace memory accesses in boogie pre/post conditions with identified memory regions

  

  l-kent

  committed
  264fca0

  Copy full SHA for 264fca0

Commits on Sep 30, 2024

• Changes in MRA and made Reaching def interproc

  yousifpatti

  committed
  846b020

  Copy full SHA for 846b020

Commits on Oct 1, 2024

• Merge branch 'yousif-fixMemoryInjection' into memory-region-boogie

  Show description for 75d871f
  

  l-kent

  committed
  75d871f

  Copy full SHA for 75d871f

Commits on Oct 14, 2024

• handle regions with size < 64 bits correctly

  

  l-kent

  committed
  98d8b92

  Copy full SHA for 98d8b92

• include memory regions in renaming to avoid boogie keywords

  

  l-kent

  committed
  eadcf67

  Copy full SHA for eadcf67

Commits on Oct 17, 2024

• Added GRA

  yousifpatti

  committed
  733cd0b

  Copy full SHA for 733cd0b

• Merge branch 'yousif-VSA' into yousif-fixAnalysis

  yousifpatti

  committed
  19e4d60

  Copy full SHA for 19e4d60

• Better Data Region Approximation

  yousifpatti

  committed
  72c238e

  Copy full SHA for 72c238e

• VSA results feedback

  yousifpatti

  committed
  874b5b0

  Copy full SHA for 874b5b0

Commits on Oct 21, 2024

• Handling multiple regions

  yousifpatti

  committed
  71f1cba

  Copy full SHA for 71f1cba

Commits on Oct 22, 2024

• use visitor to resolve specification variables

  

  l-kent

  committed
  277a3fc

  Copy full SHA for 277a3fc

• fix mistake in SystemTests

  

  l-kent

  committed
  8612486

  Copy full SHA for 8612486

• add regions to boogie output for specifications and guarantees

  

  l-kent

  committed
  b228b7f

  Copy full SHA for b228b7f

Commits on Oct 23, 2024

• add regions to boogie output for rely

  

  l-kent

  committed
  d601a51

  Copy full SHA for d601a51

• correct regions in Boogie output for secure update and guarantee checks, remove guarantee checks relating to unused variables

  

  l-kent

  committed
  e4e2682

  Copy full SHA for e4e2682

• properly collect Boogie global variables

  

  l-kent

  committed
  cbbe539

  Copy full SHA for cbbe539

• have L function in Boogie take in all relevant memories as parameters, comment out SummaryGenerator since it needs significant work to be compatible with these changes

  

  l-kent

  committed
  6aa0f42

  Copy full SHA for 6aa0f42

• prevent stack being added to rely

  

  l-kent

  committed
  74e4810

  Copy full SHA for 74e4810

Commits on Oct 25, 2024

• Cleanup

  yousifpatti

  committed
  53e5ad9

  Copy full SHA for 53e5ad9

Commits on Oct 28, 2024

• Merge branch 'yousif-fixMemoryInjection' into memory-region-boogie

  Show description for 106737d
  

  l-kent

  committed
  106737d

  Copy full SHA for 106737d

• re-enable procedure summaries

  

  l-kent

  committed
  d0ca3ac

  Copy full SHA for d0ca3ac

• Merge branch 'main' into memory-region-boogie

  Show description for 717b645
  

  l-kent

  committed
  717b645

  Copy full SHA for 717b645

Commits on Oct 29, 2024

• Fixes to pointers-to-pointers

  yousifpatti

  committed
  46b144c

  Copy full SHA for 46b144c

• Merge branch 'yousif-fixMemoryInjection' into memory-region-boogie

  Show description for 8cb5e2a
  

  l-kent

  committed
  8cb5e2a

  Copy full SHA for 8cb5e2a

• general clean up

  

  l-kent

  committed
  937cfc2

  Copy full SHA for 937cfc2

Commits on Oct 30, 2024

• remove mutability in DataRegion case class

  

  l-kent

  committed
  dabf9f9

  Copy full SHA for dabf9f9

• remove mutability in StackRegion case class

  

  l-kent

  committed
  af29cc1

  Copy full SHA for af29cc1

• add --memory-regions flag to control whether regions are added to Boogie

  

  l-kent

  committed
  250d9c7

  Copy full SHA for 250d9c7

• Merge pull request #262 from UQ-PAC/memory-region-boogie

  Show description for 162da67
  l-kent

  authored
  162da67

  Copy full SHA for 162da67

• don't do multiple iterations unless needed for regions

  

  l-kent

  committed
  d1c0870

  Copy full SHA for d1c0870

• fix issue with L function when analysis is off

  

  l-kent

  committed
  c6e5d8a

  Copy full SHA for c6e5d8a

• fix issue with initialised memory and stack when analysis is enabled

  

  l-kent

  committed
  dc1668e

  Copy full SHA for dc1668e

• update expected

  

  l-kent

  committed
  19dcdb0

  Copy full SHA for 19dcdb0

• Merge branch 'memory-region-boogie' into yousif-fixMemoryInjection

  

  l-kent

  committed
  ba13989

  Copy full SHA for ba13989