Skip to content
Switch branches/tags

Latest commit

* use shallow instead of shallowP

* eliminate manifest in new_stream

* more simplification on fs models

* define size_= and cursor_=

* implement wrap

* fix field-assign node, eliminate ctrl effect on field-@

* fix fs test

* added sketch for dup

* implement transparent stat syscall

* adapt playground to fs

* more refactoring

* added literal, shift file.write methods to frontend

* minor refactor

- add statFieldMap

* fix error

* from_bytes uses lvalue reference

* added test gen

* add testUnit

* updated generated tests

* fix up testUnit

* added generated files (can remove in the future)

* implemented operator== on Value

* More tests

- modified implementation for assertEq,
- implement testReadStatField

* added tests for writeStatField

* added syscall prefix to syscalls

* generate set_file helper

* more backend cleanup

* File passing by pointer

- use virtualize for assertEq

* FS uses root_file

* fix FS operation effect

* fix literal

* added stringops

* fixed deref, field reflect using explicit unit

* eliminate seek_file backend, fix setter return type

* use pointer to model stream

* backend modification

* change NullPtr type to Nothing

* add list-last node

* codegen tweak

* added either cpp codegen

* refactor assert

* FS operations support directory structure

- added tests

* remove String constructor and explicit unit

* added type parameter to NullPtr

* implemented has_file_type and set_file_type

* fix vararg argument width

* added PURE_STATE

* refactor flag

* change setFile semantics, refactor ExternalUtil

* implemented mkdir and test

* implemented more syscalls and tests

* added creat.c

Git stats


Failed to load latest commit information.

Scala CI

Staged Program Analyzers

Improving the performance of static analysis by meta-programming/multi-stage programming.


  • dev-clean Current development using LMS-clean
  • oopsla19-code The artifact of the OOPSLA '19 submission

Related Software/Code

  • lms-clean The new version of LMS library
  • immer An immutable data structures library for C++
  • dev-obsolete Outdated development using virtualization-lms-core
  • pldi19-code The code for the PLDI '19 submission (obsoleted)
  • abscomp-racket Abstract Compilation (CC '96) implemented in Racket


  • Towards Partially Evaluating Symbolic Interpreters for All
    Shangyin Tan, Guannan Wei, Tiark Rompf
    ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), co-located with POPL 2022. Philadelphia, PA, USA

  • LLSC: A Parallel Symbolic Execution Compiler for LLVM IR (Demo Paper)
    Guannan Wei, Shangyin Tan, Oliver Bračevac, Tiark Rompf
    Proceedings of The 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2021)
    PDF (ACM DL)

  • Compiling Symbolic Execution with Staging and Algebraic Effect
    Guannan Wei, Oliver Bračevac, Shangyin Tan, Tiark Rompf
    Proceedings of the ACM on Programming Languages, Volume 4 (OOPSLA 2020). Online
    PDF (ACM DL)

  • Staged Abstract Interpreters: Fast and Modular Whole-Program Analysis via Meta-Programming
    Guannan Wei, Yuxuan Chen, Tiark Rompf
    Proceedings of the ACM on Programming Languages, Volume 3 (OOPSLA 2019). Athens, Greece
    PDF (ACM DL)