Update README and Config.py for dune-built CodeHawk

Author: brk

README.md

@@ -4,33 +4,22 @@ Sound Static Analysis of C for Memory Safety (Undefined Behavior)
 ### Quick start
 
 The CodeHawk-C Analyzer consists of two parts:
-- A python front end (this repository) through which all user interaction
+- A Python front end (this repository) through which all user interaction
   is performed, and
-- An ocaml abstract-interpretation engine that powers the analysis.
+- An OCaml abstract-interpretation engine that powers the analysis.
 
-To use the CodeHawk-C Analyzer first clone or download the ocaml application
+To use the CodeHawk-C Analyzer first clone or download the OCaml application
 from
 ```
 https://github.com/static-analysis-engineering/codehawk
 ```
-and build according to the accompanying instructions given there.
-Then copy the following files from that build:
-```
-codehawk/CodeHawk/CHC/cchcil/parseFile
-codehawk/CodeHawk/CHC/cchcmdline/canalyzer
-```
-to the following location in this repository:
-```
-CodeHawk-C/chc/bin/linux/
-```
-or
-```
-CodeHawk-C/chc/bin/macOS
-```
-depending on the platform where the executables were built.
-Alternatively, you can edit the path to these two executables directly
-in chc/util/Config.py or chc/util/ConfigLocal.py, so there is no need
-to copy them or update them with each new version of the ocaml analyzer.
+and build according to the accompanying instructions given there (using `dune`).
+
+If this repository is placed within, or next to, that directory,
+you should be ready to proceed. Otherwise, copy
+`chc/util/ConfigLocal.template` to `chc/util/ConfigLocal.py` in this
+repository, and edit the latter file to set `config.codehawkdir` to
+the location of the `codehawk` checkout.
 
 Set the python path and path:
 ```
@@ -47,8 +36,8 @@ which should show something like:
 Analyzer configuration:
 -----------------------
   platform : linux
-  parser   : /home/user/codehawk/CodeHawk/CHC/cchcil/parseFile (found)
-  analyzer : /home/user/codehawk/CodeHawk/CHC/cchcmdline/canalyzer (found)
+  parser   : /home/user/codehawk/CodeHawk/_build/default/CHC/cchcil/cCHXParseFile.exe (found)
+  analyzer : /home/user/codehawk/CodeHawk/_build/default/CHC/cchcmdline/cCHXCAnalyzer.exe (found)
 
   summaries: /home/user/CodeHawk-C/chc/summaries/cchsummaries.jar (found)
 ```

chc/bin/linux/README.md

@@ -42,6 +42,12 @@
 
 class Config(object):
     def __init__(self) -> None:
+        self.codehawkdir: Optional[str] = None
+
+        # initial personalization, in particular for self.codehawkdir
+        if localconfig:
+            ConfigLocal.getLocals(self)
+
         # platform settings
         if os.uname()[0] == "Linux":
             self.platform = "linux"
@@ -51,20 +57,33 @@ def __init__(self) -> None:
         # general settings
         self.utildir = os.path.dirname(os.path.abspath(__file__))
         self.rootdir = os.path.dirname(self.utildir)
-        self.bindir = os.path.join(self.rootdir, "bin")
         self.topdir = os.path.dirname(self.rootdir)
         self.testdir = os.path.join(self.topdir, "tests")
 
-        # parser and analyzer executables
-        if self.platform == "linux":
-            self.linuxdir = os.path.join(self.bindir, "linux")
-            self.cparser = os.path.join(self.linuxdir, "parseFile")
-            self.canalyzer = os.path.join(self.linuxdir, "canalyzer")
-
-        if self.platform == "macOS":
-            self.macOSdir = os.path.join(self.bindir, "macOS")
-            self.cparser = os.path.join(self.macOSdir, "parseFile")
-            self.canalyzer = os.path.join(self.macOSdir, "canalyzer")
+        if self.codehawkdir is None:
+            # CodeHawk directory -- assumption is it will be either the
+            # parent directory of the rootdir, or a sibling in the parent.
+            def looks_like_codehawk(path: str) -> bool:
+                chb = os.path.join(path, "CodeHawk", "CHB")
+                chc = os.path.join(path, "CodeHawk", "CHC")
+                return os.path.isdir(chb) and os.path.isdir(chc)
+            topparent = os.path.dirname(self.topdir)
+            alts = [topparent,
+                    os.path.join(topparent, "codehawk"),
+                    os.path.join(topparent, "CodeHawk")]
+            viable_alts = [alt for alt in alts if looks_like_codehawk(alt)]
+            self.codehawkdir = (viable_alts + [None])[0]
+
+        ## parser and analyzer executables
+        if self.codehawkdir is not None:
+            # Look for non-installed binaries by default
+            self.cparser = os.path.join(self.codehawkdir, "CodeHawk",
+                "_build", "default", "CHC", "cchcil", "cCHXParseFile.exe")
+            self.canalyzer = os.path.join(self.codehawkdir, "CodeHawk",
+                "_build", "default", "CHC", "cchcmdline", "cCHXCAnalyzer.exe")
+        else:
+            self.cparser = "<no codehawkdir!>"
+            self.canalyzer = "<no codehawkdir!>"
 
         self.chc_gui: Optional[str] = None
 
@@ -80,7 +99,7 @@ def __init__(self) -> None:
         self.name_separator = ":"
         self.targets: Dict[str, str] = {}
 
-        # personalization
+        # personalization: ConfigLocal takes precedence over options above
         if localconfig:
             ConfigLocal.getLocals(self)
 

chc/bin/macOS/README.md

@@ -43,9 +43,6 @@ def getLocals(config: chc.util.Config.Config) -> None:
     '''Set local configuration variables here if they differ from the defaults in Config.py
 
     Example :
-    config.canalyzer = '/home/username/my-analyzer/canalyzer'
-    config.cparser = '/home/username/my-parser/parseFile'
+    config.codehawkdir = '/home/username/codehawk/'
     config.summaries = '/home/username/my-summaries/cchsummaries.jar'
-    config.bear = '/home/username/bear-home/bear'
-    config.libear = '/home/username/bear-home/libear.so'
     '''