Code

Issue 448#450

Code

Merged

danmatichuk merged 36 commits intomasterGaloisInc/pate:masterfrom issue-448GaloisInc/pate:issue-448Copy head branch name to clipboardJan 10, 2025

+2,370-555

Commits

Commits on Dec 11, 2024

• add FnBindings module representing post-hoc defined functions

  danmatichuk

  committed
  9620ea8

  Copy full SHA for 9620ea8

• overhaul the control flow sync/merge logic to use uninterpreted functions

  Show description for 8016376
  danmatichuk

  committed
  8016376

  Copy full SHA for 8016376

• Use BoundVars in FnBindings rather than SymFn to work around grounding issues

  danmatichuk

  committed
  cd2100c

  Copy full SHA for cd2100c

• FnBindings: use bound variables instead of functions

  Show description for 6f3c8bb
  danmatichuk

  committed
  6f3c8bb

  Copy full SHA for 6f3c8bb

• WIP: handleProcessMerge is over-widening at the moment, see TODO

  danmatichuk

  committed
  206e308

  Copy full SHA for 206e308

• FnBindings: don't generate uninterpreted functions for concrete values

  Show description for 0af3e98
  danmatichuk

  committed
  0af3e98

  Copy full SHA for 0af3e98

• drop implicit SimSpec wrapping from 'withFreshScope'

  Show description for e3df8b8
  danmatichuk

  committed
  e3df8b8

  Copy full SHA for e3df8b8

• remove deprecaded 'scopeAsm' field from 'SimScope'

  danmatichuk

  committed
  92813a6

  Copy full SHA for 92813a6

• add "composite" scopes to handle mixing variables from

  Show description for 45e49ba
  danmatichuk

  committed
  45e49ba

  Copy full SHA for 45e49ba

• WIP: rework control flow merge logic to use mixed scopes

  danmatichuk

  committed
  d688d9e

  Copy full SHA for d688d9e

• add desync-assert tests

  danmatichuk

  committed
  a01f3ba

  Copy full SHA for a01f3ba

• resolve merge artifacts from Data.Quant

  danmatichuk

  committed
  0f3ab93

  Copy full SHA for 0f3ab93

• more Node generalizations

  danmatichuk

  committed
  d49e7c5

  Copy full SHA for d49e7c5

• WIP: transplant function binding propagation

  danmatichuk

  committed
  5a6d730

  Copy full SHA for 5a6d730

Commits on Dec 12, 2024

• more Quant refinements

  danmatichuk

  committed
  8157622

  Copy full SHA for 8157622

• pull in rewriteStrategy

  danmatichuk

  committed
  1ed1b2c

  Copy full SHA for 1ed1b2c

Commits on Dec 13, 2024

• Data.Quant: misc interface changes

  danmatichuk

  committed
  43c8754

  Copy full SHA for 43c8754

Commits on Dec 18, 2024

• properly track divergence points for single-sided nodes

  Show description for d652078
  danmatichuk

  committed
  d652078

  Copy full SHA for d652078

Commits on Jan 6, 2025

• use global uninterpreted function to define "caller" stack base for return site bundle

  Show description for 89fa195
  danmatichuk

  committed
  89fa195

  Copy full SHA for 89fa195

• always add divergence point when combining single-sided nodes

  Show description for 8d6da88
  danmatichuk

  committed
  8d6da88

  Copy full SHA for 8d6da88

• avoid scheduling loop when re-processing control flow divergence

  Show description for 66ed8ef
  danmatichuk

  committed
  66ed8ef

  Copy full SHA for 66ed8ef

• rewrite propagated assertion using function bindings

  Show description for c9937d6
  danmatichuk

  committed
  c9937d6

  Copy full SHA for c9937d6

• add debugging information when function bindings need to be propagated

  danmatichuk

  committed
  eab0181

  Copy full SHA for eab0181

Commits on Jan 7, 2025

• add type-level case distinction for QuantK

  danmatichuk

  committed
  6b4b247

  Copy full SHA for 6b4b247

• drop divergence point from two-sided nodes

  Show description for ba4e782
  danmatichuk

  committed
  ba4e782

  Copy full SHA for ba4e782

• avoid implicit condition propagation when widening between one and two sided nodes

  danmatichuk

  committed
  47ab6aa

  Copy full SHA for 47ab6aa

Commits on Jan 8, 2025

• queue ancestors of divergence point when propagating assertions

  danmatichuk

  committed
  9132cfe

  Copy full SHA for 9132cfe

• ensure that fresh domains have the expected original/patched shape

  danmatichuk

  committed
  7f1839b

  Copy full SHA for 7f1839b

• desync-zerostep: set desync to be before pushing any arguents to the stack

  danmatichuk

  committed
  adb874a

  Copy full SHA for adb874a

Commits on Jan 10, 2025

• fix symbolic pointer support when adding domain refinements

  Show description for 739dc5d
  danmatichuk

  committed
  739dc5d

  Copy full SHA for 739dc5d

• queueSyncNodeMerge: fix after dropping diverge points from two-sided nodes

  Show description for 023739c
  danmatichuk

  committed
  023739c

  Copy full SHA for 023739c

• use a runtime error when expected quantifier convertion fails

  danmatichuk

  committed
  79732d9

  Copy full SHA for 79732d9

• ignore "handleMerge" flag when scheduling single-sided sync points

  Show description for ad19598
  danmatichuk

  committed
  ad19598

  Copy full SHA for ad19598

• add informative error message when a scheduled node has no domain

  danmatichuk

  committed
  9dd8ad8

  Copy full SHA for 9dd8ad8

• give Inequivalent result when entry point has unsolved assertions

  danmatichuk

  committed
  3111d0a

  Copy full SHA for 3111d0a

• add desync-assert test

  danmatichuk

  committed
  65e5208

  Copy full SHA for 65e5208