From 04e5e6920d774f784aa790c53c836e14085f5758 Mon Sep 17 00:00:00 2001 From: Bill Hallahan Date: Tue, 4 Jul 2023 21:19:18 -0400 Subject: [PATCH] Lift specification on tuple elements outside of the tuple --- src/G2/Liquid/Inference/GeneratedSpecs.hs | 2 +- src/G2/Liquid/Inference/Sygus/LiaSynth.hs | 64 ++++++++++++++++++++++- tests/LiquidInf/Paper/Eval/compare.py | 6 +-- tests_lh/LHTest.hs | 1 + tests_lh/test_files/Pos/Test51.hs | 21 ++++++++ 5 files changed, 89 insertions(+), 5 deletions(-) create mode 100644 tests_lh/test_files/Pos/Test51.hs diff --git a/src/G2/Liquid/Inference/GeneratedSpecs.hs b/src/G2/Liquid/Inference/GeneratedSpecs.hs index 5806baed0..086a6c98e 100644 --- a/src/G2/Liquid/Inference/GeneratedSpecs.hs +++ b/src/G2/Liquid/Inference/GeneratedSpecs.hs @@ -1,7 +1,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-} -module G2.Liquid.Inference.GeneratedSpecs ( GeneratedSpecs +module G2.Liquid.Inference.GeneratedSpecs ( GeneratedSpecs (..) , emptyGS , namesGS diff --git a/src/G2/Liquid/Inference/Sygus/LiaSynth.hs b/src/G2/Liquid/Inference/Sygus/LiaSynth.hs index ce65e1f70..40fbff8c6 100644 --- a/src/G2/Liquid/Inference/Sygus/LiaSynth.hs +++ b/src/G2/Liquid/Inference/Sygus/LiaSynth.hs @@ -574,10 +574,72 @@ sySpecNamesForModel sys = modelToGS :: M.Map Name SpecInfo -> SMTModel -> GeneratedSpecs modelToGS m_si mdl = let - lh_spec = M.map (\si -> buildLIA_LH si mdl) . M.filter (\si -> s_status si == Synth) $ m_si + lh_spec = M.map (\si -> liftTupleSpecs si $ buildLIA_LH si mdl) . M.filter (\si -> s_status si == Synth) $ m_si in M.foldrWithKey insertAssertGS emptyGS lh_spec +-- | Only use measures for tuple specs +liftTupleSpecs :: SpecInfo -> [PolyBound LHF.Expr] -> [PolyBound LHF.Expr] +liftTupleSpecs si = map (uncurry3 liftTupleSpecs') + . zip3 (s_type_pre si ++ [s_type_post si]) (s_syn_pre si ++ [s_syn_post si]) + +liftTupleSpecs' :: Type -> PolyBound SynthSpec -> PolyBound LHF.Expr -> PolyBound LHF.Expr +liftTupleSpecs' t sy_spec pbe | Just i <- tupleCount (tyAppCenter t) = + liftTupleSpecs'' i + (map lh_rep . sy_rets $ headValue sy_spec) + (headValue pbe) + (removeHead sy_spec) + (removeHead pbe) + | otherwise = pbe + +tupleCount :: Type -> Maybe Int +tupleCount (TyCon (Name n _ _ _) _) + | Just ('(', _) <- T.uncons n + , T.last n == ')' + , T.all (== ',') (T.init $ T.tail n) = Just (T.length n - 2) +tupleCount _ = Nothing + +liftTupleSpecs'' :: Int + -> [LH.Expr] -- ^ Tuple extractors, i.e. x_Tuple## + -> LH.Expr + -> [PolyBound SynthSpec] + -> [PolyBound LHF.Expr] + -> PolyBound LH.Expr +liftTupleSpecs'' tuple_size extractors e pb_syspec pb_e = + let + extract_ns = map (\j -> LHF.symbol $ "x_Tuple" ++ show tuple_size ++ show j) [1..tuple_size] + e' = map (uncurry3 liftTupleSpecs''') $ zip3 extractors (map headValue pb_syspec) (map headValue pb_e) + in + PolyBound (PAnd $ e:e') $ map (\(PolyBound _ ps) -> PolyBound LHF.PTrue ps) pb_e + +liftTupleSpecs''' :: LHF.Expr -> SynthSpec -> LHF.Expr -> LHF.Expr +liftTupleSpecs''' _ (SynthSpec { sy_rets = [] }) = id +liftTupleSpecs''' extracter (SynthSpec { sy_rets = (SpecArg { lh_rep = rep }):_}) = go + where + go e | e == rep = extracter + go e@(ESym _) = e + go e@(ECon _) = e + go e@(EVar _) = e + go (EApp e1 e2) = EApp (go e1) (go e2) + go (ENeg e) = ENeg (go e) + go (EBin bop e1 e2) = EBin bop (go e1) (go e2) + go (EIte e1 e2 e3) = EIte (go e1) (go e2) (go e3) + go (ECst e s) = ECst (go e) s + go (ELam sy e) = ELam sy (go e) + go (ETApp e s) = ETApp (go e) s + go (ETAbs e s) = ETAbs (go e) s + go (PAnd es) = PAnd (map go es) + go (POr es) = POr (map go es) + go (PNot e) = PNot (go e) + go (PImp e1 e2) = PImp (go e1) (go e2) + go (PIff e1 e2) = PIff (go e1) (go e2) + go (PAtom brel e1 e2) = PAtom brel (go e1) (go e2) + go e@(PKVar _ _) = e + go (PAll s e) = PAll s (go e) + go (PExist s e) = PExist s (go e) + go (PGrad k sub g e) = PGrad k sub g (go e) + go (ECoerc s1 s2 e) = ECoerc s1 s2 (go e) + -- | Generates an Assert that, when added to a formula with the relevant variables, -- blocks it from returning the model blockModelDirectly :: SMTModel -> SMTHeader diff --git a/tests/LiquidInf/Paper/Eval/compare.py b/tests/LiquidInf/Paper/Eval/compare.py index 525be0bfa..4127e1302 100644 --- a/tests/LiquidInf/Paper/Eval/compare.py +++ b/tests/LiquidInf/Paper/Eval/compare.py @@ -84,12 +84,12 @@ def main(): # log = log_test # (log_haskell, safe_compare, num_compare) = eval.test_pos_folder("tests/LiquidInf/Paper/Eval/Compare", "600", ["--use-invs"], skip = skip_list()); + (log_haskell, safe_compare, num_compare) = eval.test_pos_folder("tests/LiquidInf/Paper/Eval/Compare", "600", ["--use-invs"]); + print(str(safe_compare) + "/" + str(num_compare) + " Safe"); + log_z3 = runZ3() log_chc = runCHC() - (log_haskell, safe_compare, num_compare) = eval.test_pos_folder("tests/LiquidInf/Paper/Eval/Compare", "10", ["--use-invs"]); - print(str(safe_compare) + "/" + str(num_compare) + " Safe"); - eval.create_table(log_haskell) eval.create_simple_table(log_haskell) diff --git a/tests_lh/LHTest.hs b/tests_lh/LHTest.hs index aa8bcf3bc..886ad579c 100644 --- a/tests_lh/LHTest.hs +++ b/tests_lh/LHTest.hs @@ -339,6 +339,7 @@ posInfTests = testGroup "Tests" , posTestInference "tests_lh/test_files/Pos/Test48.hs" , posTestInference "tests_lh/test_files/Pos/Test49.hs" , posTestInference "tests_lh/test_files/Pos/Test50.hs" + , posTestInference "tests_lh/test_files/Pos/Test51.hs" , posTestInference "tests_lh/test_files/Pos/Sets1.hs" , posTestInference "tests_lh/test_files/Pos/Sets2.hs" diff --git a/tests_lh/test_files/Pos/Test51.hs b/tests_lh/test_files/Pos/Test51.hs new file mode 100644 index 000000000..f8baaa818 --- /dev/null +++ b/tests_lh/test_files/Pos/Test51.hs @@ -0,0 +1,21 @@ +{-@ LIQUID "--no-termination" @-} + +module Test51 (main) where + +data Peano = Succ | Nil + +{-@ main :: Bool -> { b : Bool | b } @-} +main :: Bool -> Bool +main xs = case while xs loop (1, 0, 0, 0) of + (w', z', x', y') -> x' <= 1 + +while :: Bool -> (a -> a) -> a -> a +while ys body x = if ys then while False body (body x) else x + +{-@ loop :: (Int, Int, Int, Int) -> (Int, Int, Int, Int) @-} +loop :: (Int, Int, Int, Int) -> (Int, Int, Int, Int) +loop (w, z, x, y) = + ( if w `mod` 2 == 1 then w + 1 else w + , if z `mod` 2 == 0 then z + 1 else z + , if w `mod` 2 == 1 then x + 1 else x + , if z `mod` 2 == 0 then y + 1 else y)