First attempt at state property generalization

cksystemsteaching · Dec 13, 2023 · 62c873a · 62c873a
1 parent 1b4bdb3
commit 62c873a
Showing 1 changed file with 137 additions and 147 deletions.
diff --git a/tools/rotor.c b/tools/rotor.c
@@ -579,6 +579,8 @@ uint64_t* core_control_flow();
 
 // ------------------------ GLOBAL CONSTANTS -----------------------
 
+uint64_t SYNTHESIZE = 1;
+
 // RISC-V codes missing in RISC-U
 
 uint64_t F3_LB = 0;
@@ -732,10 +734,13 @@ uint64_t* next_core_pc_nid = (uint64_t*) 0;
 // ------------------------ MODEL GENERATOR ------------------------
 // -----------------------------------------------------------------
 
-void output_machine();
+uint64_t* state_property(uint64_t* good_nid, uint64_t* bad_nid, char* symbol, char* comment);
 
+void kernel();
 void rotor();
 
+void output_machine();
+
 uint64_t selfie_model();
 
 // ------------------------ GLOBAL VARIABLES -----------------------
@@ -747,9 +752,9 @@ uint64_t w = 0; // number of written characters
 
 uint64_t bad_exit_code = 0; // model for this exit code
 
-uint64_t* constraint_ir_nid = (uint64_t*) 0;
+uint64_t* is_instruction_known_nid = (uint64_t*) 0;
+uint64_t* is_next_fetch_in_code_segment_nid = (uint64_t*) 0;
 
-uint64_t* bad_pc_nid = (uint64_t*) 0;
 uint64_t* bad_read_nid = (uint64_t*) 0;
 uint64_t* bad_syscall_id_nid = (uint64_t*) 0;
 uint64_t* bad_exit_nid = (uint64_t*) 0;
