1-- SPDX-FileCopyrightText: 2024 University of Bremen2-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>3--4-- SPDX-License-Identifier: MIT AND GPL-3.0-only56module Language.QBE.Simulator.Symbolic.Tracer7 ( Branch (Branch),8 newBranch,9 fromBranch,10 ExecTrace,11 newExecTrace,12 toSExprs,13 appendBranch,14 appendCons,15 )16where1718import Language.QBE.Simulator.Symbolic.Expression qualified as SE19import SimpleSMT qualified as SMT2021-- Represents a branch condition in the executed code22data Branch23 = Branch24 Bool -- Whether negation of the branch was attempted25 SE.BitVector -- The symbolic branch condition26 deriving (Show, Eq)2728-- Create a new branch condition.29newBranch :: SE.BitVector -> Branch30newBranch = Branch False3132-- Create a new branch from an existing branch, thereby updating its metadata.33-- It is assumed that the condition, encoded in the branches, is equal.34fromBranch :: Branch -> Branch -> Branch35fromBranch (Branch wasNeg' _) (Branch wasNeg ast) =36 Branch (wasNeg || wasNeg') ast3738------------------------------------------------------------------------3940-- Represents a single execution through a program, tracking for each41-- symbolic branch condition if it was 'True' or 'False'.42type ExecTrace = [(Bool, Branch)]4344-- Create a new empty execution tree.45newExecTrace :: ExecTrace46newExecTrace = []4748-- Return all branch conditions of an 'ExecTrace'.49toSExprs :: ExecTrace -> [SMT.SExpr]50toSExprs = map (\(_, Branch _ bv) -> SE.toSExpr bv)5152-- Append a branch to the execution trace, denoting via a 'Bool'53-- if the branch was taken or if it was not taken.54appendBranch :: ExecTrace -> Bool -> Branch -> ExecTrace55appendBranch trace wasTrue branch = trace ++ [(wasTrue, branch)]5657-- Append a constraint to the execution tree. This constraint must58-- be true and, contrary to appendBranch, negation will not be59-- attempted for it.60appendCons :: ExecTrace -> SE.BitVector -> ExecTrace61appendCons trace cons = trace ++ [(True, Branch True cons)]