From c4b78ad09e09cf09b429edba2fc64b669e9831dd Mon Sep 17 00:00:00 2001
From: Christoph Kirsch <ckirsch@gmail.com>
Date: Mon, 8 Jan 2024 16:25:09 +0100
Subject: [PATCH] Checking brk failing

---
 tools/rotor.c | 41 +++++++++++++++++++++++++++++------------
 1 file changed, 29 insertions(+), 12 deletions(-)

diff --git a/tools/rotor.c b/tools/rotor.c
index 1e4cbbc4..df0c3331 100644
--- a/tools/rotor.c
+++ b/tools/rotor.c
@@ -1249,6 +1249,7 @@ uint64_t* load_seg_faulting_nid       = (uint64_t*) 0;
 uint64_t* store_seg_faulting_nid      = (uint64_t*) 0;
 uint64_t* stack_seg_faulting_nid      = (uint64_t*) 0;
 
+uint64_t* brk_failing_nid         = (uint64_t*) 0;
 uint64_t* read_seg_faulting_nid   = (uint64_t*) 0;
 uint64_t* is_syscall_id_known_nid = (uint64_t*) 0;
 uint64_t* bad_exit_code_nid       = (uint64_t*) 0;
@@ -3284,7 +3285,7 @@ uint64_t* core_control_flow(uint64_t* pc_nid, uint64_t* ir_nid) {
 
 void new_core_state() {
   if (SYNTHESIZE)
-    initial_core_pc_nid = NID_MACHINE_WORD_0;
+    initial_core_pc_nid = new_constant(OP_CONSTH, SID_MACHINE_WORD, code_start, 8, "initial pc value");
   else
     initial_core_pc_nid = new_constant(OP_CONSTH, SID_MACHINE_WORD, get_pc(current_context), 8, "entry pc value");
 
@@ -3332,6 +3333,7 @@ void kernel(uint64_t* pc_nid, uint64_t* ir_nid, uint64_t* memory_nid) {
 
   uint64_t* a0_value_nid;
 
+  uint64_t* new_program_break_in_heap_segment_nid;
   uint64_t* new_program_break_nid;
 
   uint64_t* a2_value_nid;
@@ -3370,21 +3372,23 @@ void kernel(uint64_t* pc_nid, uint64_t* ir_nid, uint64_t* memory_nid) {
 
   // update brk kernel state
 
+  new_program_break_in_heap_segment_nid = new_binary_boolean(OP_AND,
+    new_binary_boolean(OP_UGTE,
+      a0_value_nid,
+      state_program_break_nid,
+      "new program break >= current program break?"),
+    new_binary_boolean(OP_ULTE,
+      a0_value_nid,
+      NID_HEAP_END,
+      "new program break <= end of heap segment?"),
+    "is new program break in heap segment?");
+
   new_program_break_nid =
     new_ternary(OP_ITE, SID_MACHINE_WORD,
-      new_binary_boolean(OP_AND,
-        new_binary_boolean(OP_UGTE,
-          a0_value_nid,
-          state_program_break_nid,
-          "new program break >= current program break?"),
-        new_binary_boolean(OP_ULTE,
-          a0_value_nid,
-          NID_HEAP_END,
-          "new program break <= end of heap segment?"),
-        "is new program break in heap segment?"),
+      new_program_break_in_heap_segment_nid,
       a0_value_nid,
       state_program_break_nid,
-      "");
+      "update a0 if new program break is in heap segment");
 
   next_program_break_nid =
     new_binary(OP_NEXT, SID_MACHINE_WORD,
@@ -3563,6 +3567,15 @@ void kernel(uint64_t* pc_nid, uint64_t* ir_nid, uint64_t* memory_nid) {
 
   // kernel properties
 
+  brk_failing_nid = state_property(
+    UNUSED,
+    new_binary_boolean(OP_AND,
+      active_brk_nid,
+      new_unary_boolean(OP_NOT, new_program_break_in_heap_segment_nid, ""),
+      "new program break is in heap segment if brk system call is active"),
+    "brk-failing",
+    "brk is failing");
+
   read_seg_faulting_nid = state_property(
     UNUSED,
     new_binary_boolean(OP_AND,
@@ -3824,6 +3837,10 @@ void output_model() {
 
   print_break("\n");
 
+  print_line(brk_failing_nid);
+
+  print_break("\n");
+
   print_line(read_seg_faulting_nid);
 
   print_break("\n");