From 11baef6dd58fb5ba528b17c993069d12f8420332 Mon Sep 17 00:00:00 2001
From: Petr Rockai <me@mornfall.net>
Date: Sun, 16 Jun 2019 14:05:59 +0000
Subject: [PATCH] VM: Move loop tracking code into a separate header file.
---
divine/vm/context.hpp | 34 +++------------------------
divine/vm/loops.hpp | 53 +++++++++++++++++++++++++++++++++++++++++++
2 files changed, 56 insertions(+), 31 deletions(-)
create mode 100644 divine/vm/loops.hpp
diff --git a/divine/vm/context.hpp b/divine/vm/context.hpp
index 48daa6c96..738677327 100644
--- a/divine/vm/context.hpp
+++ b/divine/vm/context.hpp
@@ -18,10 +18,11 @@
#pragma once
+#include <divine/vm/loops.hpp>
+#include <divine/vm/frame.hpp>
#include <divine/vm/value.hpp>
#include <divine/vm/memory.hpp>
#include <divine/vm/types.hpp>
-#include <divine/vm/frame.hpp>
#include <divine/vm/divm.h>
#include <brick-data>
@@ -33,41 +34,12 @@ namespace llvm { class Value; }
namespace divine::vm
{
-
struct TraceSchedChoice { value::Pointer list; };
using Location = _VM_Operand::Location;
using PtrRegister = GenericPointer;
using IntRegister = uint64_t;
- struct LoopTrack
- {
- std::vector< std::unordered_set< GenericPointer > > loops;
-
- void entered( CodePointer )
- {
- loops.emplace_back();
- }
-
- void left( CodePointer )
- {
- loops.pop_back();
- if ( loops.empty() ) /* more returns than calls could happen along an edge */
- loops.emplace_back();
- }
-
- bool test_loop( CodePointer pc, int /* TODO */ )
- {
- /* TODO track the counter value too */
- if ( loops.back().count( pc ) )
- return true;
- else
- loops.back().insert( pc );
-
- return false;
- }
- };
-
/* state of a computation */
struct State
{
@@ -212,7 +184,7 @@ namespace divine::vm
struct Tracing : NoTracing
{
State _debug_state;
- LoopTrack _loops;
+ track_loops _loops;
PtrRegister _debug_pc;
int _debug_depth = 0;
diff --git a/divine/vm/loops.hpp b/divine/vm/loops.hpp
new file mode 100644
index 000000000..76bd54ffc
--- /dev/null
+++ b/divine/vm/loops.hpp
@@ -0,0 +1,53 @@
+// -*- mode: C++; indent-tabs-mode: nil; c-basic-offset: 4 -*-
+
+/*
+ * (c) 2019 Petr RoÄŤkai <code@fixp.eu>
+ *
+ * Permission to use, copy, modify, and distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ */
+
+#pragma once
+
+#include <divine/vm/pointer.hpp>
+#include <unordered_set>
+
+namespace divine::vm
+{
+ struct track_loops
+ {
+ std::vector< std::unordered_set< GenericPointer > > loops;
+
+ void entered( CodePointer )
+ {
+ loops.emplace_back();
+ }
+
+ void left( CodePointer )
+ {
+ loops.pop_back();
+ if ( loops.empty() ) /* more returns than calls could happen along an edge */
+ loops.emplace_back();
+ }
+
+ bool test_loop( CodePointer pc, int /* TODO */ )
+ {
+ /* TODO track the counter value too */
+ if ( loops.back().count( pc ) )
+ return true;
+ else
+ loops.back().insert( pc );
+
+ return false;
+ }
+ };
+}
--
GitLab