Code

Integrate type inf#1

Code

Open

yelhsams wants to merge 88 commits intowellesley-prog-sys:verify-mainwellesley-prog-sys/wasmtime:verify-mainfrom yelhsams:integrate-type-infyelhsams/wasmtime:integrate-type-infCopy head branch name to clipboard

+16,111-142

Commits

Commits on Feb 2, 2024

• debugging

  mmcloughlin

  committed
  c33c1b3

  Copy full SHA for c33c1b3

Commits on Feb 6, 2024

• skeleton of smt-based TypeSolver

  mmcloughlin

  committed
  7fdf7fa

  Copy full SHA for 7fdf7fa

• implement WidthOf

  mmcloughlin

  committed
  61d9621

  Copy full SHA for 61d9621

• assert integer values

  mmcloughlin

  committed
  5656b54

  Copy full SHA for 5656b54

• deduce types from model

  mmcloughlin

  committed
  e16a2b4

  Copy full SHA for e16a2b4

Commits on Feb 7, 2024

• assert equivalence with unify output

  mmcloughlin

  committed
  d45db47

  Copy full SHA for d45db47

Commits on Feb 9, 2024

• fix symbolic type invariants

  mmcloughlin

  committed
  46a7d66

  Copy full SHA for 46a7d66

• check smt result vs dynwidths solver

  mmcloughlin

  committed
  76188df

  Copy full SHA for 76188df

Commits on Feb 18, 2024

