Code

Transformer based memory model#4

Code

Draft

2over12 wants to merge 110 commits intomastertrail-of-forks/Gillian:masterfrom ian/pointer-memory-modeltrail-of-forks/Gillian:ian/pointer-memory-modelCopy head branch name to clipboard

+5,454-1,595

Commits

Commits on Jan 17, 2025

• add bplus syntactic form

  2over12

  committed
  7d41b7d

  Copy full SHA for 7d41b7d

• new expr form for bvs

  2over12

  committed
  4cc3506

  Copy full SHA for 4cc3506

• more bitvectors

  2over12

  committed
  d867c21

  Copy full SHA for d867c21

• type inference

  2over12

  committed
  044fd3a

  Copy full SHA for 044fd3a

• bv type visitors

  2over12

  committed
  f71e567

  Copy full SHA for f71e567

• smt translation

  2over12

  committed
  cc3a255

  Copy full SHA for cc3a255

• declare bv stuff

  2over12

  committed
  c610e53

  Copy full SHA for c610e53

• actually call decls

  2over12

  committed
  e1b9a6a

  Copy full SHA for e1b9a6a

• handle in sstate

  2over12

  committed
  fb15532

  Copy full SHA for fb15532

• stub normalizer

  2over12

  committed
  899d620

  Copy full SHA for 899d620

• noop reductions

  2over12

  committed
  20cb9ea

  Copy full SHA for 20cb9ea

• fix construction when no bvs

  2over12

  committed
  207b084

  Copy full SHA for 207b084

• add add encodings

  2over12

  committed
  efea9f4

  Copy full SHA for efea9f4

• Fix overlapping cons

  2over12

  committed
  86cfea7

  Copy full SHA for 86cfea7

• add ops

  2over12

  committed
  90dde0d

  Copy full SHA for 90dde0d

• typed expressions for bv instrinsic

  2over12

  committed
  c898317

  Copy full SHA for c898317

• fix types

  2over12

  committed
  d12a2a4

  Copy full SHA for d12a2a4

• fix parser

  2over12

  committed
  c860369

  Copy full SHA for c860369

• refactor to have preds

  2over12

  committed
  f99eb4a

  Copy full SHA for f99eb4a

• make visitors less painful

  2over12

  committed
  0e08a53

  Copy full SHA for 0e08a53

• more visitor fixes

  2over12

  committed
  f917d2e

  Copy full SHA for f917d2e

• implement typing

  2over12

  committed
  6a25665

  Copy full SHA for 6a25665

• matching plan

  2over12

  committed
  79188ab

  Copy full SHA for 79188ab

• norm

  2over12

  committed
  93fb86a

  Copy full SHA for 93fb86a

• mor norm

  2over12

  committed
  a6ed95c

  Copy full SHA for a6ed95c

• more type fixes

  2over12

  committed
  f691a20

  Copy full SHA for f691a20

• even more types

  2over12

  committed
  092e370

  Copy full SHA for 092e370

• more

  2over12

  committed
  d7d7e23

  Copy full SHA for d7d7e23

• fixes for types, implement extract

  2over12

  committed
  26ce163

  Copy full SHA for 26ce163

• add form parsing

  2over12

  committed
  365a720

  Copy full SHA for 365a720

• encode assertions

  2over12

  committed
  61f1d5a

  Copy full SHA for 61f1d5a

• stubs

  2over12

  committed
  f40973d

  Copy full SHA for f40973d

• remove chunks

  2over12

  committed
  7cf60be

  Copy full SHA for 7cf60be

• bv literals

  2over12

  committed
  febccfc

  Copy full SHA for febccfc

• wrapper bv

  2over12

  committed
  426932f

  Copy full SHA for 426932f

• more sval implementations

  2over12

  committed
  04a7326

  Copy full SHA for 04a7326

• implement cast

  2over12

  committed
  47950f4

  Copy full SHA for 47950f4

