initialize nanojs

.gitignore

@@ -0,0 +1,38 @@
+dist
+cabal-dev
+*.md
+*.o
+*.hi
+*.chi
+*.chs.h
+.virthualenv
+*.a
+*.cmxa
+*.cm[oxai]
+*.annot
+*.vmap
+*.di?
+*.native
+*.fqout
+*.out
+*.fq
+*.annot
+*.cgi
+*.log
+*.html
+*.pyc
+build.sh
+config.make
+*.scalarlog
+*.tags
+_build
+*~
+*.swp
+*.swo
+
+TAGS
+a.out
+*.json
+js/
+css/
+

LICENSE

@@ -0,0 +1,30 @@
+Copyright (c) 2013, Ranjit Jhala
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Ranjit Jhala nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Language/Nano/JS/CmdLine.hs

@@ -0,0 +1,49 @@
+{-# LANGUAGE TupleSections, DeriveDataTypeable #-}
+
+module Language.Nano.JS.CmdLine (getOpts) where
+
+import Control.Applicative                      ((<$>))
+import System.FilePath                          (dropFileName)
+import Language.Fixpoint.Misc                   (single, sortNub) 
+import Language.Nano.JS.Types                   (Config (..))
+import System.Console.CmdArgs                  
+
+---------------------------------------------------------------------------------
+-- | Parsing Command Line -------------------------------------------------------
+---------------------------------------------------------------------------------
+
+config = Config { 
+   files   = def &= typ "TARGET" 
+                 &= args 
+                 &= typFile 
+
+ , incdirs = def &= typDir 
+                 &= help "Paths to Spec Include Directory " 
+
+ } &= verbosity
+   &= program "nano-js" 
+   &= help    "The Nano Software Verification System" 
+   &= summary "nano-js © Copyright 2013 Regents of the University of California." 
+   &= details [ "nano-js is suite of toy program verifiers"
+              , ""
+              , "To check a file foo.js, type:"
+              , "  nano-js foo.hs "
+              ]
+
+getOpts :: IO Config 
+getOpts = do md <- cmdArgs config 
+             putStrLn $ banner md
+             return   $ md
+
+banner args =  "nano-js © Copyright 2013 Regents of the University of California.\n" 
+            ++ "All Rights Reserved.\n"
+            ++ "nano-js" ++ show args ++ "\n" 
+
+-- mkOpts :: Config -> IO Config
+-- mkOpts = return
+
+-- mkOpts md  
+--   = do files' <- sortNub . concat <$> mapM getHsTargets (files md) 
+--        idirs' <- if null (idirs md) then single <$> getIncludePath else return (idirs md) 
+--        return  $ md { files = files' } { idirs = map dropFileName files' ++ idirs' }
+

Language/Nano/JS/Types.hs

@@ -0,0 +1,24 @@
+{-# LANGUAGE DeriveDataTypeable     #-}
+{- LANGUAGE MultiParamTypeClasses  #-}
+{- LANGUAGE TypeSynonymInstances   #-}
+{- LANGUAGE FlexibleInstances      #-}
+{- LANGUAGE FlexibleContexts       #-} 
+{- LANGUAGE OverlappingInstances   #-}
+
+
+
+module Language.Nano.JS.Types (
+  -- * Configuration Options
+  Config (..)
+
+  ) where
+
+import Data.Typeable                (Typeable)
+import Data.Generics                (Data)   
+
+data Config = Config { 
+    files   :: [FilePath]     -- ^ source files to check
+  , incdirs :: [FilePath]     -- ^ path to directory for including specs
+  } deriving (Data, Typeable, Show, Eq)
+
+

Makefile

@@ -0,0 +1,19 @@
+PROFOPTS="-O2 -rtsopts -prof -auto-all -caf-all -XStandaloneDeriving -XDeriveDataTypeable"
+
+CABAL=cabal
+CABALP=$(CABAL) install -p
+
+all:
+	$(CABAL) install
+
+build:
+	$(CABAL) build
+
+clean:
+	cabal clean
+
+docs:
+	$(CABAL) haddock --executables --internal --hoogle --hyperlink-source #--html-location=http://goto.ucsd.edu/~rjhala/llvm-haskell/
+
+lint:
+	hlint --colour --report .

NanoJS.hs

@@ -0,0 +1,35 @@
+
+import System.Environment           (getArgs)
+import Text.Printf                  (printf)
+
+-- import Language.Nano.SMT.Misc       (errorstar)
+-- import Language.Nano.SMT.Types      (Formula)
+-- import Language.Nano.SMT.Tests      (runTests)
+-- import Language.Nano.SMT.SMT        (smt_solver)
+import Control.Monad                (forM_)
+import Language.Nano.JS.CmdLine         (getOpts)
+
+
+main = do cfg <- getOpts  
+          putStrLn $ "nano-js: " ++ show cfg
+
+-- main 
+--   = do files <- getArgs
+--        case files of
+--          []  -> errorstar "No Input Files!"
+--          fs  -> forM fs solveFile
+--
+-- main 
+--   = runTests 
+-- 
+-- solveFile f 
+--   = parseQuery f >>= solveQuery f
+-- 
+-- solveQuery name q
+--   = putStrLn $ printf "Result: %s is %s" name (show $ smt_solver q)
+-- 
+-- parseQuery :: FilePath -> IO Formula
+-- parseQuery = undefined
+-- 
+-- tests :: [(String, Formula)]
+-- tests = []  

README.md

@@ -1,4 +1,47 @@
-nano-js
+README
 =======
 
-Language for experimenting with verification algorithms
+Language for experimenting with verification algorithms
+
+nano-js is the basis for the programming assignments in 
+
+    http://goto.ucsd.edu/~rjhala/classes/sp13/cse291
+
+TODO
+----
+
+HW 1            <------------------------- HEREHEREHEREHERE
+
+0. Wrap parser
+
+1. Port small tests 
+    - int-incr
+    - if-max
+    - if-abs
+
+2. Parse small functions : FilePath -> Com
+
+3. VCGen :: Com -> Pred
+
+4. valid :: Pred -> Bool [liquid-fixpoint wrapper for Pred]
+
+5. Port big tests
+
+    - while-array
+    - while-binsearch
+    - adpcmini.c
+
+Homework Plan
+-------------
+
+HW 1
+1a. VCG 
+1b. Use ESC/J
+
+HW 2
+2a. ConsGen = VCG+K for LoopInv via FIXPOINT
+2b. Implement FIXPOINT (over liquid-fixpoint)
+
+HW 3
+3a. VCG for Refinement Type Checking
+3b. Consgen = VCG+K for Liquid Type Inference via FIXPOINT

Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

nano-js.cabal

@@ -0,0 +1,51 @@
+-- Initial nano-smt.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                nano-js
+version:             0.1.0.0
+synopsis:            Small Language for Implementing Verification Algorithms
+-- description:         
+homepage:            https://github.com/UCSD-PL/nano-js
+license:             BSD3
+license-file:        LICENSE
+author:              Ranjit Jhala
+maintainer:          jhala@cs.ucsd.edu
+-- copyright:           
+category:            Language
+build-type:          Simple
+cabal-version:       >=1.8
+
+executable nano-js
+  build-depends:       base ==4.5.*, pretty, hashable, unordered-containers, 
+                       filepath, ansi-terminal, process, HUnit, syb, cmdargs,
+                       liquid-fixpoint 
+
+  extensions:          ExistentialQuantification, 
+                       FlexibleInstances, 
+                       UndecidableInstances,
+                       DeriveDataTypeable,
+                       TupleSections,
+                       NoMonomorphismRestriction,
+                       ScopedTypeVariables,
+                       BangPatterns
+
+  ghc-options:         -W -O2  
+  Main-is:             NanoJS.hs
+
+Library
+  build-depends:       base ==4.5.*, pretty, hashable, unordered-containers, 
+                       filepath, ansi-terminal, process, HUnit 
+
+  extensions:          ExistentialQuantification, 
+                       FlexibleInstances, 
+                       UndecidableInstances,
+                       DeriveDataTypeable,
+                       TupleSections,
+                       NoMonomorphismRestriction,
+                       ScopedTypeVariables,
+                       BangPatterns
+
+  ghc-options:         -W -O2  
+
+
+  Exposed-Modules: