Working with unmapped variable in an expression environment and build…

g2.cabal

@@ -47,6 +47,7 @@ library
  , G2.Equiv.Types
  , G2.Equiv.Generalize
  , G2.Equiv.Summary
+ , G2.Equiv.Uninterpreted
 
  , G2.Execution
  , G2.Execution.Interface

nebula_scripts/Build_cabal_and_project.py

@@ -4,15 +4,20 @@
 # first argument is the python file
 # second argument is the directory that contain all the package that contain rules
 # third argument is the location of g2 in one's computer
+
+
 import os 
 import sys
 import re
 import tempfile
+import itertools
 
 def changing_cabal(directory):
  found_ghc = False
  found_build = False
  extension_to_check = ['library','test-suite','executable']
+ # common stanza: binding or expression reused in different parts of the module
+ modularity = ['import'] 
  for root, dirs, files in os.walk(directory):
  for file_name in files:
  # process for replace cabal file 
@@ -27,7 +32,7 @@ def changing_cabal(directory):
  with open(file_path,'r') as file, open(temp_path,'a') as temp_file:
  lines = file.readlines()
  # reading two lines together 
- for line,next_line in zip(lines,lines[1:]):
+ for line,next_line in itertools.zip_longest(lines, lines[1:], fillvalue=''):
  search_build_depends = re.search("Build-Depends:",line,re.IGNORECASE)
  if search_build_depends:
  print("The build-depends before update is " + line)
@@ -36,22 +41,44 @@ def changing_cabal(directory):
  found_build = True
  for extension in extension_to_check:
  if line.startswith(extension):
+ for module in modularity:
+ next_line_strip = next_line.lstrip()
+ if not next_line_strip.startswith(module):
  # finding the correct amount of whitespace to insert in the next line 
+ print("The next line's content " + next_line)
+ without_whitespace = next_line.lstrip()
+ whitespace_amount = len(next_line) - len(without_whitespace)
+ line = line + "\n" + " " * whitespace_amount + "ghc-options: -fplugin=G2.Nebula -fplugin-opt=G2.Nebula:--limit -fplugin-opt=G2.Nebula:10" + "\n"
+ print("Chaging line for ghc-option")
+ print("the line after changing is " + line)
+ found_ghc = True
+ # taking care of the common stanza case 
+ for module in modularity:
+ line_without_space = line.lstrip()
+ if line_without_space.startswith(module):
  without_whitespace = next_line.lstrip()
  whitespace_amount = len(next_line) - len(without_whitespace)
  line = line + "\n" + " " * whitespace_amount + "ghc-options: -fplugin=G2.Nebula -fplugin-opt=G2.Nebula:--limit -fplugin-opt=G2.Nebula:10" + "\n"
  print("Chaging line for ghc-option")
- print("the line after changing is " + line )
+ print("the line after changing is " + line)
  found_ghc = True
  temp_file.write(line)
  #writing build-depends and ghc-option in case of not founding those
  with open(temp_path, 'a+') as temp:
- if found_build == False:
- print("build-depends not found \n")
- temp.write( "build-depends: g2 >= 0.1.0.2 " + '\n')
- if found_ghc == False:
- print("ghc-option not found \n")
- temp.write("ghc-options: -fplugin=G2.Nebula -fplugin-opt=G2.Nebula:--limit -fplugin-opt=G2.Nebula:10")
+ lines = temp.readlines()
+ if lines:
+ # format the ghc option and build-depends against previous line of the file
+ last_line = lines[-1]
+ last_line_whitespace = last_line.lstrip()
+ whitespace_amount = len(last_line) - len(last_line_whitespace)
+ if found_build == False:
+ print("build-depends not found \n")
+ write_line = whitespace_amount * " " + "build-depends: g2 >= 0.1.0.2 " + '\n'
+ temp.write(write_line)
+ if found_ghc == False:
+ print("ghc-option not found \n")
+ write_line = whitespace_amount * " " + "ghc-options: -fplugin=G2.Nebula -fplugin-opt=G2.Nebula:--limit -fplugin-opt=G2.Nebula:10"
+ temp.write(write_line)
  os.replace(temp_path, file_path)
  # checking for error just in case and left a error file in the directory 
  except BaseException:

nebula_scripts/ScriptForHackageRules2.py

@@ -82,7 +82,7 @@ def starter(directory):
 # "main"
 args = sys.argv
 if len(args) != 2:
- raise Exception("Invalid number of commands provided.")
+ raise Exception("Invalid number of commands provided. The first argument is the script name. The second argument is the name of the directory contain all of the download hackage")
 with open("./hackageRules1.txt", 'w') as file:
  file.truncate()
 directory = sys.argv[1]

src/G2/Equiv/Config.hs

@@ -8,10 +8,10 @@
 
 import G2.Config.Config
 
 import Data.Monoid ((<>))
 import qualified Data.Text as T
 import Options.Applicative
 import Text.Read
 
 -- Config options
 data NebulaConfig = NC { limit :: Int
@@ -19,7 +19,9 @@
  , print_summary :: SummaryMode
  , use_labeled_errors :: UseLabeledErrors
  , log_states :: LogMode -- ^ Determines whether to Log states, and if logging states, how to do so.
- , sync :: Bool }
+ , log_rule :: Maybe String -- ^ Allow user to log the states for specific rule. 
+ , sync :: Bool 
+ , symbolic_unmapped :: Bool}
 
 data SummaryMode = SM { have_summary :: Bool
  , have_history :: Bool
@@ -74,7 +76,17 @@
  <*> mkSummaryMode
  <*> flag UseLabeledErrors NoLabeledErrors (long "no-labeled-errors" <> help "disable labeled errors, treating all errors as equivalent")
  <*> mkLogMode
+ <*> mkLogRule
  <*> flag False True (long "sync" <> help "sync the left and right expressions prior to symbolic execution")
+ <*> flag True False (long "sym-unmapped" <> help "automatically treat unmapped function as symbolic")
+
+mkLogRule :: Parser (Maybe String)
+mkLogRule =
+ option (maybeReader (Just . Just))
+ ( long "log-rule"
+ <> metavar "RULE"
+ <> value Nothing
+ <> help "Output states for this rule when logging")
 
 mkSummaryMode :: Parser SummaryMode
 mkSummaryMode =

src/G2/Equiv/EquivADT.hs

@@ -94,7 +94,7 @@ exprPairing ns s1@(State {expr_env = h1}) s2@(State {expr_env = h2}) e1 e2 pairs
  | m <- idName i
  , not $ m `elem` ns
  , Just e <- E.lookup m h2 -> exprPairing ns s1 s2 e1 e pairs n1 (m:n2)
- | not $ (idName i) `elem` ns -> error "unmapped variable"
+ | not $ (idName i) `elem` ns -> error $ "unmapped variable" ++ show (idName i)
  (Prim p1 _, Prim p2 _) | p1 == Error || p1 == Undefined
  , p2 == Error || p2 == Undefined -> Just pairs
  -- extra cases for avoiding Error problems

src/G2/Equiv/Uninterpreted.hs

@@ -0,0 +1,139 @@
+{-# LANGUAGE FlexibleContexts, OverloadedStrings #-}
+
+
+module G2.Equiv.Uninterpreted where 
+
+import G2.Language
+import qualified G2.Language.ExprEnv as E
+import Data.Foldable
+import Data.Maybe 
+import qualified Data.Monoid as DM
+import qualified Data.HashMap.Lazy as HM
+import qualified Data.HashSet as HS
+import Debug.Trace
+import qualified Data.Text as T
+
+-- | Find variables that don't have binding and adjust the epxression environment to treat them as symbolic 
+addFreeVarsAsSymbolic :: ExprEnv -> ExprEnv 
+addFreeVarsAsSymbolic eenv = let xs = freeVars eenv eenv 
+ in foldl' (flip E.insertSymbolic) eenv xs 
+
+-- | changing the signature of addFreeTypes so that we have 
+-- we want to modify the rewrite-rules passed in checkrule 
+-- (AstContainer c Expr, Astcontainer c Type, AstContainer t Expr, Astcontainer t Type) => c -> State t -> NameGen -> (c, State t, NameGen)
+-- | apply subvars to the rule 
+addFreeTypes :: (ASTContainer c Expr, ASTContainer c Type, ASTContainer t Expr, ASTContainer t Type) => c -> State t -> NameGen -> (c, State t, NameGen) 
+addFreeTypes c s@(State {type_env = tenv }) ng =
+ let 
+ (tenv', ng') = freeTypesToTypeEnv (freeTypes tenv s) ng
+ tenv'' = HM.union tenv tenv'
+ free_dc = HS.toList $ freeDC tenv'' s
+ m = dataConMapping free_dc
+ s' = subVars m s
+ c' = subVars m c
+ n_te = addDataCons tenv'' free_dc
+ in (c', s' { type_env = n_te }, ng' )
+ -- trace ("show map " ++ show m) (s' { type_env = n_te }, ng') 
+
+
+allDC :: ASTContainer t Expr => t -> HS.HashSet DataCon
+allDC = evalASTs allDC' 
+
+allDC' :: Expr -> HS.HashSet DataCon
+allDC' e = case e of 
+ Data dc -> HS.singleton dc
+ Case _ _ _ as ->
+ HS.fromList $ mapMaybe (\(Alt am _) -> case am of 
+ DataAlt dc _ -> Just dc
+ _ -> Nothing) as 
+ _ -> HS.empty
+
+
+
+freeDC :: ASTContainer e Expr => TypeEnv -> e -> HS.HashSet DataCon
+freeDC typeEnv e =
+ let al = allDC e
+ inTEnv = HS.map (\(DataCon n _) -> n)
+ . HS.fromList
+ . concatMap dataCon
+ . HM.elems $ typeEnv in
+ HS.filter (\(DataCon n _) -> not (HS.member n inTEnv)) al
+
+
+allTypes :: ASTContainer t Type => t -> [(Name, Kind)]
+allTypes = evalASTs allTypes' 
+
+allTypes' :: Type -> [(Name, Kind)]
+allTypes' t = case t of 
+ TyCon n k -> [(n,k)]
+ _ -> []
+
+
+freeTypes :: ASTContainer t Type => TypeEnv -> t -> [(Name, Kind)]
+freeTypes typeEnv t = HM.toList $ HM.difference (HM.fromList $ allTypes t) typeEnv 
+
+
+-- | we getting "free" typesnames and insert it into the TypeEnv with a "uninterprted " dataCons 
+-- Uninterpreted means there are potentially unlimited amount of datacons for a free type
+freeTypesToTypeEnv :: [(Name,Kind)] -> NameGen -> (TypeEnv, NameGen)
+freeTypesToTypeEnv nks ng = 
+ let (adts, ng') = mapNG freeTypesToTypeEnv' nks ng 
+ in (HM.fromList adts, ng') 
+
+freeTypesToTypeEnv' :: (Name, Kind) -> NameGen -> ( (Name, AlgDataTy), NameGen)
+freeTypesToTypeEnv' (n,k) ng =
+ let (bids, ng') = freshIds (argumentTypes $ PresType k) ng 
+ (dcs,ng'') = unknownDC ng' n k bids
+ n_adt = (n, DataTyCon {bound_ids = bids,
+ data_cons = [dcs]})
+ in (n_adt, ng'')
+
+unknownDC :: NameGen -> Name -> Kind -> [Id] -> (DataCon, NameGen)
+unknownDC ng n@(Name occn _ _ _) k is =
+ let tc = TyCon n k 
+ tv = map TyVar is
+ ta = foldl' TyApp tc tv 
+ ti = TyLitInt `TyFun` ta 
+ tfa = foldl' (flip TyForAll) ti is
+ (dc_n, ng') = freshSeededString ("Unknown" DM.<> occn) ng 
+ in (DataCon dc_n tfa, ng')
+
+-- | add free Datacons into the TypeEnv at the appriorpate Type)
+addDataCons :: TypeEnv -> [DataCon] -> TypeEnv
+addDataCons = foldl' addDataCon
+
+addDataCon :: TypeEnv -> DataCon -> TypeEnv
+addDataCon te dc | (TyCon n _):_ <- unTyApp $ returnType dc = 
+ let dtc = HM.lookup n te
+ adt = case dtc of 
+ Just (DataTyCon ids' dcs) -> DataTyCon {bound_ids = ids', data_cons = dc : dcs}
+ Nothing -> error "addDataCons: cannot find corresponding Name in TypeEnv"
+ Just _ -> error "addDataCons: Not DataTyCon AlgDataTy found"
+ in HM.insert n adt te 
+addDataCon _ _ = error "addDataCon: Type of DataCon had incorrect form"
+
+-- | addMapping will handle classification between the DataCon and Type
+addMapping :: [DataCon] -> ExprEnv -> ExprEnv 
+addMapping dcs ee = foldl' addMapping' ee dcs
+
+addMapping' :: ExprEnv -> DataCon -> ExprEnv 
+addMapping' ee dc@(DataCon name _) = E.insert name (Data dc) ee
+
+
+-- | The translation between GHC and g2 didn't have a matching id for the same occurence name
+-- so we are using brute force by matching the same occurence name 
+
+dataConMapping :: [DataCon] -> HM.HashMap (T.Text, Maybe T.Text) DataCon
+dataConMapping dcs = HM.fromList $ map dataConMapping' dcs 
+
+dataConMapping' :: DataCon -> ((T.Text, Maybe T.Text ), DataCon)
+dataConMapping' dc@(DataCon (Name t mt _ _ ) _ ) = ((t,mt), dc)
+
+subVars :: ASTContainer t Expr => HM.HashMap (T.Text, Maybe T.Text) DataCon -> t -> t
+subVars m = modifyASTs (subVars' m) 
+
+subVars' :: HM.HashMap (T.Text, Maybe T.Text) DataCon -> Expr -> Expr
+subVars' m expr@(Var (Id (Name t mt _ _) _ )) = case HM.lookup (t,mt) m of 
+ Just (DataCon n' k) -> Data (DataCon n' k)
+ Nothing -> expr 
+subVars' _ expr = expr

src/G2/Equiv/Verifier.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE FlexibleContexts #-}
 
 module G2.Equiv.Verifier
  ( verifyLoop
@@ -14,6 +15,7 @@ import G2.Interface
 
 import qualified Control.Monad.State.Lazy as CM
 
+
 import qualified G2.Language.ExprEnv as E
 import qualified G2.Language.CallGraph as G
 import qualified G2.Language.Typing as T
@@ -34,6 +36,7 @@ import G2.Equiv.G2Calls
 import G2.Equiv.Tactics
 import G2.Equiv.Generalize
 import G2.Equiv.Summary
+import G2.Equiv.Uninterpreted 
 
 import qualified Data.Map as M
 import G2.Execution.Memory
@@ -754,17 +757,23 @@ reducedGuide ((Marker _ m):ms) = case m of
  _ -> reducedGuide ms
 reducedGuide (_:ms) = reducedGuide ms
 
-checkRule :: Config
+checkRule :: (ASTContainer t Type, ASTContainer t Expr) => Config
  -> NebulaConfig
  -> State t
  -> Bindings
  -> [DT.Text] -- ^ names of forall'd variables required to be total
  -> RewriteRule
  -> IO (S.Result () () ())
 checkRule config nc init_state bindings total rule = do
- let (rewrite_state_l, bindings') = initWithLHS init_state bindings $ rule
- (rewrite_state_r, bindings'') = initWithRHS init_state bindings' $ rule
- sym_ids = ru_bndrs rule
+ let (rule' ,mod_state@(State { expr_env = ee }), te_ng) = addFreeTypes rule init_state (name_gen bindings)
+ (mod_state', ng') = if symbolic_unmapped nc 
+ then 
+ ( mod_state { expr_env = addFreeVarsAsSymbolic ee }
+ , te_ng)
+ else (init_state, name_gen bindings)
+ (rewrite_state_l, bindings') = initWithLHS mod_state' (bindings { name_gen = ng' }) $ rule'
+ (rewrite_state_r, bindings'') = initWithRHS mod_state' bindings' $ rule'
+ sym_ids = ru_bndrs rule' 
  total_names = filter (includedName total) (map idName sym_ids)
  total_hs = foldr HS.insert HS.empty total_names
  EquivTracker et m _ _ _ _ = emptyEquivTracker
@@ -781,6 +790,8 @@ checkRule config nc init_state bindings total rule = do
 
  rewrite_state_l'' = startingState start_equiv_tracker ns rewrite_state_l'
  rewrite_state_r'' = startingState start_equiv_tracker ns rewrite_state_r'
+
+ print (curr_expr rewrite_state_l)
 
  S.SomeSolver solver <- initSolver config
  putStrLn $ "***\n" ++ (show $ ru_name rule) ++ "\n***"

src/G2/Execution/Rules.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE OverloadedStrings, FlexibleContexts #-}
 
 module G2.Execution.Rules ( module G2.Execution.RuleTypes
  , Sharing (..)

src/G2/Language/Expr.hs

@@ -472,9 +472,14 @@ symbVars' eenv (Id n _) = E.isSymbolic n eenv
 freeVars :: ASTContainer m Expr => E.ExprEnv -> m -> [Id]
 freeVars eenv = evalASTsMonoid (freeVars' eenv)
 
+freeAltMatch :: AltMatch -> [Id]
+freeAltMatch (DataAlt _ is) = is
+freeAltMatch _ = []
+
 freeVars' :: E.ExprEnv -> [Id] -> Expr -> ([Id], [Id])
 freeVars' _ _ (Let b _) = (map fst b, [])
 freeVars' _ _ (Lam _ b _) = ([b], [])
+freeVars' _ _ (Case _ b _ alt) = (b:concatMap (freeAltMatch . altMatch) alt, [])
 freeVars' eenv bound (Var i) =
  if E.member (idName i) eenv || i `elem` bound then
  ([], [])

src/G2/Language/Support.hs

@@ -199,15 +199,17 @@ instance ASTContainer t Expr => ASTContainer (State t) Expr where
  (containedASTs $ path_conds s) ++
  (containedASTs $ assert_ids s) ++
  (containedASTs $ exec_stack s) ++
- (containedASTs $ track s)
+ (containedASTs $ track s) ++ 
+ (containedASTs $ rules s)
 
  modifyContainedASTs f s = s { type_env = modifyContainedASTs f $ type_env s
  , expr_env = modifyContainedASTs f $ expr_env s
  , curr_expr = modifyContainedASTs f $ curr_expr s
  , path_conds = modifyContainedASTs f $ path_conds s
  , assert_ids = modifyContainedASTs f $ assert_ids s
  , exec_stack = modifyContainedASTs f $ exec_stack s
- , track = modifyContainedASTs f $ track s }
+ , track = modifyContainedASTs f $ track s 
+ , rules = modifyContainedASTs f $ rules s }
 
 instance ASTContainer t Type => ASTContainer (State t) Type where
  containedASTs s = ((containedASTs . expr_env) s) ++
@@ -217,7 +219,8 @@ instance ASTContainer t Type => ASTContainer (State t) Type where
  ((containedASTs . assert_ids) s) ++
  ((containedASTs . type_classes) s) ++
  ((containedASTs . exec_stack) s) ++
- (containedASTs $ track s)
+ (containedASTs $ track s) ++ 
+ (containedASTs $ rules s)
 
  modifyContainedASTs f s = s { type_env = (modifyContainedASTs f . type_env) s
  , expr_env = (modifyContainedASTs f . expr_env) s
@@ -226,7 +229,8 @@ instance ASTContainer t Type => ASTContainer (State t) Type where
  , assert_ids = (modifyContainedASTs f . assert_ids) s
  , type_classes = (modifyContainedASTs f . type_classes) s
  , exec_stack = (modifyContainedASTs f . exec_stack) s
- , track = modifyContainedASTs f $ track s }
+ , track = modifyContainedASTs f $ track s 
+ , rules = modifyContainedASTs f $ rules s }
 
 instance Named Bindings where
  names b = names (fixed_inputs b)