Automatic Update

.gitignore

@@ -2,7 +2,6 @@ __pycache__
 *.pyc
 intrepid_build
 intrepid_build_debug
-.vscode
 build
 dist
 intrepyd.egg-info
@@ -13,3 +12,7 @@ venv
 htmlcov
 .coverage
 .DS_Store
+intrepyd/formula2py/FormulaLexer.tokens
+intrepyd/formula2py/FormulaLexer.interp
+intrepyd/formula2py/Formula.tokens
+intrepyd/formula2py/Formula.interp

README.md

@@ -11,8 +11,6 @@ via a rich REST API.
 1. [Installation](#installation)
     1. [Officially Supported OSes](#officially-supported-oses)
     1. [Prerequisites](#prerequisites)
-    1. [Install via pip](#install-via-pip)
-    1. [Install via setup.py](#install-via-setup.py)
 1. [Quick Start](#quick-start)
     1. [Constructing Models](#constructing-models)
     1. [Simulating Models](#simulating-models)
@@ -37,20 +35,22 @@ pip3 install intrepyd
 ```
 issued from a terminal.
 
+If you wish to use intrepyd in an isolated environment you may use docker as
+follows
+```
+docker run -it python:3.8 /bin/bash
+pip3 install intrepyd
+```
+
 ## Officially Supported OSes
-- Windows 10 or above
-- Ubuntu 19.04 or above
+- Windows 10
+- Linux
+- OSX
 
 ## Prerequisites
 - python 3.8 (exactly this version)
 - (Windows only) [Visual C++ Redistributable for Visual Studio][1]
 
-## Install via pip
-TODO
-
-## Install via setup
-TODO
-
 # Quick start
 
 ## Constructing Models

VERSION

@@ -1 +1 @@
-0.10.3
+0.11.0

app/contexts.py

@@ -1,3 +1,6 @@
+"""
+Implementation of REST API for context creation
+"""
 from flask import Blueprint, request
 from intrepyd import Context
 
@@ -7,10 +10,16 @@
 
 @cr.route('', methods=['GET'])
 def list_contexts():
+    """
+    Gets the list of available contexts
+    """
     return {'contexts': [name for name in contexts]}, 200
 
 @cr.route('/create', methods=['POST'])
 def create_context():
+    """
+    Creates a context
+    """
     name = request.get_json()['name']
     if name is None:
         return {'result': 'error'}, 400

app/debug.py

@@ -1,10 +1,16 @@
+"""
+Implementation of REST API for debugging
+"""
 from flask import Blueprint, request
 from intrepyd.api import apitrace_dump_to_file
 
 dr = Blueprint('debug', __name__)
 
 @dr.route('/apitracedump', methods=['POST'])
 def apitracedump():
+    """
+    Obtain a dump of the C++ API called so far
+    """
     filepath = request.get_json()['filepath']
     if filepath is None:
         return {'result': 'error'}, 400

app/engines.py

@@ -1,19 +1,27 @@
-from flask import Blueprint, request, jsonify
-from intrepyd.engine import Bmc, OptimizingBmc, BackwardReach
+"""
+Implementation of REST API for engines
+"""
+from flask import Blueprint, request
+from intrepyd.engine import Bmc, OptimizingBmc
 from intrepyd.engine import EngineResult
+from .contexts import contexts
 
 er = Blueprint('engines', __name__)
 
-from .contexts import contexts
-
 @er.route('', methods=['GET'])
 def list_engines():
+    """
+    List all the previously created engines
+    """
     context = request.args.get('context')
     engines = contexts[context]['engines']
     return {'engines': [name for name in engines]}, 200
 
 @er.route('/assumptions/create', methods=['POST'])
 def create_assumption():
+    """
+    Creates an assumption
+    """
     context = request.get_json()['context']
     net = request.get_json()['net']
     if context is None or net is None:
@@ -24,12 +32,15 @@ def create_assumption():
 
 @er.route('/create', methods=['POST'])
 def create_engine():
+    """
+    Creates an engine
+    """
     context = request.get_json()['context']
     engine = request.get_json()['engine']
     if context is None or engine is None:
         return {'result': 'error'}, 400
     ctx = contexts[context]['context']
-    assert(ctx is not None)
+    assert ctx is not None
     eng = None
     if engine == 'bmc':
         eng = ctx.mk_bmc()
@@ -39,59 +50,71 @@ def create_engine():
         eng = ctx.mk_backward_reach()
     else:
         return {'result': 'error: unknown engine {}'.format(engine)}, 400
-    assert(eng is not None)
+    assert eng is not None
     name = 'e{}'.format(len(contexts[context]['engines']))
     contexts[context]['engines'][name] = eng
     return {'result': name}, 201
 
 @er.route('/setcurrentdepth', methods=['PUT'])
 def set_current_depth():
+    """
+    Sets the current depth for a BMC engine
+    """
     context = request.get_json()['context']
     engine = request.get_json()['engine']
     depth = request.get_json()['depth']
     if context is None or engine is None or depth is None:
         return {'result': 'error'}, 400
     ctx = contexts[context]['context']
     eng = contexts[context]['engines'][engine]
-    assert(ctx is not None)
-    assert(eng is not None)
+    assert ctx is not None
+    assert eng is not None
     if not isinstance(eng, Bmc) and not isinstance(eng, OptimizingBmc):
         return {'result': 'error: cannot set depth on this engine'}, 400
     eng.set_current_depth(depth)
     return {'result': depth}, 200
 
 @er.route('/setuseinduction', methods=['PUT'])
 def set_use_induction():
+    """
+    Enable induction on a BMC engine
+    """
     context = request.get_json()['context']
     engine = request.get_json()['engine']
     if context is None or engine is None:
         return {'result': 'error'}, 400
     ctx = contexts[context]['context']
     eng = contexts[context]['engines'][engine]
-    assert(ctx is not None)
-    assert(eng is not None)
+    assert ctx is not None
+    assert eng is not None
     if not isinstance(eng, Bmc) and not isinstance(eng, OptimizingBmc):
         return {'result': 'error: cannot set induction on this engine'}, 400
     eng.set_use_induction()
     return {'result': 'ok'}, 200
 
 @er.route('/setallowtargetsatanydepth', methods=['PUT'])
 def set_allow_targets_at_any_depth():
+    """
+    Allow BMC to reach targets at any depth, not just the last one
+    """
     context = request.get_json()['context']
     engine = request.get_json()['engine']
     if context is None or engine is None:
         return {'result': 'error'}, 400
     ctx = contexts[context]['context']
     eng = contexts[context]['engines'][engine]
-    assert(ctx is not None)
-    assert(eng is not None)
+    assert ctx is not None
+    assert eng is not None
     if not isinstance(eng, Bmc) and not isinstance(eng, OptimizingBmc):
         return {'result': 'error: cannot set induction on this engine'}, 400
     eng.set_allow_targets_at_any_depth()
     return {'result': 'ok'}, 200
 
 @er.route('/setuseattackpathaxioms', methods=['PUT'])
 def set_use_attack_path_axioms():
+    """
+    Inserts specifically effective axioms for computing an Attack Path
+    """
     context = request.get_json()['context']
     engine = request.get_json()['engine']
     source = request.get_json()['source']
@@ -102,17 +125,20 @@ def set_use_attack_path_axioms():
     eng = contexts[context]['engines'][engine]
     sou = ctx.nets[source]
     tar = ctx.nets[target]
-    assert(ctx is not None)
-    assert(eng is not None)
-    assert(sou is not None)
-    assert(tar is not None)
+    assert ctx is not None
+    assert eng is not None
+    assert sou is not None
+    assert tar is not None
     if not isinstance(eng, Bmc) and not isinstance(eng, OptimizingBmc):
         return {'result': 'error: cannot set attack path axioms on this engine'}, 400
     eng.set_use_attack_path_axioms(sou, tar)
     return {'result': 'ok'}, 200
 
 @er.route('/addtarget', methods=['PUT'])
 def add_target():
+    """
+    Adds a target to the engine
+    """
     context = request.get_json()['context']
     engine = request.get_json()['engine']
     net = request.get_json()['net']
@@ -121,20 +147,23 @@ def add_target():
     ctx = contexts[context]['context']
     eng = contexts[context]['engines'][engine]
     net = ctx.nets[net]
-    assert(ctx is not None)
-    assert(eng is not None)
-    assert(net is not None)
+    assert ctx is not None
+    assert eng is not None
+    assert net is not None
     eng.add_target(net)
     return {'result': 'ok'}, 200
 
 @er.route('/reachtargets', methods=['PUT'])
 def reach_targets():
+    """
+    Executes reachability for the specified targets
+    """
     context = request.get_json()['context']
     engine = request.get_json()['engine']
     if context is None or engine is None:
         return {'result': 'error'}, 400
     eng = contexts[context]['engines'][engine]
-    assert(eng is not None)
+    assert eng is not None
     result = eng.reach_targets()
     res = 'unknown'
     if result == EngineResult.REACHABLE:
@@ -145,6 +174,9 @@ def reach_targets():
 
 @er.route('/watch', methods=['PUT'])
 def add_watch():
+    """
+    Adds a net to the set of watches
+    """
     context = request.get_json()['context']
     engine = request.get_json()['engine']
     net = request.get_json()['net']
@@ -153,35 +185,41 @@ def add_watch():
     ctx = contexts[context]['context']
     eng = contexts[context]['engines'][engine]
     net = ctx.nets[net]
-    assert(ctx is not None)
-    assert(eng is not None)
-    assert(net is not None)
+    assert ctx is not None
+    assert eng is not None
+    assert net is not None
     eng.add_watch(net)
     return {'result': 'ok'}, 200
 
 @er.route('/lastreachedtargets', methods=['GET'])
 def last_reached_targets():
+    """
+    Gets the list of reached targets
+    """
     context = request.args.get('context')
     engine = request.args.get('engine')
     if context is None or engine is None:
         return {'result': 'error'}, 400
     ctx = contexts[context]['context']
     eng = contexts[context]['engines'][engine]
-    assert(ctx is not None)
-    assert(eng is not None)
+    assert ctx is not None
+    assert eng is not None
     result = [ctx.net2name[net] for net in eng.get_last_reached_targets()]
     return {'result': result}, 200
 
 @er.route('/lasttrace', methods=['GET'])
 def last_trace():
+    """
+    Gets the trace for the last reached target
+    """
     context = request.args.get('context')
     engine = request.args.get('engine')
     if context is None or engine is None:
         return {'result': 'error'}, 400
     ctx = contexts[context]['context']
     eng = contexts[context]['engines'][engine]
-    assert(ctx is not None)
-    assert(eng is not None)
+    assert ctx is not None
+    assert eng is not None
     name = 't{}'.format(len(contexts[context]['traces']))
     trace = eng.get_last_trace()
     contexts[context]['traces'][name] = trace

app/inputs.py

@@ -1,16 +1,17 @@
 """
-APIs for inputs
+Implementation of REST API for inputs
 """
-
 from flask import Blueprint, request
-
-ir = Blueprint('inputs', __name__)
-
 from .utils import typename_to_type
 from .contexts import contexts
 
+ir = Blueprint('inputs', __name__)
+
 @ir.route('', methods=['GET'])
 def list_inputs():
+    """
+    Gets the list of inputs
+    """
     context = request.args.get('context')
     if context is None:
         return {'result': 'error'}, 400
@@ -19,12 +20,15 @@ def list_inputs():
 
 @ir.route('/create', methods=['POST'])
 def create_input():
+    """
+    Creates a new input
+    """
     context = request.get_json()['context']
     typ = request.get_json()['type']
     if context is None or typ is None:
         return {'result': 'error'}, 400
     ctx = contexts[context]['context']
-    assert(ctx is not None)
+    assert ctx is not None
     name = '__i{}'.format(len(ctx.inputs.items()))
     ctx.mk_input(name, typename_to_type(ctx, typ))
     return {'result': name}, 201