From 9f5b527d154d79ea9df209befff46ccdfc3b41d3 Mon Sep 17 00:00:00 2001 From: Samuel Balco Date: Tue, 21 Nov 2023 15:12:37 +0000 Subject: [PATCH] Fix incorrect KMap injections, received from the LLVM library (#378) This is a temporary fix for #321 until properly addressed upstream by https://github.com/runtimeverification/llvm-backend/issues/886 . The fix involves manually adjusting an injection to the correct sort, since we know the sort of the argument for a given symbol from the `KoreDefintion`, passed to the decoder. --------- Co-authored-by: github-actions Co-authored-by: Jost Berthold --- library/Booster/Pattern/Binary.hs | 18 +++++--- test/llvm-integration/LLVM.hs | 58 ++++++++++++++++++++++++- test/llvm-integration/definition/llvm.k | 43 ++++++++++++++++++ 3 files changed, 113 insertions(+), 6 deletions(-) diff --git a/library/Booster/Pattern/Binary.hs b/library/Booster/Pattern/Binary.hs index bd8417844..80e5e4410 100644 --- a/library/Booster/Pattern/Binary.hs +++ b/library/Booster/Pattern/Binary.hs @@ -192,21 +192,21 @@ popStackSorts n = BSort s -> pure s _ -> fail "popping a non sort" -lookupKoreDefinitionSymbol :: SymbolName -> DecodeM (Maybe Symbol) +lookupKoreDefinitionSymbol :: SymbolName -> DecodeM (Either Symbol (Maybe Symbol)) lookupKoreDefinitionSymbol name = DecodeM $ do (_, mDef) <- ask pure $ case mDef of -- return a symbol with dummy attributes if no definition is supplied. -- this should be used for testing ONLY! Nothing -> - Just $ + Left $ Symbol name [] [] (SortApp "UNKNOWN" []) (SymbolAttributes PartialFunction IsNotIdem IsNotAssoc IsNotMacroOrAlias CannotBeEvaluated Nothing) - Just def -> Map.lookup name $ symbols def + Just def -> Right $ Map.lookup name $ symbols def {- | Successively decodes items from the given "block" of bytes, branching on the initial tag of the item. @@ -299,12 +299,20 @@ decodeBlock mbSize = do mkSymbolApplication "inj" _ bs = argError "Injection" [BTerm undefined] bs mkSymbolApplication name sorts bs = lookupKoreDefinitionSymbol name >>= \case - Just symbol@Symbol{sortVars} -> do + -- testing case when we don't have a KoreDefinition + Left symbol@Symbol{sortVars} -> do args <- forM bs $ \case BTerm trm -> pure trm _ -> fail "Expecting term" pure $ BTerm $ SymbolApplication symbol (zipWith (const id) sortVars sorts) args - Nothing -> fail $ "Unknown symbol " <> show name + Right (Just symbol@Symbol{sortVars, argSorts}) -> do + args <- forM (zip argSorts bs) $ \case + -- temporarily fix injections until https://github.com/runtimeverification/llvm-backend/issues/886 is closed + (srt, BTerm (Injection from _to trm)) -> pure $ Injection from srt trm + (srt, BTerm trm) -> if sortOfTerm trm /= srt then fail "Term has incorrect sort" else pure trm + _ -> fail "Expecting term" + pure $ BTerm $ SymbolApplication symbol (zipWith (const id) sortVars sorts) args + Right Nothing -> fail $ "Unknown symbol " <> show name argError cons expectedArgs receivedArgs = fail $ diff --git a/test/llvm-integration/LLVM.hs b/test/llvm-integration/LLVM.hs index 6465f1452..ba1862d1a 100644 --- a/test/llvm-integration/LLVM.hs +++ b/test/llvm-integration/LLVM.hs @@ -1,4 +1,5 @@ {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE QuasiQuotes #-} {- | Copyright : (c) Runtime Verification, 2023 @@ -41,7 +42,7 @@ import Booster.Pattern.Base import Booster.Syntax.Json.Externalise (externaliseTerm) import Booster.Syntax.Json.Internalise (pattern AllowAlias, pattern IgnoreSubsorts) import Booster.Syntax.Json.Internalise qualified as Syntax -import Booster.Syntax.ParsedKore.Internalise (buildDefinitions) +import Booster.Syntax.ParsedKore.Internalise (buildDefinitions, symb) import Booster.Syntax.ParsedKore.Parser (parseDefinition) import Kore.Syntax.Json.Types qualified as Syntax import System.Info (os) @@ -90,6 +91,10 @@ llvmSpec = it "should work with latin-1strings" $ hedgehog . propertyTest . latin1Prop + beforeAll loadAPI $ + it "should correct sort injections in non KItem maps" $ + hedgehog . propertyTest . mapKItemInjProp + -------------------------------------------------- -- individual hedgehog property tests and helpers @@ -147,6 +152,41 @@ latin1Prop api = property $ do | otherwise -> error $ "Unexpected sort " <> show s otherTerm -> error $ "Unexpected term " <> show otherTerm +mapKItemInjProp :: Internal.API -> Property +mapKItemInjProp api = property $ do + let k = wrapIntTerm 1 + let v = wrapIntTerm 2 + LLVM.simplifyTerm api testDef (update k v) (SortApp "SortMapValToVal" []) === singleton k v + where + update k v = + SymbolApplication + (defSymbols Map.! "LblMapValToVal'Coln'primitiveUpdate") + [] + [ SymbolApplication + (defSymbols Map.! "Lbl'Stop'MapValToVal") + [] + [] + , k + , v + ] + + singleton k v = + SymbolApplication + (defSymbols Map.! "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'") + [] + [k, v] + + wrapIntTerm :: Int -> Term + wrapIntTerm i = + SymbolApplication + (defSymbols Map.! "inj") + [SortApp "SortWrappedInt" [], SortApp "SortVal" []] + [ SymbolApplication + (defSymbols Map.! "LblwrapInt") + [] + [intTerm i] + ] + ------------------------------------------------------------ runKompile :: IO () @@ -3470,4 +3510,20 @@ defSymbols = } } ) + , + ( "LblwrapInt" + , [symb| symbol LblwrapInt{}(SortInt{}) : SortWrappedInt{} [constructor{}(), functional{}(), injective{}()] |] + ) + , + ( "Lbl'Stop'MapValToVal" + , [symb| symbol Lbl'Stop'MapValToVal{}() : SortMapValToVal{} [function{}(), functional{}(), total{}()] |] + ) + , + ( "LblMapValToVal'Coln'primitiveUpdate" + , [symb| symbol LblMapValToVal'Coln'primitiveUpdate{}(SortMapValToVal{}, SortVal{}, SortVal{}) : SortMapValToVal{} [function{}(), functional{}(), klabel{}("MapValToVal:primitiveUpdate"), total{}()] |] + ) + , + ( "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'" + , [symb| symbol Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'{}(SortVal{}, SortVal{}) : SortMapValToVal{} [function{}(), functional{}(), klabel{}("_Val2Val|->_"), total{}()] |] + ) ] diff --git a/test/llvm-integration/definition/llvm.k b/test/llvm-integration/definition/llvm.k index 766f3c4cd..8e79f5118 100644 --- a/test/llvm-integration/definition/llvm.k +++ b/test/llvm-integration/definition/llvm.k @@ -5,6 +5,7 @@ module LLVM imports MAP imports SET imports K-EQUAL + imports MAP-VAL-TO-VAL syntax Num ::= Even | Odd syntax Even ::= Zero() | Two() | Four() | Six() | Eight() | Ten() @@ -39,3 +40,45 @@ module LLVM rule div2(Ten()) => Five() endmodule + +module MAP-VAL-TO-VAL + imports WRAPPED-INT + + syntax Val ::= WrappedInt + // ----------------------- + + syntax MapValToVal [hook(MAP.Map)] + syntax MapValToVal ::= MapValToVal MapValToVal + [ left, function, hook(MAP.concat), klabel(_MapValToVal_), + symbol, assoc, comm, unit(.MapValToVal), element(_Val2Val|->_) + ] + syntax MapValToVal ::= ".MapValToVal" + [function, total, hook(MAP.unit),klabel(.MapValToVal), symbol] + syntax MapValToVal ::= Val "Val2Val|->" Val + [function, total, hook(MAP.element), klabel(_Val2Val|->_), symbol] + + syntax MapValToVal ::= MapValToVal "[" key: Val "<-" value: Val "]" [function, total, klabel(MapVal2Val:update), symbol, hook(MAP.update), prefer] + + syntax priorities _Val2Val|->_ > _MapValToVal_ .MapValToVal + syntax non-assoc _Val2Val|->_ + + syntax MapValToVal ::= MapValToVal "{{" key: Val "<-" value: Val "}}" + [ function, total, klabel(MapValToVal:primitiveUpdate), symbol, + prefer + ] + rule M:MapValToVal {{ Key:Val <- Value:Val }} + => M[Key <- Value] + +endmodule + +module WRAPPED-INT + imports INT + + syntax WrappedInt ::= wrap(Int) [symbol, klabel(wrapInt)] + // ------------------------------------------------------- + + syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol, klabel(unwrapInt)] + // --------------------------------------------------------------------------------------- + rule unwrap(wrap(A:Int)) => A +endmodule +