Code

Optimizations using caching#453

Code

Merged

danmatichuk merged 16 commits intomasterGaloisInc/pate:masterfrom dm/optimizeGaloisInc/pate:dm/optimizeCopy head branch name to clipboardOct 28, 2024

+780-187

Commits

Commits on Oct 14, 2024

• add "time" tag to display processing time for TraceTree elements

  danmatichuk

  committed
  b0cadef

  Copy full SHA for b0cadef

Commits on Oct 18, 2024

• re-enable parsedFunction cache, conservatively flushing for each node

  Show description for 42ca7c7
  danmatichuk

  committed
  42ca7c7

  Copy full SHA for 42ca7c7

• add first-pass filter for concretizing memory writes

  danmatichuk

  committed
  39c3f02

  Copy full SHA for 39c3f02

Commits on Oct 21, 2024

• ParsedFunctions: track function cache validity instead of flushing

  Show description for fde2e5c
  danmatichuk

  committed
  fde2e5c

  Copy full SHA for fde2e5c

• cleanup merge artifact

  danmatichuk

  committed
  15dbfd2

  Copy full SHA for 15dbfd2

• Repl: output duration when using "status" command

  danmatichuk

  committed
  de0a065

  Copy full SHA for de0a065

Commits on Oct 24, 2024

• use batch processing when initializing abstract value domain

  Show description for e010f58
  danmatichuk

  committed
  e010f58

  Copy full SHA for e010f58

• Experimenting with some limited parallelism in simple cases

  danmatichuk

  committed
  fcb2f7c

  Copy full SHA for fcb2f7c

Commits on Oct 25, 2024

• fixup packet integration test

  danmatichuk

  committed
  49c7eeb

  Copy full SHA for 49c7eeb

• fix bug where nodes were not outputted during 'wait' unless

  Show description for 7500e0c
  danmatichuk

  committed
  7500e0c

  Copy full SHA for 7500e0c

• initAbsDomainVals: handle case where a cell has multiple writes, with only some concrete

  Show description for 6ecb882
  danmatichuk

  committed
  6ecb882

  Copy full SHA for 6ecb882

• disable simplifcation of 'SimBundle'

  Show description for 65a18a9
  danmatichuk

  committed
  65a18a9

  Copy full SHA for 65a18a9

• allow forked solver instances to share the sat/unsat cache

  Show description for d19920a
  danmatichuk

  committed
  d19920a

  Copy full SHA for d19920a

• move 'asScopedConst' to last rescoping strategy

  Show description for b7c0b16
  danmatichuk

  committed
  b7c0b16

  Copy full SHA for b7c0b16

Commits on Oct 28, 2024

• use Crucible's assumption/frames to initialize forked solver state

  Show description for 97d1c09
  danmatichuk

  committed
  97d1c09

  Copy full SHA for 97d1c09

• concretize: add explicit positivity assumptions for integers

  Show description for c923ac3
  danmatichuk

  committed
  c923ac3

  Copy full SHA for c923ac3