• fix decode as sval

  2over12

  committed
  d15f94e

  Copy full SHA for d15f94e

• fix value -> array

  2over12

  committed
  636a8b9

  Copy full SHA for 636a8b9

• rename

  2over12

  committed
  26908df

  Copy full SHA for 26908df

• fix

  2over12

  committed
  2ecda3e

  Copy full SHA for 2ecda3e

• cg logging...

  2over12

  committed
  a32d549

  Copy full SHA for a32d549

• hacky fix for callgraph

  2over12

  committed
  949c954

  Copy full SHA for 949c954

• fix semantics of branching

  2over12

  committed
  347e5e4

  Copy full SHA for 347e5e4

• only preserve basic ci

  2over12

  committed
  15dd551

  Copy full SHA for 15dd551

• remove prints

  2over12

  committed
  383edbe

  Copy full SHA for 383edbe

• flip to optional

  2over12

  committed
  6d5d145

  Copy full SHA for 6d5d145

• add whole program symbolic test runner

  2over12

  committed
  04f4631

  Copy full SHA for 04f4631

• add bulk wpst to workflow

  2over12

  committed
  c0dee46

  Copy full SHA for c0dee46

• add gil_test

  2over12

  committed
  6e3161f

  Copy full SHA for 6e3161f

• fix git ignore

  2over12

  committed
  b938a56

  Copy full SHA for b938a56

• try to fix linking when cached

  2over12

  committed
  555435a

  Copy full SHA for 555435a

• dont waste storage

  2over12

  committed
  d88ae0e

  Copy full SHA for d88ae0e

• sudo

  2over12

  committed
  f7b2b19

  Copy full SHA for f7b2b19

• add more binop encodings

  2over12

  committed
  ee835e6

  Copy full SHA for ee835e6

• add unop encodings

  2over12

  committed
  303fc21

  Copy full SHA for 303fc21

• remove unneeded case

  2over12

  committed
  8ed3a38

  Copy full SHA for 8ed3a38

• add backend xor srem sub

  2over12

  committed
  d694f34

  Copy full SHA for d694f34

• add parser for xor srem and sub

  2over12

  committed
  ec3e885

  Copy full SHA for ec3e885

• backend preds uleq slt sleq

  2over12

  committed
  a47d223

  Copy full SHA for a47d223

• add parser bvuleq bvslt bvsleq

  2over12

  committed
  9e06624

  Copy full SHA for 9e06624

• add backend for BVSignExtend|BVZeroExtend|BVSdiv|BVSmod|BVAshr

  2over12

  committed
  808a15b

  Copy full SHA for 808a15b

• parser for sext zext sdiv smod and ashr

  2over12

  committed
  2a6a616

  Copy full SHA for 2a6a616

• use fork with overflow preds

  2over12

  committed
  569a82a

  Copy full SHA for 569a82a

• add bv preds

  2over12

  committed
  554f595

  Copy full SHA for 554f595

Commits on Jan 18, 2025

• fixes

  2over12

  committed
  9923f42

  Copy full SHA for 9923f42

• builds

  2over12

  committed
  698c67c

  Copy full SHA for 698c67c

• fix types

  2over12

  committed
  9017a68

  Copy full SHA for 9017a68

• implement type checking for preds

  2over12

  committed
  7f749d2

  Copy full SHA for 7f749d2

• update parser

  2over12

  committed
  b8eaaca

  Copy full SHA for b8eaaca

• fix test

  2over12

  committed
  ca637de

  Copy full SHA for ca637de

• remove runtime:

  2over12

  committed
  46e9218

  Copy full SHA for 46e9218

• remove runtime from dune

  2over12

  committed
  7731417

  Copy full SHA for 7731417

Commits on Jan 23, 2025

• building transformer model

  2over12

  committed
  5361b6a

  Copy full SHA for 5361b6a

Commits on Jan 24, 2025

• modify chunk

  2over12

  committed
  06193bd

  Copy full SHA for 06193bd

