Skip to content

Commit 9f5b527

Browse files
goodlyrottenapplegithub-actionsjberthold
authored
Fix incorrect KMap injections, received from the LLVM library (#378)
This is a temporary fix for #321 until properly addressed upstream by runtimeverification/llvm-backend#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 <[email protected]> Co-authored-by: Jost Berthold <[email protected]>
1 parent 62139cd commit 9f5b527

File tree

3 files changed

+113
-6
lines changed

3 files changed

+113
-6
lines changed

‎library/Booster/Pattern/Binary.hs

+13-5
Original file line numberDiff line numberDiff line change
@@ -192,21 +192,21 @@ popStackSorts n =
192192
BSort s -> pure s
193193
_ -> fail "popping a non sort"
194194

195-
lookupKoreDefinitionSymbol :: SymbolName -> DecodeM (Maybe Symbol)
195+
lookupKoreDefinitionSymbol :: SymbolName -> DecodeM (Either Symbol (Maybe Symbol))
196196
lookupKoreDefinitionSymbol name = DecodeM $ do
197197
(_, mDef) <- ask
198198
pure $ case mDef of
199199
-- return a symbol with dummy attributes if no definition is supplied.
200200
-- this should be used for testing ONLY!
201201
Nothing ->
202-
Just $
202+
Left $
203203
Symbol
204204
name
205205
[]
206206
[]
207207
(SortApp "UNKNOWN" [])
208208
(SymbolAttributes PartialFunction IsNotIdem IsNotAssoc IsNotMacroOrAlias CannotBeEvaluated Nothing)
209-
Just def -> Map.lookup name $ symbols def
209+
Just def -> Right $ Map.lookup name $ symbols def
210210

211211
{- | Successively decodes items from the given "block" of bytes,
212212
branching on the initial tag of the item.
@@ -299,12 +299,20 @@ decodeBlock mbSize = do
299299
mkSymbolApplication "inj" _ bs = argError "Injection" [BTerm undefined] bs
300300
mkSymbolApplication name sorts bs =
301301
lookupKoreDefinitionSymbol name >>= \case
302-
Just symbol@Symbol{sortVars} -> do
302+
-- testing case when we don't have a KoreDefinition
303+
Left symbol@Symbol{sortVars} -> do
303304
args <- forM bs $ \case
304305
BTerm trm -> pure trm
305306
_ -> fail "Expecting term"
306307
pure $ BTerm $ SymbolApplication symbol (zipWith (const id) sortVars sorts) args
307-
Nothing -> fail $ "Unknown symbol " <> show name
308+
Right (Just symbol@Symbol{sortVars, argSorts}) -> do
309+
args <- forM (zip argSorts bs) $ \case
310+
-- temporarily fix injections until https://github.com/runtimeverification/llvm-backend/issues/886 is closed
311+
(srt, BTerm (Injection from _to trm)) -> pure $ Injection from srt trm
312+
(srt, BTerm trm) -> if sortOfTerm trm /= srt then fail "Term has incorrect sort" else pure trm
313+
_ -> fail "Expecting term"
314+
pure $ BTerm $ SymbolApplication symbol (zipWith (const id) sortVars sorts) args
315+
Right Nothing -> fail $ "Unknown symbol " <> show name
308316

309317
argError cons expectedArgs receivedArgs =
310318
fail $

‎test/llvm-integration/LLVM.hs

+57-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
{-# LANGUAGE PatternSynonyms #-}
2+
{-# LANGUAGE QuasiQuotes #-}
23

34
{- |
45
Copyright : (c) Runtime Verification, 2023
@@ -41,7 +42,7 @@ import Booster.Pattern.Base
4142
import Booster.Syntax.Json.Externalise (externaliseTerm)
4243
import Booster.Syntax.Json.Internalise (pattern AllowAlias, pattern IgnoreSubsorts)
4344
import Booster.Syntax.Json.Internalise qualified as Syntax
44-
import Booster.Syntax.ParsedKore.Internalise (buildDefinitions)
45+
import Booster.Syntax.ParsedKore.Internalise (buildDefinitions, symb)
4546
import Booster.Syntax.ParsedKore.Parser (parseDefinition)
4647
import Kore.Syntax.Json.Types qualified as Syntax
4748
import System.Info (os)
@@ -90,6 +91,10 @@ llvmSpec =
9091
it "should work with latin-1strings" $
9192
hedgehog . propertyTest . latin1Prop
9293

94+
beforeAll loadAPI $
95+
it "should correct sort injections in non KItem maps" $
96+
hedgehog . propertyTest . mapKItemInjProp
97+
9398
--------------------------------------------------
9499
-- individual hedgehog property tests and helpers
95100

@@ -147,6 +152,41 @@ latin1Prop api = property $ do
147152
| otherwise -> error $ "Unexpected sort " <> show s
148153
otherTerm -> error $ "Unexpected term " <> show otherTerm
149154

155+
mapKItemInjProp :: Internal.API -> Property
156+
mapKItemInjProp api = property $ do
157+
let k = wrapIntTerm 1
158+
let v = wrapIntTerm 2
159+
LLVM.simplifyTerm api testDef (update k v) (SortApp "SortMapValToVal" []) === singleton k v
160+
where
161+
update k v =
162+
SymbolApplication
163+
(defSymbols Map.! "LblMapValToVal'Coln'primitiveUpdate")
164+
[]
165+
[ SymbolApplication
166+
(defSymbols Map.! "Lbl'Stop'MapValToVal")
167+
[]
168+
[]
169+
, k
170+
, v
171+
]
172+
173+
singleton k v =
174+
SymbolApplication
175+
(defSymbols Map.! "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'")
176+
[]
177+
[k, v]
178+
179+
wrapIntTerm :: Int -> Term
180+
wrapIntTerm i =
181+
SymbolApplication
182+
(defSymbols Map.! "inj")
183+
[SortApp "SortWrappedInt" [], SortApp "SortVal" []]
184+
[ SymbolApplication
185+
(defSymbols Map.! "LblwrapInt")
186+
[]
187+
[intTerm i]
188+
]
189+
150190
------------------------------------------------------------
151191

152192
runKompile :: IO ()
@@ -3470,4 +3510,20 @@ defSymbols =
34703510
}
34713511
}
34723512
)
3513+
,
3514+
( "LblwrapInt"
3515+
, [symb| symbol LblwrapInt{}(SortInt{}) : SortWrappedInt{} [constructor{}(), functional{}(), injective{}()] |]
3516+
)
3517+
,
3518+
( "Lbl'Stop'MapValToVal"
3519+
, [symb| symbol Lbl'Stop'MapValToVal{}() : SortMapValToVal{} [function{}(), functional{}(), total{}()] |]
3520+
)
3521+
,
3522+
( "LblMapValToVal'Coln'primitiveUpdate"
3523+
, [symb| symbol LblMapValToVal'Coln'primitiveUpdate{}(SortMapValToVal{}, SortVal{}, SortVal{}) : SortMapValToVal{} [function{}(), functional{}(), klabel{}("MapValToVal:primitiveUpdate"), total{}()] |]
3524+
)
3525+
,
3526+
( "Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'"
3527+
, [symb| symbol Lbl'Unds'Val2Val'Pipe'-'-GT-Unds'{}(SortVal{}, SortVal{}) : SortMapValToVal{} [function{}(), functional{}(), klabel{}("_Val2Val|->_"), total{}()] |]
3528+
)
34733529
]

‎test/llvm-integration/definition/llvm.k

+43
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ module LLVM
55
imports MAP
66
imports SET
77
imports K-EQUAL
8+
imports MAP-VAL-TO-VAL
89

910
syntax Num ::= Even | Odd
1011
syntax Even ::= Zero() | Two() | Four() | Six() | Eight() | Ten()
@@ -39,3 +40,45 @@ module LLVM
3940
rule div2(Ten()) => Five()
4041

4142
endmodule
43+
44+
module MAP-VAL-TO-VAL
45+
imports WRAPPED-INT
46+
47+
syntax Val ::= WrappedInt
48+
// -----------------------
49+
50+
syntax MapValToVal [hook(MAP.Map)]
51+
syntax MapValToVal ::= MapValToVal MapValToVal
52+
[ left, function, hook(MAP.concat), klabel(_MapValToVal_),
53+
symbol, assoc, comm, unit(.MapValToVal), element(_Val2Val|->_)
54+
]
55+
syntax MapValToVal ::= ".MapValToVal"
56+
[function, total, hook(MAP.unit),klabel(.MapValToVal), symbol]
57+
syntax MapValToVal ::= Val "Val2Val|->" Val
58+
[function, total, hook(MAP.element), klabel(_Val2Val|->_), symbol]
59+
60+
syntax MapValToVal ::= MapValToVal "[" key: Val "<-" value: Val "]" [function, total, klabel(MapVal2Val:update), symbol, hook(MAP.update), prefer]
61+
62+
syntax priorities _Val2Val|->_ > _MapValToVal_ .MapValToVal
63+
syntax non-assoc _Val2Val|->_
64+
65+
syntax MapValToVal ::= MapValToVal "{{" key: Val "<-" value: Val "}}"
66+
[ function, total, klabel(MapValToVal:primitiveUpdate), symbol,
67+
prefer
68+
]
69+
rule M:MapValToVal {{ Key:Val <- Value:Val }}
70+
=> M[Key <- Value]
71+
72+
endmodule
73+
74+
module WRAPPED-INT
75+
imports INT
76+
77+
syntax WrappedInt ::= wrap(Int) [symbol, klabel(wrapInt)]
78+
// -------------------------------------------------------
79+
80+
syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol, klabel(unwrapInt)]
81+
// ---------------------------------------------------------------------------------------
82+
rule unwrap(wrap(A:Int)) => A
83+
endmodule
84+

0 commit comments

Comments
 (0)