• Fix tests of encoded ops (avanhatt#94)

  avanhatt

  authored
  e6a8f75

  Copy full SHA for e6a8f75

• all: revive veri ci job (avanhatt#93)

  Show description for b5f113c
  mmcloughlin

  authored
  b5f113c

  Copy full SHA for b5f113c

Commits on Feb 19, 2024

• veri: fix bug in BVShr type inference (avanhatt#95)

  Show description for 487e2b3
  mmcloughlin

  authored
  487e2b3

  Copy full SHA for 487e2b3

• skeleton isla tool

  mmcloughlin

  committed
  5190aae

  Copy full SHA for 5190aae

• integrate isla

  mmcloughlin

  committed
  1c8692a

  Copy full SHA for 1c8692a

• it builds

  mmcloughlin

  committed
  f4af432

  Copy full SHA for f4af432

• get smt out

  mmcloughlin

  committed
  25e85ba

  Copy full SHA for 25e85ba

• trying to get multiple opcodes to work

  mmcloughlin

  committed
  aa70c44

  Copy full SHA for aa70c44

• emit Inst to opcodes

  mmcloughlin

  committed
  7c432e0

  Copy full SHA for 7c432e0

• Inst to ISLA trace

  mmcloughlin

  committed
  8a9082e

  Copy full SHA for 8a9082e

• anyhow::bail

  mmcloughlin

  committed
  943bd86

  Copy full SHA for 943bd86

• veri: slight refactor isla emit

  mmcloughlin

  committed
  173bb50

  Copy full SHA for 173bb50

• veri: isla emit tree shake

  mmcloughlin

  committed
  565f70f

  Copy full SHA for 565f70f

• use todo!

  mmcloughlin

  committed
  6c1bebf

  Copy full SHA for 6c1bebf

• start adhoc tool to experiment with x64 isla

  mmcloughlin

  committed
  ee2655c

  Copy full SHA for ee2655c

• copypasta isla logic into x86

  mmcloughlin

  committed
  d44f3b1

  Copy full SHA for d44f3b1

• attempting to make x64 work

  mmcloughlin

  committed
  a0e811a

  Copy full SHA for a0e811a

• first working trace output for x86

  mmcloughlin

  committed
  63d64e3

  Copy full SHA for 63d64e3

• write x64 traces to files

  mmcloughlin

  committed
  9358c6b

  Copy full SHA for 9358c6b

• linearization

  mmcloughlin

  committed
  2b24eb5

  Copy full SHA for 2b24eb5

• disable simplify::hide_initialization

  Show description for b68e55b
  mmcloughlin

  committed
  b68e55b

  Copy full SHA for b68e55b

• emit: add a selection of instructions

  mmcloughlin

  committed
  72fa499

  Copy full SHA for 72fa499

• optionally show full traces

  mmcloughlin

  committed
  f379221

  Copy full SHA for f379221

• update emit tool to use isla options

  mmcloughlin

  committed
  ba61ba7

  Copy full SHA for ba61ba7

• support filtering for ITE and struct reads

  mmcloughlin

  committed
  e7897da

  Copy full SHA for e7897da

• post-filter simplify

  mmcloughlin

  committed
  837e59b

  Copy full SHA for 837e59b

• account for PSTATE register writes

  mmcloughlin

  committed
  447f355

  Copy full SHA for 447f355

• type inference: support "extra" spec variables

  mmcloughlin

  committed
  0c06bfd

  Copy full SHA for 0c06bfd

• isle: printer skeleton

  mmcloughlin

  committed
  ad20e6e

  Copy full SHA for ad20e6e

• isle: type printing

  mmcloughlin

  committed
  d6ee519

  Copy full SHA for d6ee519

• isle: printer supports more things

  mmcloughlin

  committed
  8ed0d01

  Copy full SHA for 8ed0d01

• isle: more printing

  mmcloughlin

  committed
  81e1fb6

  Copy full SHA for 81e1fb6

• isle: more spec printing

  mmcloughlin

  committed
  f491dfb

  Copy full SHA for f491dfb

• isle: more printing

  mmcloughlin

  committed
  1ff75fc

  Copy full SHA for 1ff75fc

• isle: print if-let

  mmcloughlin

  committed
  ba0a01a

  Copy full SHA for ba0a01a

• basic printer tests

  mmcloughlin

  committed
  df71a75

  Copy full SHA for df71a75

• ensure printed isle parses

  mmcloughlin

  committed
  1e70a2f

  Copy full SHA for 1e70a2f

• alow position tagging to be disabled

  mmcloughlin

  committed
  2876e90

  Copy full SHA for 2876e90

• fix roundtrip errors

  mmcloughlin

  committed
  cda22d8

  Copy full SHA for cda22d8

• test against full isle files

  mmcloughlin

  committed
  dc155ce

  Copy full SHA for dc155ce

• start trace to spec translation

  mmcloughlin

  committed
  227989e

  Copy full SHA for 227989e

• more spec translation

  mmcloughlin

  committed
  8745a04

  Copy full SHA for 8745a04

• even more spec translation

  mmcloughlin

  committed
  493aa3d

  Copy full SHA for 493aa3d

• use concat to support arbitrary length bitvectors

  mmcloughlin

  committed
  475328c

  Copy full SHA for 475328c

• handle more spec translation

  mmcloughlin

  committed
  6ef5e50

  Copy full SHA for 6ef5e50

• isle: support printing of any Printable nodes

  mmcloughlin

  committed
  e85162d

  Copy full SHA for e85162d

• isle: Errors implement std::error::Error

  mmcloughlin

  committed
  02a46a7

  Copy full SHA for 02a46a7

• emit: print generated spec

  mmcloughlin

  committed
  814a67a

  Copy full SHA for 814a67a

• emit: tolerate spec conversion failure

  mmcloughlin

  committed
  97e8582

  Copy full SHA for 97e8582

• isaspec adhoc tool for building specs

  mmcloughlin

  committed
  73f231f

  Copy full SHA for 73f231f

• expend spec config to produce a real spec

  mmcloughlin

  committed
  92c6ffd

  Copy full SHA for 92c6ffd

• veriisle: specfunc experiment for executing single spec functions

  mmcloughlin

  committed
  8e3f5cf

  Copy full SHA for 8e3f5cf

• veriisle: exec add function

  mmcloughlin

  committed
  31e6ec7

  Copy full SHA for 31e6ec7

• isaspec: provide cases

  mmcloughlin

  committed
  f26b486

  Copy full SHA for f26b486

• generate more alu ops

  mmcloughlin

  committed
  3e137e8

  Copy full SHA for 3e137e8

• keep debug output

  mmcloughlin

  committed
  46f554d

  Copy full SHA for 46f554d

• elide no-op zext

  mmcloughlin

  committed
  f7decdd

  Copy full SHA for f7decdd

• veriisle: isaspec option to write to file

  mmcloughlin

  committed
  79d673c

  Copy full SHA for 79d673c

• isle: parse spec implication operator

  mmcloughlin

  committed
  b9da528

  Copy full SHA for b9da528

• codegen: add inst_specs.isle to aarch64 isle compilation

  mmcloughlin

  committed
  5281b49

  Copy full SHA for 5281b49

• veriisle: generate instruction specs

  mmcloughlin

  committed
  176292f

  Copy full SHA for 176292f

• verify add lowering to alu_rrr

  mmcloughlin

  committed
  b5f2b68

  Copy full SHA for b5f2b68

• wip

  mmcloughlin

  committed
  2fe39d3

  Copy full SHA for 2fe39d3

• x64 footprint

  mmcloughlin

  committed
  a49bfdf

  Copy full SHA for a49bfdf

• switch back to add rule

  mmcloughlin

  committed
  feaa688

  Copy full SHA for feaa688

• restore imp case in spec_op_to_expr

  mmcloughlin

  committed
  95f5c4a

  Copy full SHA for 95f5c4a

• revert changes to aarch64/inst.isle

  mmcloughlin

  committed
  8c95834

  Copy full SHA for 8c95834

• remove debug print in widen to register width

  mmcloughlin

  committed
  d1e50b0

  Copy full SHA for d1e50b0

• wip

  mmcloughlin

  committed
  cfd78d8

  Copy full SHA for cfd78d8

• fix build

  mmcloughlin

  committed
  eee9cff

  Copy full SHA for eee9cff

• isaspec generates the (= result #b1) condition

  mmcloughlin

  committed
  2100e74

  Copy full SHA for 2100e74

• use different prefixes for each instruction case

  mmcloughlin

  committed
  106d01e

  Copy full SHA for 106d01e

• handle the 32-bit case

  mmcloughlin

  committed
  cbc0731

  Copy full SHA for cbc0731

• extend sail spec to all bitwidths

  mmcloughlin

  committed
  5374323

  Copy full SHA for 5374323

• add more aluops

  mmcloughlin

  committed
  7bf9cc4

  Copy full SHA for 7bf9cc4

• define isla dependency with git

  mmcloughlin

  committed
  9eba5f6

  Copy full SHA for 9eba5f6

Commits on Mar 8, 2024

• containment check before accessing annotation info, still errors arising from workaround

  yelhsams

  committed
  ccf5f25

  Copy full SHA for ccf5f25

Commits on Apr 18, 2024

• broken ireduce test WIP

  yelhsams

  committed
  d5006b4

  Copy full SHA for d5006b4

Commits on May 6, 2024

• Merge branch 'mbm/unified-type-inference' into integrate-type-inf

  yelhsams

  committed
  902ee80

  Copy full SHA for 902ee80

Commits on May 7, 2024

• start of integrating smt type inf changes into wasmtime

  yelhsams

  committed
  7a50810

  Copy full SHA for 7a50810