Source code of SMC, the first string model counter. The paper of this work appears in PLDI 2014.
Java C Perl Python Shell Makefile C++
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
case_studies
src
.gitignore
LICENCES.txt
README.md
smc_kaluza.zip
test_utilities.sh

README.md

Note for insallation and run

To compile

Go to src folder and run make

$ cd src
$ make

To run SMC

./RunSMC inputfile

Replicating the results

  • Case Studies & Comparison (Section 4.2, 4.3, Table 5)

    Run the script test_utilities.sh

    $ ./test_utilities.sh
    

    Output reported on console:

    • composition of constraints
    • time
    • bounds

Top-level directory structure

test_utilities.sh

The script to runs all case studies in the paper

smc_kaluza.zip

SMC's Inputs/ Outputs for Kaluza benchmark

case_studies

Includes several input/output of what we reported in our paper

src

Source folder

  1. automaton

    Handles regexes and automatons conversons.

  2. YAPE

    Comes with regex library of HAMPI[2]

  3. Other files

  • smc_lexer.py

    The lexer file for SMC language. We use PLY library for parsing the input.

  • smc_parser.py

    The main parser of SMC. This module reads and parses the input, converts to CNF and does other tasks as described in the paper. Finally it generates the intermediate language for further processing

  • core.py

    Contains main data structures for the parsing & inital processing steps.

  • utils.py

    Contains main utilities for the parsing & inital processing steps. For example, we translalte the constraints to CNF form, build the concat dependency graph and export the constraint to intermediate constraint language in this file, which are called by smc_parser.py above.

  • main.c

    Reads the generated intermediate file and does the counting job by querying to Mathematica. We read the constraint file twice: the first read is to initialize each variable with their proper length while the second time is to translate the string constraints to GF domain. Finally it returns the results corresponding to the query.

  • utils.c

    Provide the call and interaction with Mathematica.

  • match_regex.c

    Handle regexes operations including handle with group of regex constraints.

  • contains.c

    Handle contains operations, both single contains and conjunction of contains.

  • pcre_tohampi.pm, YAPE, run_pcre.pl, read_pcre.py

    Convert and translate pcre regexes to an intermediate language and transform to GFs domain.

  • smc.conf, smc.kaluza.conf, smc.cs

    Includes serveral configurations for SMC in default, kaluza testcase and case studies respectively. You can configure MAXN - the maximum length of string, ALPHABET_SIZE - the number of characters in alphabet, or the optimization options of concat operator.

  • config.h

    Consists of several consts of the tool.

  • rawutils.py, raw_to_smc_parser.py, raw_to_smc_lexer.py

    Translate C String operators, like strcasestr, strlen,... to SMC language. The translation was mentioned in previous work [1], we just self-implemented it again here.

References

  • [1] A Symbolic Execution Framework for JavaScript. Prateek Saxena, Devdatta Akhawe, Steve Hanna, Stephen McCamant, Feng Mao, Dawn Song. 31st IEEE Symposium on Security and Privacy (Oakland 2010), May 2010.
  • [2] http://people.csail.mit.edu/akiezun/hampi/

Others

  • SMC is maintained by Loi Luu (loiluu@comp.nus.edu.sg). Should you have any comments/questions, please feel free to drop me an email. You can also report bug through email or here on github.

  • We prepared a running VM for SMC hosted on our ftp server. It can be downloaded from:

     ftp://andromeda.d2.comp.nus.edu.sg/www/smc-dev_compressed.vdi.tar.gz
     Username: smc
     Password: smc@nus
     Ubuntu password: 123456