Fixed issues with use-after-move

.clang-tidy

@@ -2,18 +2,18 @@
 # Disable everything first, then enable individual checks.
 Checks: >-
   -*,
+  bugprone-dangling-handle,
+  bugprone-infinite-loop,
+  bugprone-misplaced-widening-cast,
+  bugprone-signed-char-misuse,
+  bugprone-unused-return-value,
+  bugprone-use-after-move,
+  bugprone-virtual-near-miss,
   readability-braces-around-statements
 # Candidate checks that are not (yet) enabled:
 # bugprone-branch-clone,
 # bugprone-copy-constructor-init,
-# bugprone-dangling-handle,
-# bugprone-infinite-loop,
-# bugprone-misplaced-widening-cast,
 # bugprone-redundant-expression,
-# bugprone-signed-char-misuse,
-# bugprone-unused-return-value,
-# bugprone-use-after-move,
-# bugprone-virtual-near-miss,
 # clang-analyzer-core.*,
 # clang-analyzer-cplusplus.*,
 # clang-analyzer-deadcode.*,

resources/scripts/clang-tidy.sh

@@ -23,7 +23,8 @@ Selection:
                    <ref>...HEAD plus untracked files.
   <file>...        Only check the given files. Arguments are treated as
                    literal paths (matched as a substring of the recorded
-                   absolute path), relative to the repository root or absolute.
+                   absolute path), relative to the current directory or
+                   absolute.
   (neither)        Check the whole code base (the default).
 
 Options:
@@ -81,22 +82,49 @@ is_source_file() {
     is_cpp_file "$1" || is_header_file "$1"
 }
 
