added z3feedback

kframework · Jun 14, 2018 · 228d4d6 · 228d4d6
1 parent ff4d281
commit 228d4d6
Show file tree

Hide file tree

Showing 3 changed files with 66 additions and 6 deletions.
diff --git a/lib/local_tmp.js b/lib/local_tmp.js
@@ -244,6 +244,19 @@ const getcircc = (data, ch) => {
   });
 }
 
+const getz3feedback = (data, ch) => {
+  let d_ = data.split(" ");
+  let str = fs.readFileSync(path.join(KLAB_WD_PATH, `/${d_[0]}/circc/${d_[2]}.json`)).toString();
+  let z3feedback = JSON.parse(str);
+  ch({
+    type: "z3feedbackdata",
+    id: d_[0],
+    term: d_[1],
+    z3id: d_[2],
+    data: z3feedback
+  });
+}
+
 module.exports = (msg, ch) => {
   switch(msg.type) {
     case "run":
@@ -264,6 +277,9 @@ module.exports = (msg, ch) => {
     case "getcircc":
       getcircc(msg.data, ch);
       break;
+    case "getz3feedback":
+      getz3feedback(msg.data, ch);
+      break;
     default:
       console.log("dunno", msg);
   }

diff --git a/lib/show.js b/lib/show.js
@@ -4,6 +4,7 @@ const { formatStep } = require("./formatter.js");
 const { formatMemory } = require("./unwrapper.js");
 const { getCodeStringFromPc } = require("../lib/srchandler.js");
 const genBehaviour = require("./helper.js");
+const Constraints = require("./constraints.js");
 
 
 const formatRule = rule => {
@@ -93,6 +94,24 @@ const show = {
       // return formatted_memory;
     },
     toggle: ["m", "M"]
+  },
+  z3feedback: {
+    exec: (state, settings) => {
+      let id = state.path[state.path.length - 1].step.to;
+      let keys = Object.keys(state.z3feedback[id] || {});
+      let display = keys
+        .map(key => Object.assign({key}, state.z3feedback[id][key]))
+        .map(o => {
+          let result = o.result == "unknown"
+                     ? clc.red(o.result)
+                     : o.result;
+          return o.key + " " + result + "\n  " +
+            Constraints.clean(o.right).split("\n").join("\n  ")
+        })
+        .join("\n")
+      return display;
+    },
+    toggle: ["z", "Z"]
   }
 }
 

diff --git a/lib/stateHandler.js b/lib/stateHandler.js
@@ -27,6 +27,7 @@ module.exports = ({CLI, onion, K, Settings}) => {
     end: {},
     exception: {},
     revert: {},
+    z3feedback: {},
     show: {
       term: true
     },
@@ -113,6 +114,20 @@ module.exports = ({CLI, onion, K, Settings}) => {
         let rhs = Constraints.clean(circc.rhs)//.replace("\\n", "\n").split("\n").map(s => s.trim()).join("\n");
         updated.circc[id] = _.uniq([rhs].concat(updated.circc[id]));
       }
+      if(msg.type === "z3feedbackdata") {
+        let term_id = msg.term;
+        updated.z3feedback = Object.assign({}, prev.z3feedback);
+        if(!(term_id in updated.z3feedback)) updated.z3feedback[term_id] = [];
+        let z3id = msg.z3id;
+        updated.z3feedback[term_id][z3id] = msg.data;
+      }
+      if(msg.type === "z3feedback") {
+        let term_id = msg.data[0];
+        updated.z3feedback = Object.assign({}, prev.z3feedback);
+        if(!(term_id in updated.z3feedback)) updated.z3feedback[term_id] = {};
+        let z3id = msg.data[1];
+        updated.z3feedback[term_id][z3id] = {};
+      }
       return Object.assign({}, prev, updated);
     }
   })
@@ -133,11 +148,13 @@ module.exports = ({CLI, onion, K, Settings}) => {
         })
         steps = prev.edges[steps[0].to];
       }
-      updated.path.push({
-        type: "branch",
-        branch: parseInt(key),
-        step: steps[parseInt(key)]
-      })
+      if(typeof key == "string" && typeof parseInt(key) == "number" && steps[parseInt(key)]) {
+        updated.path.push({
+          type: "branch",
+          branch: parseInt(key),
+          step: steps[parseInt(key)]
+        })
+      }
     }
     if(key == "N") {
       // todo test this for crashing in init
@@ -253,6 +270,13 @@ module.exports = ({CLI, onion, K, Settings}) => {
     .compose(sampleCombine(onion.state$))
     .map(([msg, state]) => ({type:"getcircc", data: state.sid + " " + msg.data[0]}))
 
+  // this streams a lot
+  // TODO - flag or conditional
+  const z3feedbackRequest$ = K
+    .filter(msg => msg.type == "z3feedback")
+    .compose(sampleCombine(onion.state$))
+    .map(([msg, state]) => ({type:"getz3feedback", data: state.sid + " " + msg.data[0] + " " + msg.data[1]}))
+
   const branchingNodeRequest$ = K
     .filter(msg => msg.type == "specialnode" && msg.data[0] == "branch")
     .compose(sampleCombine(onion.state$))
@@ -263,7 +287,8 @@ module.exports = ({CLI, onion, K, Settings}) => {
     toNodeRequest$,
     ruleRequest$,
     circcRequest$,
-    branchingNodeRequest$
+    branchingNodeRequest$,
+    z3feedbackRequest$
   );
 
   return {