clang  14.0.0git
SMTConstraintManager.h
Go to the documentation of this file.
1 //== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 //
9 // This file defines a SMT generic API, which will be the base class for
10 // every SMT solver specific class.
11 //
12 //===----------------------------------------------------------------------===//
13 
14 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
15 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
16 
18 #include "clang/Basic/TargetInfo.h"
21 
22 typedef llvm::ImmutableSet<
23  std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
26 
27 namespace clang {
28 namespace ento {
29 
31  mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
32 
33 public:
36  : SimpleConstraintManager(EE, SB) {}
37  virtual ~SMTConstraintManager() = default;
38 
39  //===------------------------------------------------------------------===//
40  // Implementation for interface from SimpleConstraintManager.
41  //===------------------------------------------------------------------===//
42 
44  bool Assumption) override {
46 
47  QualType RetTy;
48  bool hasComparison;
49 
50  llvm::SMTExprRef Exp =
51  SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
52 
53  // Create zero comparison for implicit boolean cast, with reversed
54  // assumption
55  if (!hasComparison && !RetTy->isBooleanType())
56  return assumeExpr(
57  State, Sym,
58  SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
59 
60  return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
61  }
62 
64  const llvm::APSInt &From,
65  const llvm::APSInt &To,
66  bool InRange) override {
68  return assumeExpr(
69  State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
70  }
71 
73  bool Assumption) override {
74  // Skip anything that is unsupported
75  return State;
76  }
77 
78  //===------------------------------------------------------------------===//
79  // Implementation for interface from ConstraintManager.
80  //===------------------------------------------------------------------===//
81 
84 
85  QualType RetTy;
86  // The expression may be casted, so we cannot call getZ3DataExpr() directly
87  llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
88  llvm::SMTExprRef Exp =
89  SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
90 
91  // Negate the constraint
92  llvm::SMTExprRef NotExp =
93  SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
94 
95  ConditionTruthVal isSat = checkModel(State, Sym, Exp);
96  ConditionTruthVal isNotSat = checkModel(State, Sym, NotExp);
97 
98  // Zero is the only possible solution
99  if (isSat.isConstrainedTrue() && isNotSat.isConstrainedFalse())
100  return true;
101 
102  // Zero is not a solution
103  if (isSat.isConstrainedFalse() && isNotSat.isConstrainedTrue())
104  return false;
105 
106  // Zero may be a solution
107  return ConditionTruthVal();
108  }
109 
111  SymbolRef Sym) const override {
113  ASTContext &Ctx = BVF.getContext();
114 
115  if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
116  QualType Ty = Sym->getType();
117  assert(!Ty->isRealFloatingType());
120 
121  // TODO: this should call checkModel so we can use the cache, however,
122  // this method tries to get the interpretation (the actual value) from
123  // the solver, which is currently not cached.
124 
125  llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);
126 
127  Solver->reset();
129 
130  // Constraints are unsatisfiable
131  Optional<bool> isSat = Solver->check();
132  if (!isSat.hasValue() || !isSat.getValue())
133  return nullptr;
134 
135  // Model does not assign interpretation
136  if (!Solver->getInterpretation(Exp, Value))
137  return nullptr;
138 
139  // A value has been obtained, check if it is the only value
140  llvm::SMTExprRef NotExp = SMTConv::fromBinOp(
141  Solver, Exp, BO_NE,
142  Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue())
143  : Solver->mkBitvector(Value, Value.getBitWidth()),
144  /*isSigned=*/false);
145 
146  Solver->addConstraint(NotExp);
147 
148  Optional<bool> isNotSat = Solver->check();
149  if (!isNotSat.hasValue() || isNotSat.getValue())
150  return nullptr;
151 
152  // This is the only solution, store it
153  return &BVF.getValue(Value);
154  }
155 
156  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
157  SymbolRef CastSym = SC->getOperand();
158  QualType CastTy = SC->getType();
159  // Skip the void type
160  if (CastTy->isVoidType())
161  return nullptr;
162 
163  const llvm::APSInt *Value;
164  if (!(Value = getSymVal(State, CastSym)))
165  return nullptr;
166  return &BVF.Convert(SC->getType(), *Value);
167  }
168 
169  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
170  const llvm::APSInt *LHS, *RHS;
171  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
172  LHS = getSymVal(State, SIE->getLHS());
173  RHS = &SIE->getRHS();
174  } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
175  LHS = &ISE->getLHS();
176  RHS = getSymVal(State, ISE->getRHS());
177  } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
178  // Early termination to avoid expensive call
179  LHS = getSymVal(State, SSM->getLHS());
180  RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
181  } else {
182  llvm_unreachable("Unsupported binary expression to get symbol value!");
183  }
184 
185  if (!LHS || !RHS)
186  return nullptr;
187 
188  llvm::APSInt ConvertedLHS, ConvertedRHS;
189  QualType LTy, RTy;
190  std::tie(ConvertedLHS, LTy) = SMTConv::fixAPSInt(Ctx, *LHS);
191  std::tie(ConvertedRHS, RTy) = SMTConv::fixAPSInt(Ctx, *RHS);
192  SMTConv::doIntTypeConversion<llvm::APSInt, &SMTConv::castAPSInt>(
193  Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy);
194  return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
195  }
196 
197  llvm_unreachable("Unsupported expression to get symbol value!");
198  }
199 
201  SymbolReaper &SymReaper) override {
202  auto CZ = State->get<ConstraintSMT>();
203  auto &CZFactory = State->get_context<ConstraintSMT>();
204 
205  for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
206  if (SymReaper.isDead(I->first))
207  CZ = CZFactory.remove(CZ, *I);
208  }
209 
210  return State->set<ConstraintSMT>(CZ);
211  }
212 
213  void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
214  unsigned int Space = 0, bool IsDot = false) const override {
215  ConstraintSMTType Constraints = State->get<ConstraintSMT>();
216 
217  Indent(Out, Space, IsDot) << "\"constraints\": ";
218  if (Constraints.isEmpty()) {
219  Out << "null," << NL;
220  return;
221  }
222 
223  ++Space;
224  Out << '[' << NL;
225  for (ConstraintSMTType::iterator I = Constraints.begin();
226  I != Constraints.end(); ++I) {
227  Indent(Out, Space, IsDot)
228  << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
229  I->second->print(Out);
230  Out << "\" }";
231 
232  if (std::next(I) != Constraints.end())
233  Out << ',';
234  Out << NL;
235  }
236 
237  --Space;
238  Indent(Out, Space, IsDot) << "],";
239  }
240 
242  ProgramStateRef S2) const override {
243  return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
244  }
245 
246  bool canReasonAbout(SVal X) const override {
248 
250  if (!SymVal)
251  return true;
252 
253  const SymExpr *Sym = SymVal->getSymbol();
254  QualType Ty = Sym->getType();
255 
256  // Complex types are not modeled
257  if (Ty->isComplexType() || Ty->isComplexIntegerType())
258  return false;
259 
260  // Non-IEEE 754 floating-point types are not modeled
261  if ((Ty->isSpecificBuiltinType(BuiltinType::LongDouble) &&
262  (&TI.getLongDoubleFormat() == &llvm::APFloat::x87DoubleExtended() ||
263  &TI.getLongDoubleFormat() == &llvm::APFloat::PPCDoubleDouble())))
264  return false;
265 
266  if (Ty->isRealFloatingType())
267  return Solver->isFPSupported();
268 
269  if (isa<SymbolData>(Sym))
270  return true;
271 
272  SValBuilder &SVB = getSValBuilder();
273 
274  if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
275  return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
276 
277  if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
278  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
279  return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
280 
281  if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE))
282  return canReasonAbout(SVB.makeSymbolVal(ISE->getRHS()));
283 
284  if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE))
285  return canReasonAbout(SVB.makeSymbolVal(SSE->getLHS())) &&
286  canReasonAbout(SVB.makeSymbolVal(SSE->getRHS()));
287  }
288 
289  llvm_unreachable("Unsupported expression to reason about!");
290  }
291 
292  /// Dumps SMT formula
293  LLVM_DUMP_METHOD void dump() const { Solver->dump(); }
294 
295 protected:
296  // Check whether a new model is satisfiable, and update the program state.
298  const llvm::SMTExprRef &Exp) {
299  // Check the model, avoid simplifying AST to save time
300  if (checkModel(State, Sym, Exp).isConstrainedTrue())
301  return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
302 
303  return nullptr;
304  }
305 
306  /// Given a program state, construct the logical conjunction and add it to
307  /// the solver
309  // TODO: Don't add all the constraints, only the relevant ones
310  auto CZ = State->get<ConstraintSMT>();
311  auto I = CZ.begin(), IE = CZ.end();
312 
313  // Construct the logical AND of all the constraints
314  if (I != IE) {
315  std::vector<llvm::SMTExprRef> ASTs;
316 
317  llvm::SMTExprRef Constraint = I++->second;
318  while (I != IE) {
319  Constraint = Solver->mkAnd(Constraint, I++->second);
320  }
321 
322  Solver->addConstraint(Constraint);
323  }
324  }
325 
326  // Generate and check a Z3 model, using the given constraint.
328  const llvm::SMTExprRef &Exp) const {
329  ProgramStateRef NewState =
330  State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
331 
332  llvm::FoldingSetNodeID ID;
333  NewState->get<ConstraintSMT>().Profile(ID);
334 
335  unsigned hash = ID.ComputeHash();
336  auto I = Cached.find(hash);
337  if (I != Cached.end())
338  return I->second;
339 
340  Solver->reset();
341  addStateConstraints(NewState);
342 
343  Optional<bool> res = Solver->check();
344  if (!res.hasValue())
345  Cached[hash] = ConditionTruthVal();
346  else
347  Cached[hash] = ConditionTruthVal(res.getValue());
348 
349  return Cached[hash];
350  }
351 
352  // Cache the result of an SMT query (true, false, unknown). The key is the
353  // hash of the constraints in a state
354  mutable llvm::DenseMap<unsigned, ConditionTruthVal> Cached;
355 }; // end class SMTConstraintManager
356 
357 } // namespace ento
358 } // namespace clang
359 
360 #endif
clang::ento::SMTConstraintManager::assumeExpr
virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym, const llvm::SMTExprRef &Exp)
Definition: SMTConstraintManager.h:297
clang::TargetInfo::getLongDoubleFormat
const llvm::fltSemantics & getLongDoubleFormat() const
Definition: TargetInfo.h:670
clang::ento::BasicValueFactory
Definition: BasicValueFactory.h:108
clang::ento::SMTConstraintManager::SMTConstraintManager
SMTConstraintManager(clang::ento::ExprEngine *EE, clang::ento::SValBuilder &SB)
Definition: SMTConstraintManager.h:34
clang::ento::SMTConstraintManager::assumeSym
ProgramStateRef assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption) override
Given a symbolic expression that can be reasoned about, assume that it is true/false and generate the...
Definition: SMTConstraintManager.h:43
TargetInfo.h
clang::ento::SValBuilder::makeSymbolVal
SVal makeSymbolVal(SymbolRef Sym)
Make an SVal that represents the given symbol.
Definition: SValBuilder.h:399
clang::QualType
A (possibly-)qualified type.
Definition: Type.h:673
clang::ento::ConditionTruthVal::isConstrainedFalse
bool isConstrainedFalse() const
Return true if the constraint is perfectly constrained to 'false'.
Definition: ConstraintManager.h:61
clang::ento::BinarySymExpr
Represents a symbolic expression involving a binary operator.
Definition: SymbolManager.h:313
clang::TargetInfo
Exposes information about the current target.
Definition: TargetInfo.h:189
clang::Type::isRealFloatingType
bool isRealFloatingType() const
Floating point categories.
Definition: Type.cpp:2113
llvm::Optional< bool >
clang::ento::SMTConstraintManager::checkNull
ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override
Returns whether or not a symbol is known to be null ("true"), known to be non-null ("false"),...
Definition: SMTConstraintManager.h:82
clang::Type::isVoidType
bool isVoidType() const
Definition: Type.h:6956
clang::tooling::X
static ToolExecutorPluginRegistry::Add< AllTUsToolExecutorPlugin > X("all-TUs", "Runs FrontendActions on all TUs in the compilation database. " "Tool results are stored in memory.")
clang::ento::SMTConv::getRangeExpr
static llvm::SMTExprRef getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange)
Definition: SMTConv.h:508
clang::ento::SMTConv::getZeroExpr
static llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const llvm::SMTExprRef &Exp, QualType Ty, bool Assumption)
Definition: SMTConv.h:477
REGISTER_TRAIT_WITH_PROGRAMSTATE
#define REGISTER_TRAIT_WITH_PROGRAMSTATE(Name, Type)
Declares a program state trait for type Type called Name, and introduce a type named NameTy.
Definition: ProgramStateTrait.h:33
clang::ento::SymbolCast
Represents a cast expression.
Definition: SymbolManager.h:264
clang::ento::SMTConstraintManager::printJson
void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL="\n", unsigned int Space=0, bool IsDot=false) const override
Definition: SMTConstraintManager.h:213
clang::ento::ConditionTruthVal
Definition: ConstraintManager.h:38
APSInt
llvm::APSInt APSInt
Definition: ByteCodeEmitter.cpp:19
JsonSupport.h
clang::ento::SymbolReaper::isDead
bool isDead(SymbolRef sym)
Returns whether or not a symbol has been confirmed dead.
Definition: SymbolManager.h:570
clang::ento::SMTConstraintManager::assumeSymInclusiveRange
ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From, const llvm::APSInt &To, bool InRange) override
Given a symbolic expression within the range [From, To], assume that it is true/false and generate th...
Definition: SMTConstraintManager.h:63
clang::Type::isSignedIntegerOrEnumerationType
bool isSignedIntegerOrEnumerationType() const
Determines whether this is an integer type that is signed or an enumeration types whose underlying ty...
Definition: Type.cpp:2025
clang::ento::SymExpr::getType
virtual QualType getType() const =0
clang::ento::BasicValueFactory::Convert
const llvm::APSInt & Convert(const llvm::APSInt &To, const llvm::APSInt &From)
Convert - Create a new persistent APSInt with the same value as 'From' but with the bitwidth and sign...
Definition: BasicValueFactory.h:157
clang::ento::SMTConstraintManager::dump
LLVM_DUMP_METHOD void dump() const
Dumps SMT formula.
Definition: SMTConstraintManager.h:293
clang::ento::SimpleConstraintManager::getSValBuilder
SValBuilder & getSValBuilder() const
Definition: SimpleConstraintManager.h:77
clang::ento::SMTConstraintManager::checkModel
ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, const llvm::SMTExprRef &Exp) const
Definition: SMTConstraintManager.h:327
ConstraintSMTType
llvm::ImmutableSet< std::pair< clang::ento::SymbolRef, const llvm::SMTExpr * > > ConstraintSMTType
Definition: SMTConstraintManager.h:24
clang::ASTContext
Holds long-lived AST nodes (such as types and decls) that can be referred to throughout the semantic ...
Definition: ASTContext.h:212
clang::ento::SymExpr
Symbolic value.
Definition: SymExpr.h:29
clang::Type::isComplexType
bool isComplexType() const
isComplexType() does not include complex integers (a GCC extension).
Definition: Type.cpp:601
clang::ento::SimpleConstraintManager::getBasicVals
BasicValueFactory & getBasicVals() const
Definition: SimpleConstraintManager.h:78
SMTConv.h
clang::ASTContext::getTypeSize
uint64_t getTypeSize(QualType T) const
Return the size of the specified (complete) type T, in bits.
Definition: ASTContext.h:2245
clang::ento::SMTConstraintManager::getSymVal
const llvm::APSInt * getSymVal(ProgramStateRef State, SymbolRef Sym) const override
If a symbol is perfectly constrained to a constant, attempt to return the concrete value.
Definition: SMTConstraintManager.h:110
clang::ento::SMTConstraintManager::addStateConstraints
virtual void addStateConstraints(ProgramStateRef State) const
Given a program state, construct the logical conjunction and add it to the solver.
Definition: SMTConstraintManager.h:308
clang::ento::SymbolReaper
A class responsible for cleaning up unused symbols.
Definition: SymbolManager.h:505
clang::ento::SMTConstraintManager::haveEqualConstraints
bool haveEqualConstraints(ProgramStateRef S1, ProgramStateRef S2) const override
Definition: SMTConstraintManager.h:241
clang::interp::InRange
bool InRange(InterpState &S, CodePtr OpPC)
Definition: Interp.h:266
clang::ento::ConditionTruthVal::isConstrainedTrue
bool isConstrainedTrue() const
Return true if the constraint is perfectly constrained to 'true'.
Definition: ConstraintManager.h:56
clang::ento::BasicValueFactory::getContext
ASTContext & getContext() const
Definition: BasicValueFactory.h:136
clang::ento::SValBuilder
Definition: SValBuilder.h:53
clang::Indent
raw_ostream & Indent(raw_ostream &Out, const unsigned int Space, bool IsDot)
Definition: JsonSupport.h:20
clang::ento::BinarySymExprImpl
Template implementation for all binary symbolic expressions.
Definition: SymbolManager.h:360
clang::Type::isComplexIntegerType
bool isComplexIntegerType() const
Definition: Type.cpp:607
clang::ento::SMTConstraintManager
Definition: SMTConstraintManager.h:30
Value
Value
Definition: UninitializedValues.cpp:102
clang::ento::SMTConv::fromBinOp
static llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, const BinaryOperator::Opcode Op, const llvm::SMTExprRef &RHS, bool isSigned)
Construct an SMTSolverRef from a binary operator.
Definition: SMTConv.h:90
State
LineState State
Definition: UnwrappedLineFormatter.cpp:986
clang::ASTContext::getTargetInfo
const TargetInfo & getTargetInfo() const
Definition: ASTContext.h:747
clang::Type::isBooleanType
bool isBooleanType() const
Definition: Type.h:7072
clang::ento::ExprEngine
Definition: ExprEngine.h:127
clang::ento::nonloc::SymbolVal
Represents symbolic expression that isn't a location.
Definition: SVals.h:356
clang::Builtin::ID
ID
Definition: Builtins.h:48
clang
Definition: CalledOnceCheck.h:17
clang::ento::SMTConstraintManager::Cached
llvm::DenseMap< unsigned, ConditionTruthVal > Cached
Definition: SMTConstraintManager.h:354
clang::ento::SymbolData
A symbol representing data which can be stored in a memory location (region).
Definition: SymExpr.h:116
clang::ento::BasicValueFactory::evalAPSInt
const llvm::APSInt * evalAPSInt(BinaryOperator::Opcode Op, const llvm::APSInt &V1, const llvm::APSInt &V2)
Definition: BasicValueFactory.cpp:250
clang::ento::SMTConstraintManager::removeDeadBindings
ProgramStateRef removeDeadBindings(ProgramStateRef State, SymbolReaper &SymReaper) override
Scan all symbols referenced by the constraints.
Definition: SMTConstraintManager.h:200
clang::ento::SVal
SVal - This represents a symbolic expression, which can be either an L-value or an R-value.
Definition: SVals.h:75
clang::ento::SimpleConstraintManager
Definition: SimpleConstraintManager.h:23
clang::ento::SMTConstraintManager::assumeSymUnsupported
ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym, bool Assumption) override
Given a symbolic expression that cannot be reasoned about, assume that it is zero/nonzero and add it ...
Definition: SMTConstraintManager.h:72
clang::ento::SMTConv::getExpr
static llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, QualType *RetTy=nullptr, bool *hasComparison=nullptr)
Definition: SMTConv.h:465
clang::ento::SMTConv::fixAPSInt
static std::pair< llvm::APSInt, QualType > fixAPSInt(ASTContext &Ctx, const llvm::APSInt &Int)
Definition: SMTConv.h:554
RangedConstraintManager.h
clang::Type::isSpecificBuiltinType
bool isSpecificBuiltinType(unsigned K) const
Test for a particular builtin type.
Definition: Type.h:6925
clang::ento::SMTConstraintManager::~SMTConstraintManager
virtual ~SMTConstraintManager()=default
clang::ento::SMTConstraintManager::canReasonAbout
bool canReasonAbout(SVal X) const override
canReasonAbout - Not all ConstraintManagers can accurately reason about all SVal values.
Definition: SMTConstraintManager.h:246
clang::ento::SMTConv::fromData
static llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym)
Construct an SMTSolverRef from a SymbolData.
Definition: SMTConv.h:323
llvm::IntrusiveRefCntPtr< const ProgramState >