Updated Documentation!

README.md

@@ -1,188 +1,18 @@
-# LIP (LLVM IR to Predicate)
+<img src="docs/logo.png" alt="drawing"/>
 
-## Project Structure
+## Overview
+Wyvern Graph (or **Wy-Graph**) is a python tool for translating LLVM IR into a knowledge graph. Wy-Graph takes an [LLVM IR](https://llvm.org/docs/LangRef.html) file as input and performs standard static analyses (Syntactic, Control-Flow, Data-Flow, and Memory). It encodes these analyses results in a list of unary and binary formal predicates with the intention of building data sets that convey knowledge graph equivalents of LLVM IR programs. The goal is for these data sets to be utilized to apply [Neuro-symbolic AI](https://en.wikipedia.org/wiki/Neuro-symbolic_AI) (Specifically differentiable Inductive Logic Programming AI) to program analysis.
 
-The project will follow a structure derived from compiler design. 
-We aim to take LLVM IR input, and lex, parse, analyze, and generate resulting facts that capture the structure of the program and potentially important characteristics for understanding the structure of the program as well as potential vulnerability detection.
+## Table of Contents
+1. [Getting Started](docs/getting_started.md)
+2. [Features](docs/features.md)
+3. [Demo](docs/demo.md)
+4. [Future Development](docs/future_dev.md)
 
-### Dependencies
+## Acknowledgments
 
-1. **LLVMLite**: A lightweight LLVM-Python binding for writing JIT compilers. This package will allow us to lex and parse LLVM IR code into a tree structure. This tree structure, however, is a little too *lightweight* for our desires. It carries too much information on nodes and becomes too unfocused in an attempt to be extremely generalized. We will parse this structure into a more *fit* abstract syntax tree (AST) that we can make better use of.
+This project was developed by [Christian Scaff](https://github.com/cscaff) at the Georgia Tech Research Institute's Advanced Research in Computing and Artificial Intelligence Division [(**ARCAID**)](https://www.gtri.gatech.edu/focus-areas/advanced-research-computing-and-artificial-intelligence) under the guidance of [Clayton Kerce](https://github.com/ckerce) in the summer of 2025.
 
-2. **NetworkX**: A python package for creation, manipulation, and study of networks. We will use this to model the control flow of our program through a directed graph.
-
-
-### Implementation 
-
-The project will be implemented as such:
-
-1. LLVM IR --> Lexed/Parsed by LLVMLite --> Module Tree
-2. Module Tree --> Parser --> AST
-3. AST --> Analyzer --> Decorated AST
-4. Decorated AST --> Generator --> Predicate Logic
-
-### Predicate Logic Result
-
-The goal of our predicate language is to formally express key characteristics of a program through solely unary and binary predicates. Effectively, we break down a program into properties and their relationships.
-
-### Control Flow
-
-1. *control_flow(X)* | {**X** = instruction}.
-2. *entry(X)* | {**X** = entry block}.
-3. *exit(X)* | {**X** = exit block}.
-4. *has_successor(X, Y)* | {block **X** has a directed edge to block **Y**}.
-5. *has_predecessor(X, Y)* | {block **Y** has a directed edge to block **X**}.
-6. *dominates(X, Y)* | {block **X** dominates block **Y**}.
-7. *post_dominates(X, Y)* | {block **X** post dominates block **Y**}.
-8. *loop(X)* | {**X** is a loop}.
-9. *loop_head(X, Y)* | {loop **X** has loop header block **Y**}.
-10. *in_loop(X, Y)* | {block **X** resides in loop **Y**}.
-11. *down_flow(X, Y)* | {block **X** flows down to block **Y**}.
-12. *up_flow(X, Y)* | {block **X** flows back up to block **Y**}.
-13. *originates_from(X, Y)* | {block **X** is called in block **Y**}.
-14. *control_dependent(X, Y)* | {inst. **X** depends on the result of inst. **Y**}.
-15. *exception_flow(X, Y)* | {try block **X** may throw an exception to catch block **Y**}.
-
-### Data Flow
-
-#### Reaching Definition Analysis
-
-1. *reaches(X, Y)* | {definition **X** reaches block **Y**}.
-2. *defines(X, Y)* | {inst. **X** defines value **Y**}.
-3. *uses(X, Y)* | {inst. **X** uses value **Y**}.
-4. *kills(X, Y)* | {inst. **X** kills value **Y**}.
-5. *data_dependent(X, Y)* | {inst. **X** depends on data from inst. **Y**}.
-
-#### Live Variable Analysis
-
-1. *live_in(X, Y)* | {variable **X** is live entering block **Y**}.
-2. *live_out(X, Y)* | {variable **X** is live leaving block **Y**}. 
-
-#### Definite Assignment Analysis
-
-1. *definitely_assigned(X)* | {variable **X** is definitely assigned}.
-2. *definitely_unassigned(X)* | {variable **X** is definitely unassigned}.
-3. *unknown_assignment(X)* | {variable **X** assignment status is unknown}.
-
-### Memory
-
-1. *allocates(X, Y)* | {inst. **X** allocates type width **Y**}.
-2. *loads(X, Y)* | {inst. **X** loads value **Y** into virtual register}.
-3. *stores_value(X, Y)* | {inst. **X** stores value **Y**}.
-4. *stores_at(X, Y)* | {inst. **X** stores value at memory location **Y**}.
-5. *local_variable(X)* | {**X** = local variable}
-6. *has_atomic_ordering(X, Y)* | {inst. **X** has ordering **Y**}.
-
-
-#### Pointers
-
-##### Andersen Style
-
-1. *points_to(X, Y)* | {pointer **X** may point to value **Y**}. (Core Rule)
-   - *assigns(X,Y)* | {pointer **X** is assigned to value of pointer **Y**}.
-   - *address_of(X, Y)* | {object **Y** is stored at address **X**}.
-
-##### Alias Style
-
-1. *may_alias(X, Y)* | {pointer **X** might alias pointer **Y**}.
-2. *must_alias(X, Y)* | {pointer **X** must alias pointer **Y**}.
-
-### Syntactic
-
-#### Module
-
-1. *module(X)* | {**X** = module}.
-2. *data_layout(X)* | {**X** = data layout for given module}.
-3. *target_triple(X)* | {**X** = target triple for given module}.
-
-#### Global Variables
-
-1. *global_variable(X)* | {**X** = global variable}.
-2. *constant(X)* | {**X** = constant variable}.
-3. *has_initializer(X, Y)* | {variable **X** has initial value **Y**}.
-   - Denotes initializer or declaration.
-4. *has_linkage(X, Y)* | {variable **X** has linkage **Y**}.
-5. *has_storage_class(X, Y)* | {variable **X** has storage class **Y**}.
-   - Y = default, dll_import, dll_export, weak, private...
-6. *has_type(X, Y)* | {variable **X** has type **Y**}. 
-7. *has_visibility(X, Y)* | {variable **X** has visibility **Y**}.
-   - Y = default, hidden, protected...
-8. *has_attribute(X, Y)* | {variable **X** has attribute **Y**}.
-
-#### Functions
-
-1. *function(X)* | {**X** = function}.
-2. *has_argument(X, Y)* | {function **X** has argument **Y**}.
-   - *has_attribute(X, Y)* | {argument **X** has attribute **Y**}.
-   - *has_type(X, Y)* | {argument **X** has type **Y**}.
-   - *constant(X)* | {**X** = constant argument}.
-   - *has_linkage(X, Y)* | {argument **X** has linkage **Y**}.
-3. *has_attribute(X, Y)* | {function **X** has attribute **Y**}.
-4. *has_type(X, Y)* | {function **X** has type **Y**}.
-5. *constant(X)* | {**X** = constant function}.
-6. *declaration(X)* | {**X** = function declaration}.
-7. *has_linkage(X, Y)* | {function **X** has linkage **Y**}.
-8. *has_visibility(X, Y)* | {function **X** has visibility **Y**}.
-
-#### Blocks
-
-1. *block(X)* | {**X** = basic block}.
-2. *has_linkage(X, Y)* | {block **X** has linkage **Y**}.
-
-#### Instructions
-
-1. *instruction(X)* | {**X** = instruction}.
-2. *instruction_opcode(X, Y)* | {inst. **X** has opcode **Y**}.
-3. *instruction_operand(X, Y)* | {inst. **X** has operand **Y**}.
-4. *has_type(X, Y)* | {inst. **X** is of type **Y**}
-5. *has_attribute(X, Y)* | {inst. **X** has attribute **Y**}.
-6. *has_linkage(X, Y)* | {inst. **X** has linkage **Y**}.
-7. *const(X)* | {**X** = constant instruction}.
-
-##### Specifics
-
-1. *binary_operation(X)* | {**X** = instruction}.
-2. *unary_operation(X)* | {**X** = instruction}.
-3. *terminator(X)* | {**X** = instruction}.
-4. *select_instruction(X)* | {**X** = instruction}.
-    - *select_operand(X, Y)* | {inst. **X** has operand **Y**}.
-5. *invoke_instruction(X)* | {**X** = instruction}.
-   - *invokes(X, Y)* | {function **X** invokes function **Y**}.
-   - *invoke_normal(X, Y)* | {inst. **X** has normal location **Y**}.
-   - *invoke_unwind(X, Y)* | {inst. **X** has unwind location **Y**}.
-   - *landing_pad(X)* | {**X** = instruction}.
-     - *catches(X, Y)* | {landing pad **X** catches exception type **Y**}.
-     - *Filters(X, Y)* | {landing pad **X** filters exception type **Y**}.
-6. *call_instruction(X)* | {**X** = instruction}.
-    - *calls(X, Y)* | {function **X** calls function **Y**}.
-7. *aggregate_operation(X)* | {**X** = instruction}.
-   - *extract_val_instruction(X)* | {**X** = instruction}.
-     - *extract_val_agg(X, Y)* | {inst. **X** extracts agg **Y**}. 
-     - *extract_val_index(X, Y)* | {inst. **X** extracts from index **Y**}. 
-   - *insert_val_instruction(X)* | {**X** = instruction}.
-     - *insert_val_agg(X, Y)* | {inst. **X** inserts to agg **Y**}.
-     - *insert_val_index(X, Y)* | {inst. **X** inserts val **Y**}.
-8. *vector_operation(X)* | {**X** = instruction}.
-   - *extract_val_instruction(X)* | {**X** = instruction}.
-     - *extract_element(X, Y)* | {inst. **X** extracts element **Y**}.
-     - *extract_val_index(X, Y)* | {inst. **X** extracts from index **Y**}.
-   - *insert_val_instruction(X)* | {**X** = instruction}.
-     - *insert_element(X, Y)* | {inst. **X** inserts element **Y**}.
-     - *insert_val_index(X, Y)* | {inst. **X** inserts val **Y**}.
-9.  *memory_access(X)* | {**X** = instruction}.
-   - get_element_ptr_operation(X)* | {**X** = instruction}.
-     - *get_element_ptr_base(X, Y)* | {inst. **X** has base index **Y**}.
-     - *get_element_ptr_index(X, Y)* | {inst. **X** has index **Y**}.
-     - *get_element_ptr_val(X, Y)* | {inst. **X** points to value **Y**}.
-10. *conversion_operation(X)* | {**X** = instruction}.
-11. *phi_node(X)* | {**X** = instruction}.
-    - *phi_operand(X, Y)* | {inst. **X** has operand **Y**}.
-    - *phi_incoming(X, Y)* | {inst. **X** has incoming block **Y**}. *Might need to change*!
-12. *returns(X, Y)* | {inst. **X** returns value **Y**}.
-13. *throws(X, Y)* | {inst. **X** throws exception **Y**}.
-14. *has_metadata(X, Y)* | {object **X** has metadata **Y**}.
-15. *metadata_value(X, Y)* | {metadata **X** has value **Y**}.
-16. *constant_expression(X)* | {**X** = instruction}.
-17. *constant_expression_opcode(X, Y)* | {inst. **X** has opcode **Y**}.
-    - Denotes operation that only uses constants.
-    - Maybe useful for constant propagation?
+The project was made possible with:
+- The LLVM Project ([https://llvm.org](https://llvm.org))
+- LLVMLite Library ([https://github.com/numba/llvmlite](https://github.com/numba/llvmlite))

docs/demo.md

@@ -0,0 +1,63 @@
+# Demo
+Let's try it out and see what this program is capable of!
+
+You can find a collection of examples in `test/examples/input`. Most of these examples derive from [SV-Benchmarks](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks) which provides a solid collection of verification tasks.
+
+While, ironically, the dynamic nature of threads may not be the most suitable demo, we will look at an example of a data race within a C file as it illustrates a real application on a small file.
+
+Let's dive into [pthread-demo-datarace-2.ll](/test/examples/input/pthread-demo-datarace-2.ll)!
+
+## Running the Program
+Let's run the command with our input file!
+![demo](./demo/demo.gif)
+
+## Looking at our Predicates
+We can view the predicate results [here](./demo/predicates.txt)!
+
+An excerpt:
+```
+entry(reach_error_block_0)
+exit(reach_error_virtual_exit)
+has_successor(reach_error_block_0, reach_error_virtual_exit)
+has_predecessor(reach_error_virtual_exit, reach_error_block_0)
+dominates(reach_error_block_0, reach_error_virtual_exit)
+post_dominates(reach_error_virtual_exit, reach_error_block_0)
+```
+This illustrates some of our control flow for a specific function, `reach_error`, which has only one block. We can view that IR here:
+```
+define void @reach_error() #0 {
+  call void @__assert_rtn(i8* noundef getelementptr inbounds ([12 x i8], [12 x i8]* @__func__.reach_error, i64 0, i64 0), i8* noundef getelementptr inbounds ([26 x i8], [26 x i8]* @.str, i64 0, i64 0), i32 noundef 25, i8* noundef getelementptr inbounds ([2 x i8], [2 x i8]* @.str.1, i64 0, i64 0)) #4
+  unreachable
+}
+```
+We notice that we make a function call here to `@__assert_rtn`. However, this is an external call so we do not pick up on any control flow information regarding that.
+
+## Looking at our Graph
+
+### Uploading
+We can upload our graph to [Gephi Lite](https://gephi.org/gephi-lite/) as shown:
+![demo](./demo/uploading_graph.gif)
+
+### Displaying
+That's a little messy though, no? We can clean it up by clicking on the layout tab on the left menu bar and applying a display algorithm.
+ ![demo](./demo/displayalgo.jpeg)
+*Pretty!*
+
+### Filtering
+What if we want to explore specific graph properties or relationships?
+
+We can accomplish this by going to the Filters tab.
+
+#### Filtering By Analysis Category
+We can select category to filter by analysis types.
+ ![demo](./demo/filtering_category.gif)
+
+### Filtering By Binary Predicates
+We can select predicates to filter specific edge types.
+ ![demo](./demo/filter_preds.png)
+
+### Filtering By Unary Predicates
+We can select node types to filter specific node properties. Do note, the current filtering system needs a little work.
+ ![demo](./demo/filter_nodes.png)
+
+For more sophisticated graph exploration, you can use the full [Gephi](https://gephi.org) software.