-# Reads newline-separated repository-relative paths from stdin and fills the
-# globals $files (displayable) and $regex (escaped absolute paths, '|'-joined).
+# Collapse redundant '.' and '..' path segments lexically, without resolving
+# symlinks, so that paths such as "$root/../src/foo.h" produce the same
+# absolute path as recorded in the compilation database.
+normalize_path() {
+    local path=$1 out="/" seg
+    local -a parts
+    IFS='/' read -r -a parts <<< "$path"
+    for seg in "${parts[@]}"; do
+        case "$seg" in
+            ''|'.') : ;;
+            '..') out=${out%/*} ;;
+            *) out="${out%/}/$seg" ;;
+        esac
+    done
+    printf '%s' "${out:-/}"
+}
+
+# Reads newline-separated paths from stdin and fills the globals $files
+# (displayable) and $regex (escaped absolute paths, '|'-joined).
+# Relative paths are resolved against the current directory ($1 = "cwd", for
+# explicit file arguments) or against the repository root ($1 = "repo", for
+# the repo-relative paths produced by git).
 files=()
 regex=""
 has_cpp=0
 has_header=0
 build_file_lists() {
-    local root file escaped
+    local mode=$1 root file abs escaped
     root=$(git_ rev-parse --show-toplevel) || die "not inside a git repository"
     while IFS= read -r file; do
         [ -z "$file" ] && continue
         is_source_file "$file" || continue
         case "$file" in
-            /*) escaped=$(escape_regex "$file") ;;
-            *) escaped=$(escape_regex "$root/$file") ;;
+            /*) abs=$file ;;
+            *)
+                if [ "$mode" = "cwd" ]; then
+                    abs="$PWD/$file"
+                else
+                    abs="$root/$file"
+                fi
+                ;;
         esac
+        escaped=$(escape_regex "$(normalize_path "$abs")")
         regex="${regex:+$regex|}${escaped}"
         files+=("$file")
         is_cpp_file "$file" && has_cpp=1
@@ -208,15 +236,15 @@ fi
 echo "Using run-clang-tidy executable: $run_clang_tidy_bin"
 
 if [ "$git_ref_mode" -eq 1 ]; then
-    build_file_lists < <(changed_files "$git_ref")
+    build_file_lists repo < <(changed_files "$git_ref")
     if [ "${#files[@]}" -eq 0 ]; then
         echo "No source files changed relative to $git_ref; nothing to check."
         exit 0
     fi
     echo "Checking ${#files[@]} file(s) changed relative to $git_ref:"
     printf '  %s\n' "${files[@]}"
 elif [ "$#" -gt 0 ]; then
-    build_file_lists < <(printf '%s\n' "$@")
+    build_file_lists cwd < <(printf '%s\n' "$@")
     if [ "${#files[@]}" -eq 0 ]; then
         echo "No source files selected; nothing to check."
         exit 0
@@ -239,7 +267,9 @@ args=()
 
 if [ "$dry_run" -eq 1 ]; then
     printf 'PYTHONUNBUFFERED=1 %s' "$run_clang_tidy_bin"
-    printf ' %q' "${args[@]}"
+    for a in "${args[@]}"; do
+        printf ' %q' "$a"
+    done
     if [ "${#files[@]}" -gt 0 ]; then
         printf ' %q' "$regex"
     fi

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -130,6 +130,8 @@ storm::generator::StateBehavior<ValueType, StateType> DftNextStateGenerator<Valu
                                  "Self loop was added for " << unsuccessfulStateId << " and unsuccessful trigger of " << dependency->name());
             }
             result.addChoice(std::move(choice));
+            // Start a fresh choice for the next conflicting dependency.
+            choice = storm::generator::Choice<ValueType, StateType>(0, !exploreDependencies);
 
             // Handle premature stop for dependencies
             if (!iterFailable.isConflictingDependency()) {

src/storm-pars/modelchecker/region/monotonicity/MonotonicityResult.cpp

@@ -18,7 +18,7 @@ MonotonicityResult<VariableType>::MonotonicityResult() {
 
 template<typename VariableType>
 void MonotonicityResult<VariableType>::addMonotonicityResult(VariableType var, MonotonicityResult<VariableType>::Monotonicity mon) {
-    monotonicityResult.insert(std::pair<VariableType, MonotonicityResult<VariableType>::Monotonicity>(std::move(var), std::move(mon)));
+    monotonicityResult.insert(std::pair<VariableType, MonotonicityResult<VariableType>::Monotonicity>(std::move(var), mon));
 }
 
 template<typename VariableType>
@@ -27,7 +27,7 @@ void MonotonicityResult<VariableType>::updateMonotonicityResult(VariableType var
     if (force) {
         STORM_LOG_ASSERT(mon == MonotonicityResult<VariableType>::Monotonicity::Not, "Expected Not monotonicity for force.");
         if (monotonicityResult.find(var) == monotonicityResult.end()) {
-            addMonotonicityResult(std::move(var), std::move(mon));
+            addMonotonicityResult(std::move(var), mon);
         } else {
             monotonicityResult[var] = mon;
         }
@@ -36,20 +36,24 @@ void MonotonicityResult<VariableType>::updateMonotonicityResult(VariableType var
             mon = MonotonicityResult<VariableType>::Monotonicity::Unknown;
         }
 
+        bool unknownMon = false;
         if (monotonicityResult.find(var) == monotonicityResult.end()) {
-            addMonotonicityResult(std::move(var), std::move(mon));
+            addMonotonicityResult(std::move(var), mon);
+            unknownMon = (mon == MonotonicityResult<VariableType>::Monotonicity::Unknown);
         } else {
             auto monRes = monotonicityResult[var];
             if (monRes == MonotonicityResult<VariableType>::Monotonicity::Unknown || monRes == mon ||
                 mon == MonotonicityResult<VariableType>::Monotonicity::Constant) {
                 return;
             } else if (mon == MonotonicityResult<VariableType>::Monotonicity::Unknown || monRes == MonotonicityResult<VariableType>::Monotonicity::Constant) {
                 monotonicityResult[var] = mon;
+                unknownMon = (mon == MonotonicityResult<VariableType>::Monotonicity::Unknown);
             } else {
                 monotonicityResult[var] = MonotonicityResult<VariableType>::Monotonicity::Unknown;
+                unknownMon = true;
             }
         }
-        if (monotonicityResult[var] == MonotonicityResult<VariableType>::Monotonicity::Unknown) {
+        if (unknownMon) {
             setAllMonotonicity(false);
             setSomewhereMonotonicity(false);
         } else {

src/storm/modelchecker/helper/indefinitehorizon/visitingtimes/SparseDeterministicVisitingTimesHelper.cpp

@@ -471,9 +471,17 @@ std::vector<ValueType> SparseDeterministicVisitingTimesHelper<ValueType>::comput
     }
 
     // Get the solver object and satisfy requirements
+    // The solver consumes the matrix, so the acyclic check must be performed before moving it.
+    auto req = linearEquationSolverFactory.getRequirements(env);
+    if (req.acyclic().isCritical()) {
+        // The solver consumes the matrix, so the acyclic check must be performed before moving it.
+        STORM_LOG_THROW(!storm::utility::graph::hasCycle(sccMatrix), storm::exceptions::UnmetRequirementException,
+                        "The solver requires an acyclic model, but the model is not acyclic.");
+        req.clearAcyclic();
+    }
     auto solver = linearEquationSolverFactory.create(env, std::move(sccMatrix));
     solver->setLowerBound(storm::utility::zero<ValueType>());
-    auto req = solver->getRequirements(env);
+    req = solver->getRequirements(env);
     req.clearLowerBounds();
     if (req.upperBounds().isCritical()) {
         // Compute upper bounds on EVTs using techniques from Baier et al. [CAV'17] (https://doi.org/10.1007/978-3-319-63387-9_8)
@@ -482,12 +490,6 @@ std::vector<ValueType> SparseDeterministicVisitingTimesHelper<ValueType>::comput
         req.clearUpperBounds();
     }
 
-    if (req.acyclic().isCritical()) {
-        STORM_LOG_THROW(!storm::utility::graph::hasCycle(sccMatrix), storm::exceptions::UnmetRequirementException,
-                        "The solver requires an acyclic model, but the model is not acyclic.");
-        req.clearAcyclic();
-    }
-
     STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException,
                     "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
     std::vector<ValueType> eqSysValues(initialValues.size());
@@ -500,4 +502,4 @@ template class SparseDeterministicVisitingTimesHelper<storm::RationalNumber>;
 template class SparseDeterministicVisitingTimesHelper<storm::RationalFunction>;
 }  // namespace helper
 }  // namespace modelchecker
-}  // namespace storm
+}  // namespace storm

src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

@@ -141,10 +141,12 @@ std::vector<SolutionType> computeRobustValuesForMaybeStates(Environment const& e
 
     // Set up the solver.
     storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType, SolutionType> minMaxLinearEquationSolverFactory;
+    // The goal is consumed by the solver configuration, so capture what is needed first.
+    auto const uncertaintyResolutionMode = goal.getUncertaintyResolutionMode();
     std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType, SolutionType>> solver = storm::solver::configureMinMaxLinearEquationSolver(
         env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix),
         convert(OptimizationDirection::Maximize));  // default to maximize for IDTMCs; does not affect the result
-    solver->setUncertaintyResolutionMode(goal.getUncertaintyResolutionMode());
+    solver->setUncertaintyResolutionMode(uncertaintyResolutionMode);
     solver->setHasUniqueSolution(computeReward);  // As we check for graph-preservation, in case of rewards on IDTMCs, we have a unique solution
     solver->setHasNoEndComponents(false);
 

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -436,12 +436,14 @@ MaybeStateResult<SolutionType> computeValuesForMaybeStates(Environment const& en
                             : std::vector<SolutionType>(submatrix.getRowGroupCount(),
                                                         hint.hasLowerResultBound() ? hint.getLowerResultBound() : storm::utility::zero<SolutionType>());
 
+    // Capture the uncertainty resolution mode before the goal is consumed by the solver configuration.
+    auto const uncertaintyResolutionMode = goal.getUncertaintyResolutionMode();
     // Set up the solver.
     storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType, SolutionType> minMaxLinearEquationSolverFactory;
     std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType, SolutionType>> solver =
         storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix));
     solver->setRequirementsChecked();
-    solver->setUncertaintyResolutionMode(goal.getUncertaintyResolutionMode());
+    solver->setUncertaintyResolutionMode(uncertaintyResolutionMode);
     solver->setHasUniqueSolution(hint.hasUniqueSolution());
     solver->setHasNoEndComponents(hint.hasNoEndComponents());
     if (hint.hasLowerResultBound()) {
@@ -578,14 +580,13 @@ void extractSchedulerChoices(storm::storage::Scheduler<SolutionType>& scheduler,
 }
 
 template<typename ValueType, typename SolutionType>
-void extendScheduler(storm::storage::Scheduler<SolutionType>& scheduler, storm::solver::SolveGoal<ValueType, SolutionType> const& goal,
-                     QualitativeStateSetsUntilProbabilities const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
-                     storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates,
-                     storm::storage::BitVector const& psiStates) {
+void extendScheduler(storm::storage::Scheduler<SolutionType>& scheduler, bool minimize, QualitativeStateSetsUntilProbabilities const& qualitativeStateSets,
+                     storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
+                     storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
     // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for
     // the states with probability 1 or 0 (depending on whether we maximize or minimize).
     // We also need to define some arbitrary choice for the remaining states to obtain a fully defined scheduler.
-    if (goal.minimize()) {
+    if (minimize) {
         storm::utility::graph::computeSchedulerProb0E(qualitativeStateSets.statesWithProbability0, transitionMatrix, scheduler);
         for (auto prob1State : qualitativeStateSets.statesWithProbability1) {
             scheduler.setChoice(0, prob1State);
@@ -704,6 +705,8 @@ MDPSparseModelCheckingHelperReturnType<SolutionType> SparseMdpPrctlHelper<ValueT
     // Check if the values of the maybe states are relevant for the SolveGoal
     bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates);
 
+    // Capture the goal direction before the goal is consumed by the solver configuration.
+    bool const minimize = goal.minimize();
     // If requested, we will produce a scheduler.
     std::unique_ptr<storm::storage::Scheduler<SolutionType>> scheduler;
     if (produceScheduler) {
@@ -778,7 +781,7 @@ MDPSparseModelCheckingHelperReturnType<SolutionType> SparseMdpPrctlHelper<ValueT
 
     // Extend scheduler with choices for the states in the qualitative state sets.
     if (produceScheduler) {
-        extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, phiStates, psiStates);
+        extendScheduler(*scheduler, minimize, qualitativeStateSets, transitionMatrix, backwardTransitions, phiStates, psiStates);
     }
 
     // Sanity check for created scheduler.
@@ -1161,13 +1164,12 @@ QualitativeStateSetsReachabilityRewards getQualitativeStateSetsReachabilityRewar
 }
 
 template<typename ValueType, typename SolutionType>
-void extendScheduler(storm::storage::Scheduler<SolutionType>& scheduler, storm::solver::SolveGoal<ValueType, SolutionType> const& goal,
-                     QualitativeStateSetsReachabilityRewards const& qualitativeStateSets, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
-                     storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates,
-                     std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter) {
+void extendScheduler(storm::storage::Scheduler<SolutionType>& scheduler, bool minimize, QualitativeStateSetsReachabilityRewards const& qualitativeStateSets,
+                     storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
+                     storm::storage::BitVector const& targetStates, std::function<storm::storage::BitVector()> const& zeroRewardChoicesGetter) {
     // Finally, if we need to produce a scheduler, we also need to figure out the parts of the scheduler for
     // the states with reward zero/infinity.
-    if (goal.minimize()) {
+    if (minimize) {
         storm::utility::graph::computeSchedulerProb1E(qualitativeStateSets.rewardZeroStates, transitionMatrix, backwardTransitions,
                                                       qualitativeStateSets.rewardZeroStates, targetStates, scheduler, zeroRewardChoicesGetter());
         for (auto state : qualitativeStateSets.infinityStates) {
@@ -1374,6 +1376,8 @@ MDPSparseModelCheckingHelperReturnType<SolutionType> SparseMdpPrctlHelper<ValueT
     // Check if the values of the maybe states are relevant for the SolveGoal
     bool maybeStatesNotRelevant = goal.hasRelevantValues() && goal.relevantValues().isDisjointFrom(qualitativeStateSets.maybeStates);
 
+    // Capture the goal direction before the goal is consumed by the solver configuration.
+    bool const minimize = goal.minimize();
     // Check whether we need to compute exact rewards for some states.
     if (qualitative || maybeStatesNotRelevant) {
         STORM_LOG_INFO("The rewards for the initial states were determined in a preprocessing step. No exact rewards were computed.");
@@ -1456,7 +1460,7 @@ MDPSparseModelCheckingHelperReturnType<SolutionType> SparseMdpPrctlHelper<ValueT
 
     // Extend scheduler with choices for the states in the qualitative state sets.
     if (produceScheduler) {
-        extendScheduler(*scheduler, goal, qualitativeStateSets, transitionMatrix, backwardTransitions, targetStates, zeroRewardChoicesGetter);
+        extendScheduler(*scheduler, minimize, qualitativeStateSets, transitionMatrix, backwardTransitions, targetStates, zeroRewardChoicesGetter);
     }
 
     // Sanity check for created scheduler.

src/storm/models/sparse/Ctmc.cpp

@@ -43,6 +43,7 @@ Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::sparse::ModelComponents<V
 template<typename ValueType, typename RewardModelType>
 Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components)
     : DeterministicModel<ValueType, RewardModelType>(storm::models::ModelType::Ctmc, std::move(components)) {
+    // NOLINTBEGIN(bugprone-use-after-move) The base constructor only consumes the base-relevant fields of components.
     if (components.exitRates) {
         exitRates = std::move(components.exitRates.get());
     } else {
@@ -53,6 +54,7 @@ Ctmc<ValueType, RewardModelType>::Ctmc(storm::storage::sparse::ModelComponents<V
     if (!components.rateTransitions) {
         this->getTransitionMatrix().scaleRowsInPlace(exitRates);
     }
+    // NOLINTEND(bugprone-use-after-move)
 }
 
 template<typename ValueType, typename RewardModelType>

src/storm/models/sparse/MarkovAutomaton.cpp

@@ -51,6 +51,7 @@ MarkovAutomaton<ValueType, RewardModelType>::MarkovAutomaton(storm::storage::spa
 template<typename ValueType, typename RewardModelType>
 MarkovAutomaton<ValueType, RewardModelType>::MarkovAutomaton(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components)
     : NondeterministicModel<ValueType, RewardModelType>(ModelType::MarkovAutomaton, std::move(components)),
+      // NOLINTBEGIN(bugprone-use-after-move) The base constructor only consumes the base-relevant fields of components.
       markovianStates(std::move(components.markovianStates.get())) {
     if (components.exitRates) {
         exitRates = std::move(components.exitRates.get());
@@ -59,6 +60,7 @@ MarkovAutomaton<ValueType, RewardModelType>::MarkovAutomaton(storm::storage::spa
     if (components.rateTransitions) {
         this->turnRatesToProbabilities();
     }
+    // NOLINTEND(bugprone-use-after-move)
     closed = this->checkIsClosed();
 }
 

src/storm/models/sparse/Model.cpp

@@ -585,7 +585,7 @@ void Model<ValueType, RewardModelType>::writeJsonToStream(std::ostream& outStrea
                 }
             }
             if (!choiceRewardsJson.empty()) {
-                choiceRewardsJson["rew"] = std::move(choiceRewardsJson);
+                choiceJson["rew"] = std::move(choiceRewardsJson);
             }
             storm::json<JsonValueType> successors;
             for (auto const& entry : transitionMatrix.getRow(choiceIndex)) {