@@ -1119,6 +1124,8 @@ void print_memory_sorts() {
  print_line(80, SID_CODE_ADDRESS);
  print_line(81, SID_CODE_STATE);
 
+ w = w + dprintf(output_fd, "\n");
+
  if (ISBYTEMEMORY) {
  print_line(90, SID_MEMORY_ADDRESS);
  print_line(91, SID_MEMORY_STATE);
@@ -1503,112 +1510,18 @@ void new_core_state() {
 // ------------------------ MODEL GENERATOR ------------------------
 // -----------------------------------------------------------------
 
-void output_machine() {
- w = w
- + dprintf(output_fd, "; %s\n\n", SELFIE_URL)
- + dprintf(output_fd, "; BTOR2 file %s generated by %s\n\n", model_name, selfie_name);
-
- print_interface_sorts();
- print_interface_memory();
- print_interface_kernel();
-
- print_register_sorts();
- print_memory_sorts();
-
- w = w + dprintf(output_fd, "\n; kernel state\n\n");
-
- print_line(100, readable_bytes_nid);
- print_line(101, init_readable_bytes_nid);
-
- w = w + dprintf(output_fd, "\n");
-
- print_line(103, init_read_bytes_nid);
-
- w = w + dprintf(output_fd, "\n; register file\n\n");
-
- print_line(200, init_register_file_nid);
-
- w = w + dprintf(output_fd, "\n; code segment\n\n");
-
- print_line(300, state_code_segment_nid);
-
- w = w + dprintf(output_fd, "\n; main memory\n\n");
-
- print_line(400, init_main_memory_nid);
-
- w = w + dprintf(output_fd, "\n; program counter\n\n");
-
- print_line(1000, init_core_pc_nid);
-
- w = w + dprintf(output_fd, "\n; non-kernel control flow\n\n");
-
- print_line(2000, eval_core_pc_nid);
-
- w = w + dprintf(output_fd, "\n; update kernel state\n\n");
-
- print_line(3000, next_readable_bytes_nid);
-
- w = w + dprintf(output_fd, "\n");
+uint64_t* state_property(uint64_t* good_nid, uint64_t* bad_nid, char* symbol, char* comment) {
+ if (SYNTHESIZE) {
+ if (good_nid == UNUSED)
+ good_nid = new_unary(OP_NOT, SID_BOOLEAN, bad_nid, "asserting");
 
- print_line(3100, next_read_bytes_nid);
-
- w = w + dprintf(output_fd, "\n; kernel control flow\n\n");
-
- print_line(3200, eval_kernel_pc_nid);
-
- w = w + dprintf(output_fd, "\n; update program counter\n\n");
-
- print_line(4000, next_core_pc_nid);
-
- w = w + dprintf(output_fd, "\n; non-kernel register data flow\n\n");
-
- print_line(5000, eval_core_register_data_flow_nid);
-
- w = w + dprintf(output_fd, "\n; kernel register data flow\n\n");
-
- print_line(6000, eval_kernel_register_data_flow_nid);
-
- w = w + dprintf(output_fd, "\n; update register data flow\n\n");
-
- print_line(7000, next_register_file_nid);
-
- w = w + dprintf(output_fd, "\n; non-kernel memory data flow\n\n");
-
- print_line(8000, eval_core_memory_data_flow_nid);
-
- w = w + dprintf(output_fd, "\n; kernel memory data flow\n\n");
-
- print_line(9000, eval_kernel_memory_data_flow_nid);
-
- w = w + dprintf(output_fd, "\n; update memory data flow\n\n");
-
- print_line(10000, next_main_memory_nid);
-
- w = w + dprintf(output_fd, "\n; constraints\n\n");
-
- print_line(11000, constraint_ir_nid);
-
- w = w + dprintf(output_fd, "\n; bad states\n\n");
-
- print_line(12000, bad_pc_nid);
-
- w = w + dprintf(output_fd, "\n");
-
- print_line(12100, bad_read_nid);
-
- w = w + dprintf(output_fd, "\n");
-
- print_line(12200, bad_syscall_id_nid);
-
- w = w + dprintf(output_fd, "\n");
-
- print_line(12300, bad_exit_nid);
-
- w = w + dprintf(output_fd, "\n");
-
- //print_line(12400, bad_a0_nid);
+ return new_property(OP_CONSTRAINT, good_nid, symbol, comment);
+ } else {
+ if (bad_nid == UNUSED)
+ bad_nid = new_unary(OP_NOT, SID_BOOLEAN, good_nid, "targeting");
 
- //print_line(12500, bad_memory_nid);
+ return new_property(OP_BAD, bad_nid, symbol, comment);
+ }
 }
 
 void kernel() {
@@ -1833,20 +1746,6 @@ void kernel() {
  "b2", "unknown syscall ID");
 
  bad_exit_nid = new_property(OP_BAD,
- new_binary_boolean(OP_AND,
- new_binary_boolean(OP_AND,
- new_binary_boolean(OP_EQ,
- load_byte(new_constant(OP_CONSTD, SID_MACHINE_WORD, "129", "")),
- NID_BYTE_4, ""),
- new_binary_boolean(OP_AND,
- new_binary_boolean(OP_EQ,
- load_byte(new_constant(OP_CONSTD, SID_MACHINE_WORD, "130", "")),
- NID_BYTE_0, ""),
- new_binary_boolean(OP_EQ,
- load_byte(new_constant(OP_CONSTD, SID_MACHINE_WORD, "131", "")),
- NID_BYTE_4, ""),
- ""),
- ""),
  new_binary_boolean(OP_AND,
  active_exit_nid,
  new_binary_boolean(OP_EQ,
@@ -1856,12 +1755,11 @@ void kernel() {
  format_comment("bad exit code %ld", bad_exit_code)),
  "actual exit code == bad exit code"),
  "active exit system call with bad exit code"),
- ""),
  "b3", format_comment("exit(%ld)", bad_exit_code));
 }
 
 void rotor() {
- uint64_t* known_instruction_nid;
+ uint64_t* known_instructions_nid;
 
  new_kernel_state(2);
  new_register_file_state();
@@ -1874,7 +1772,7 @@ void rotor() {
 
  // decode
 
- known_instruction_nid = decode_instruction();
+ known_instructions_nid = decode_instruction();
 
  // non-kernel control flow
 
@@ -1913,32 +1811,124 @@ void rotor() {
  eval_kernel_memory_data_flow_nid,
  "main memory");
 
- // constraints
+ // state properties
 
- constraint_ir_nid = new_property(OP_CONSTRAINT,
+ is_instruction_known_nid = state_property(
  new_binary_boolean(OP_OR,
  eval_core_active_ecall_nid,
- known_instruction_nid,
- "ecall or known instruction"),
- "known-instructions", "known instructions");
-
- // bad states
-
- bad_pc_nid = new_property(OP_CONSTRAINT,
- //new_unary(OP_NOT, SID_BOOLEAN,
- is_access_in_code_segment(eval_kernel_pc_nid),
- //"next pc not in code segment"),
- "b0", "imminent fetch segmentation fault");
-
- bad_a0_nid = new_property(OP_CONSTRAINT,
- new_binary_boolean(OP_NEQ, get_instruction_rd(eval_core_ir_nid), NID_A0, ""),
- "b", "a0");
-
- bad_memory_nid = new_property(OP_BAD,
- new_binary_boolean(OP_EQ,
- load_byte(new_constant(OP_CONSTD, SID_MACHINE_WORD, "128", "")),
- NID_BYTE_4, ""),
- "b", "memory");
+ known_instructions_nid,
+ "ecall or other known instructions"),
+ UNUSED,
+ "known-instructions",
+ "known instructions");
+
+ is_next_fetch_in_code_segment_nid = state_property(
+ is_access_in_code_segment(eval_kernel_pc_nid),
+ UNUSED,
+ "fetch-seg-fault",
+ "imminent fetch segmentation fault");
+}
+
+void output_machine() {
+ w = w
+ + dprintf(output_fd, "; %s\n\n", SELFIE_URL)
+ + dprintf(output_fd, "; BTOR2 file %s generated by %s\n\n", model_name, selfie_name);
+
+ print_interface_sorts();
+ print_interface_memory();
+ print_interface_kernel();
+
+ print_register_sorts();
+ print_memory_sorts();
+
+ w = w + dprintf(output_fd, "\n; kernel state\n\n");
+
+ print_line(100, readable_bytes_nid);
+ print_line(101, init_readable_bytes_nid);
+
+ w = w + dprintf(output_fd, "\n");
+
+ print_line(103, init_read_bytes_nid);
+
+ w = w + dprintf(output_fd, "\n; register file\n\n");
+
+ print_line(200, init_register_file_nid);
+
+ w = w + dprintf(output_fd, "\n; code segment\n\n");
+
+ print_line(300, state_code_segment_nid);
+
+ w = w + dprintf(output_fd, "\n; main memory\n\n");
+
+ print_line(400, init_main_memory_nid);
+
+ w = w + dprintf(output_fd, "\n; program counter\n\n");
+
+ print_line(1000, init_core_pc_nid);
+
+ w = w + dprintf(output_fd, "\n; non-kernel control flow\n\n");
+
+ print_line(2000, eval_core_pc_nid);
+
+ w = w + dprintf(output_fd, "\n; update kernel state\n\n");
+
+ print_line(3000, next_readable_bytes_nid);
+
+ w = w + dprintf(output_fd, "\n");
+
+ print_line(3100, next_read_bytes_nid);
+
+ w = w + dprintf(output_fd, "\n; kernel control flow\n\n");
+
+ print_line(3200, eval_kernel_pc_nid);
+
+ w = w + dprintf(output_fd, "\n; update program counter\n\n");
+
+ print_line(4000, next_core_pc_nid);
+
+ w = w + dprintf(output_fd, "\n; non-kernel register data flow\n\n");
+
+ print_line(5000, eval_core_register_data_flow_nid);
+
+ w = w + dprintf(output_fd, "\n; kernel register data flow\n\n");
+
+ print_line(6000, eval_kernel_register_data_flow_nid);
+
+ w = w + dprintf(output_fd, "\n; update register data flow\n\n");
+
+ print_line(7000, next_register_file_nid);
+
+ w = w + dprintf(output_fd, "\n; non-kernel memory data flow\n\n");
+
+ print_line(8000, eval_core_memory_data_flow_nid);
+
+ w = w + dprintf(output_fd, "\n; kernel memory data flow\n\n");
+
+ print_line(9000, eval_kernel_memory_data_flow_nid);
+
+ w = w + dprintf(output_fd, "\n; update memory data flow\n\n");
+
+ print_line(10000, next_main_memory_nid);
+
+ w = w + dprintf(output_fd, "\n; state properties\n\n");
+
+ print_line(11000, is_instruction_known_nid);
+
+ w = w + dprintf(output_fd, "\n");
+
+ print_line(11100, is_next_fetch_in_code_segment_nid);
+
+ w = w + dprintf(output_fd, "\n");
+
+ print_line(11200, bad_read_nid);
+
+ w = w + dprintf(output_fd, "\n");
+
+ print_line(11300, bad_syscall_id_nid);
+
+ w = w + dprintf(output_fd, "\n");
+
+ print_line(11400, bad_exit_nid);
 }
 
 uint64_t selfie_model() {