search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
208 stars 41 forks source link

Log rewrite rule remainders #3944

Closed geo2a closed 3 months ago

geo2a commented 3 months ago

This PR allows logging Kore's rewrite rule remainders in full.

Example log message with 'kore>remainder':

[kore][execute][remainder][detail] After applying  1  rewrite rules there is a satisfiable remainder condition:  \not{_}(\not{_}(\equals{SortInt{}, _}(ConfigVarCONTRACT'Unds'ID:SortInt{}, Lbl'UndsAnd-'Int'Unds'{}(\dv{SortInt{}}("1461501637330902918203684832716283019655932542975"), Lbllookup{}(ConfigVarCONTRACT'Unds'STORAGE:SortMap{}, \dv{SortInt{}}("1"))))))

and in json:

{"context":["kore","execute","remainder",{"term":"39a4b3d"},{"rules-count":"1"}],"message":{"format":"KORE","version":1,"term":{"tag":"Not","sort":{"tag":"SortApp","name":"SortBool","args":[]},"arg":{"tag":"Not","sort":{"tag":"SortApp","name":"SortBool","args":[]},"arg":{"tag":"Equals","argSort":{"tag":"SortApp","name":"SortInt","args":[]},"sort":{"tag":"SortApp","name":"SortBool","args":[]},"first":{"tag":"EVar","name":"VarCONTRACT'Unds'ID","sort":{"tag":"SortApp","name":"SortInt","args":[]}},"second":{"tag":"App","name":"Lbl'UndsAnd-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1461501637330902918203684832716283019655932542975"},{"tag":"App","name":"Lbllookup","sorts":[],"args":[{"tag":"EVar","name":"VarCONTRACT'Unds'STORAGE","sort":{"tag":"SortApp","name":"SortMap","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"1"}]}]}}}}}}