• use C2 wrapped in trasnformer

  2over12

  committed
  82259a8

  Copy full SHA for 82259a8

• more mem model

  2over12

  committed
  ba7685c

  Copy full SHA for ba7685c

• implement free check

  2over12

  committed
  3445c66

  Copy full SHA for 3445c66

Commits on Jan 27, 2025

• working on intefaces

  2over12

  committed
  cf5fb07

  Copy full SHA for cf5fb07

• fix heap tree

  2over12

  committed
  956dca7

  Copy full SHA for 956dca7

• builds

  2over12

  committed
  20205d1

  Copy full SHA for 20205d1

Commits on Jan 28, 2025

• fix memory model bug

  2over12

  committed
  e8e88f5

  Copy full SHA for e8e88f5

• test runs

  2over12

  committed
  7b08bd5

  Copy full SHA for 7b08bd5

Commits on Jan 29, 2025

• assertions others

  2over12

  committed
  9820678

  Copy full SHA for 9820678

Commits on Jan 30, 2025

• fix root updates

  2over12

  committed
  07d9750

  Copy full SHA for 07d9750

• fix type learning

  2over12

  committed
  4d0107a

  Copy full SHA for 4d0107a

• fix width

  2over12

  committed
  517404c

  Copy full SHA for 517404c

• add intorptr

  2over12

  committed
  65a8380

  Copy full SHA for 65a8380

• enforce resulting type on loaded value

  2over12

  committed
  6f6a5c2

  Copy full SHA for 6f6a5c2

• add comment labeling issue

  2over12

  committed
  a4f0df4

  Copy full SHA for a4f0df4

• fix learned

  2over12

  committed
  78e7ba2

  Copy full SHA for 78e7ba2

Commits on Jan 31, 2025

• update memory model to do typechecking

  2over12

  committed
  c1c87d0

  Copy full SHA for c1c87d0

Commits on Feb 3, 2025

• retarget tests

  2over12

  committed
  229f331

  Copy full SHA for 229f331

• gil_parser: add BV literals

  Show description for 4798b92
  tnytown

  committed
  4798b92

  Copy full SHA for 4798b92

• fixed lift model?

  2over12

  committed
  6b387b0

  Copy full SHA for 6b387b0

• gil_parser: accept hex digits for bv literals

  Show description for 9275487
  tnytown

  committed
  9275487

  Copy full SHA for 9275487

• hacky tester

  2over12

  committed
  a72900e

  Copy full SHA for a72900e

• Merge pull request #5 from trail-of-forks/andrew/bv-literal-syntax

  Show description for af81f07
  2over12

  authored
  af81f07

  Copy full SHA for af81f07

Commits on Feb 5, 2025

• branch on any creation

  2over12

  committed
  2845462

  Copy full SHA for 2845462

• type candidates abduce

  2over12

  committed
  7ff7497

  Copy full SHA for 7ff7497

• more type fixes

  2over12

  committed
  2878687

  Copy full SHA for 2878687

• fix test

  2over12

  committed
  c9ba75d

  Copy full SHA for c9ba75d

• rename-test

  2over12

  committed
  cc92f86

  Copy full SHA for cc92f86

• allow biadbductive axiomatic specs

  2over12

  committed
  9521854

  Copy full SHA for 9521854

• fix mem_test

  2over12

  committed
  36bfd35

  Copy full SHA for 36bfd35

• brief fix

  2over12

  committed
  10a0a61

  Copy full SHA for 10a0a61

• re-enable recogs

  2over12

  committed
  3c359f8

  Copy full SHA for 3c359f8

• fix simple wrap encoding

  2over12

  committed
  ca1696f

  Copy full SHA for ca1696f

• fix typeof

  2over12

  committed
  0d57edb

  Copy full SHA for 0d57edb

Commits on Feb 6, 2025

• add bug specs to the syntax

  2over12

  committed
  5ebf2bc

  Copy full SHA for 5ebf2bc