Merge branch 'ilair' into coverity_check

.gitmodules

@@ -1,6 +1,4 @@
 [submodule "examples/RISC-V/simulator"]
 	path = examples/RISC-V/simulator
 	url = https://github.com/zhanghongce/riscv-ila-sim.git
-[submodule "glog"]
-	path = glog
-	url = https://github.com/google/glog.git
+

.travis.yml

@@ -2,6 +2,9 @@ language: cpp
 os: linux
 sudo: required
 dist: trusty
+compiler:
+  - g++
+  #- clang++
 
 branches:
   only:

CMakeLists.txt

@@ -27,20 +27,6 @@ set(CMAKE_MODULE_PATH
 
 set(CMAKE_MACOSX_RPATH 1)
 
-# ------------------------------------------------------------------------------
-# Google Log
-# ------------------------------------------------------------------------------
-if (build_glog)
-  execute_process(COMMAND git submodule init ${PROJECT_SOURCE_DIR}/glog)
-  execute_process(COMMAND git submodule update ${PROJECT_SOURCE_DIR}/glog)
-  add_subdirectory(glog)
-else ()
-  find_package(glog 0.3.5 REQUIRED)
-  if (NOT TARGET glog::glog)
-    MESSAGE (FATAL_ERROR 
-      "Unable to find glog. Set build_glog for in-source build.")
-  endif (NOT TARGET glog::glog)
-endif ()
 
 # ------------------------------------------------------------------------------
 # Compile flags 
@@ -59,7 +45,7 @@ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall")
 # Set debug/coverage flags, or optimize, depending on options.
 if (debug)
     set(CMAKE_BUILD_TYPE "Debug")
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -g")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -g3")
     # Coverage can only be set if -g is used.
     if (coverage)
         set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fprofile-arcs -ftest-coverage")
@@ -96,6 +82,11 @@ configure_file(
   "${PROJECT_BINARY_DIR}/config.h")
 include_directories("${PROJECT_BINARY_DIR}")
 
+# ------------------------------------------------------------------------------
+# Google Log
+# ------------------------------------------------------------------------------
+find_package(glog 0.3.5 REQUIRED)
+
 # ------------------------------------------------------------------------------
 # Z3
 # ------------------------------------------------------------------------------
@@ -181,3 +172,16 @@ add_subdirectory (src)
 # ------------------------------------------------------------------------------
 add_subdirectory (test)
 
+# Install target
+install(FILES include/ila++.h DESTINATION include)
+
+# uninstall target
+if(NOT TARGET uninstall)
+  configure_file(
+    "${CMAKE_CURRENT_SOURCE_DIR}/cmake_uninstall.cmake.in"
+    "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
+    IMMEDIATE @ONLY)
+  add_custom_target(uninstall
+    COMMAND ${CMAKE_COMMAND} -P ${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake)
+endif()
+

README.md

@@ -15,7 +15,7 @@ For API documents and tutorials, see the [docs](https://github.com/Bo-Yuan-Huang
 
 For some examples, see the [examples](https://github.com/Bo-Yuan-Huang/ILA-Tools/tree/master/examples) directory.
 
-## ILA description and C/C++/Python API (under construction)
+## ILA description and C++ API 
 
 [![Build Status](https://travis-ci.org/Bo-Yuan-Huang/ILA-Tools.svg?branch=master)](https://travis-ci.org/Bo-Yuan-Huang/ILA-Tools)
 [![Coverage Status](https://coveralls.io/repos/github/Bo-Yuan-Huang/ILA-Tools/badge.svg?branch=master)](https://coveralls.io/github/Bo-Yuan-Huang/ILA-Tools?branch=master)
@@ -27,28 +27,34 @@ For some examples, see the [examples](https://github.com/Bo-Yuan-Huang/ILA-Tools
 ```bash
   mkdir -p build
   cd build
-  cmake .. -L -DZ3_INCLUDE_DIR=/usr/include 
+  cmake .. -L -DZ3_INCLUDE_DIR=<path/to/z3/header>
 ```
 
+For tutorial, see [c++ api example](https://github.com/Bo-Yuan-Huang/ILA-Tools/tree/master/examples/c++).
+
 For API documentation, see the page [ILA-Tools-API](https://rawgit.com/Bo-Yuan-Huang/ILA-Tools/master/docs/api-html/namespaceila.html).
 
 For developers, implementation details can be found on [ILA-Tools-Impl](https://rawgit.com/Bo-Yuan-Huang/ILA-Tools/master/docs/impl-html/namespaceila.html).
 
 
 ### Publications:
 
+* __Formal Security Verification of Concurrent Firmware in SoCs using Instruction-Level Abstraction for Hardware__.
+  Bo-Yuan Huang, Sayak Ray, Aarti Gupta, Jason Fung, and Sharad Malik.
+  *in* Proceedings of the Design Automation Conference. (DAC 2018), San Francisco, CA. June 2018.
+
 * __Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification__.
   Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, and Sharad Malik.
   [[arXiv:1801.01114](https://arxiv.org/abs/1801.01114)]
   [[PDF](https://arxiv.org/pdf/1801.01114.pdf)]
 
 * __Template-based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification__.
   Pramod Subramanyan, Bo-Yuan Huang, Yakir Vizel, Aarti Gupta, and Sharad Malik.
-  *in* IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2017.
+  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), 2017.
   [[PDF](https://github.com/Bo-Yuan-Huang/ILA-Tools/blob/master/docs/publications/Template-based%20Parameterized%20Synthesis%20of%20Uniform%20Instruction-Level%20Abstractions%20for%20SoC%20Verification.pdf)]
 
 * __Invited: Specification and Modeling for Systems-on-Chip Security Verification__. 
-  Sharad Malik and Pramod Subramanyan. 
+  Sharad Malik and Pramod Subramanyan.
   *in* Proceedings of the Design Automation Conference. (DAC 2016), Austin, TX. June 2016. 
   [[PDF](https://github.com/Bo-Yuan-Huang/ILA-Tools/blob/master/docs/publications/Invited_Specification_and_Modeling_for_Systems_on_Chip_Security_Verification.pdf)] 
 
@@ -58,6 +64,6 @@ For developers, implementation details can be found on [ILA-Tools-Impl](https://
   [[PDF](https://github.com/Bo-Yuan-Huang/ILA-Tools/blob/master/docs/publications/Verifying_Information_Flow_Properties_of_Firmware_using_Symbolic_Execution.pdf)]
 
 * __Template-based Synthesis of Instruction-Level Abstractions for SoC Verification__. 
-  Pramod Subramanyan, Yakir Vizel, Sayak Ray and Sharad Malik. 
+  Pramod Subramanyan, Yakir Vizel, Sayak Ray and Sharad Malik.
   *in* Proceedings of Formal Methods in Computer-Aided Design. (FMCAD 2015). Austin, TX, September 2015.
   [[PDF](https://github.com/Bo-Yuan-Huang/ILA-Tools/blob/master/docs/publications/Template_based_Instruction_Level_Abstraction_for_SoC_Verification.pdf)]

apps/empty_proj/Makefile

@@ -1,12 +1,6 @@
 
-export ROOT_PATH  = $(shell pwd)
-export ILA_LIB    = $(ROOT_PATH)/../../build/lib
-export ILA_HEADER = $(ROOT_PATH)/../../include
-
-CXX=g++
 CXX_FLAGS=-std=c++11 -Wall -fPIC
-CXX_FLAGS+=-I$(ILA_HEADER)
-LD_FLAGS=-L$(ILA_LIB) -lilatoolsd 
+LD_FLAGS=-lila++
 
 SRC_DIR=src
 OBJ_DIR=obj

apps/riscv-spec/.gitignore

@@ -0,0 +1,4 @@
+main
+*~
+*.o
+

apps/riscv-spec/Makefile

@@ -0,0 +1,31 @@
+
+export ROOT_PATH  = $(shell pwd)
+export ILA_LIB    = $(ROOT_PATH)/../../build/lib
+export ILA_HEADER = $(ROOT_PATH)/../../include
+
+CXX=clang++
+CXX_FLAGS=-std=c++11 -Wall -fPIC
+CXX_FLAGS+=-I$(ILA_HEADER)
+LD_FLAGS=-L$(ILA_LIB) -lilatoolsd
+
+HDR_DIR=include
+SRC_DIR=src
+OBJ_DIR=obj
+
+HDR_FILES := $(wildcard $(HDR_DIR)/*.hpp)
+SRC_FILES := $(wildcard $(SRC_DIR)/*.cc)
+OBJ_FILES := $(patsubst $(SRC_DIR)/%.cc,$(OBJ_DIR)/%.o,$(SRC_FILES))
+
+main: $(OBJ_FILES)
+	   $(CXX) $(LD_FLAGS) -o $@ $^
+
+$(OBJ_DIR)/%.o: $(SRC_DIR)/%.cc $(OBJ_DIR) $(HDR_FILES)
+	   $(CXX) $(CXX_FLAGS) -I$(ROOT_PATH)/$(HDR_DIR) -c -o $@ $<
+
+$(OBJ_DIR):
+	mkdir $(OBJ_DIR)
+
+all: main.exe
+
+clean:
+	rm -rf $(OBJ_DIR)/*

apps/riscv-spec/README.md

@@ -0,0 +1,14 @@
+RISC-V ILA
+---------------
+
+User Level ISA : RV32I
+
+* 8 branch/jump instructions
+* 5 load instructions
+* 3 store instructions
+* 10 ALU instructions
+* 9 ALU-immediate instructions
+* 2 immediate instructions
+
+
+

apps/empty_proj/env.sh → apps/riscv-spec/env.sh

@@ -1,4 +1,5 @@
 #!/bin/sh
 
 export LD_LIBRARY_PATH=$(pwd)/../../build/lib/:$LD_LIBRARY_PATH
+export LIBRARY_PATH=$(pwd)/../../build/lib/:$LIBRARY_PATH
 

apps/riscv-spec/include/encoding.hpp

@@ -0,0 +1,79 @@
+/********************
+
+ RISC-V Encoding 
+
+********************/
+
+#ifndef __RISCV_ENCODING_HPP__
+#define __RISCV_ENCODING_HPP__
+
+#define XLEN                32
+#define INSTR_SIZE          XLEN
+#define MEM_WORD_ADDR_LEN   (XLEN-2)
+#define MEM_WORD            XLEN
+
+
+#define OP_LEN  7
+#define OPIMM 	BvConst(0x13, OP_LEN)
+#define LUI		BvConst(0x37, OP_LEN)
+#define AUIPC	BvConst(0x17, OP_LEN)
+#define OP		BvConst(0x33, OP_LEN)
+#define BRANCH	BvConst(0x63, OP_LEN)
+#define JAL		BvConst(0x6f, OP_LEN)
+#define JALR	BvConst(0x67, OP_LEN)
+#define LOAD	BvConst(0x03, OP_LEN)
+#define STORE	BvConst(0x23, OP_LEN)
+
+// funct3 for OPIMM
+
+#define FUNCT3_LEN 3
+#define ADDI    BvConst(0x0, FUNCT3_LEN)
+#define SLTI    BvConst(0x2, FUNCT3_LEN)
+#define SLTIU   BvConst(0x3, FUNCT3_LEN)
+#define ANDI    BvConst(0x7, FUNCT3_LEN)
+#define ORI     BvConst(0x6, FUNCT3_LEN)
+#define XORI    BvConst(0x4, FUNCT3_LEN)
+#define SLLI    BvConst(0x1, FUNCT3_LEN)
+#define SRLI    BvConst(0x5, FUNCT3_LEN)
+#define SRAI    BvConst(0x5, FUNCT3_LEN)
+
+#define FUNCT7_LEN 7
+#define SLLIfunct7 BvConst(0x00, FUNCT7_LEN)
+#define SRLIfunct7 BvConst(0x00, FUNCT7_LEN)
+#define SRAIfunct7 BvConst(0x20, FUNCT7_LEN)
+#define funct7_NM  BvConst(0x00, FUNCT7_LEN)
+#define funct7_PM  BvConst(0x20, FUNCT7_LEN)
+
+// funct3 for OP
+#define ADD     BvConst(0x0 ,  FUNCT3_LEN)
+#define SLL     BvConst(0x1 ,  FUNCT3_LEN)
+#define SLT     BvConst(0x2 ,  FUNCT3_LEN)
+#define SLTU    BvConst(0x3 ,  FUNCT3_LEN)
+#define XOR     BvConst(0x4 ,  FUNCT3_LEN)
+#define SRL     BvConst(0x5 ,  FUNCT3_LEN)
+#define OR      BvConst(0x6 ,  FUNCT3_LEN)
+#define AND     BvConst(0x7 ,  FUNCT3_LEN)
+#define SUB     BvConst(0x0 ,  FUNCT3_LEN)
+#define SRA     BvConst(0x5 ,  FUNCT3_LEN)
+
+// funct 3 for BRANCH
+#define BEQ     BvConst(0x0, FUNCT3_LEN)
+#define BNE     BvConst(0x1, FUNCT3_LEN)
+#define BLT     BvConst(0x4, FUNCT3_LEN)
+#define BGE     BvConst(0x5, FUNCT3_LEN)
+#define BLTU    BvConst(0x6, FUNCT3_LEN)
+#define BGEU    BvConst(0x7, FUNCT3_LEN)
+
+// funct 3 for L/S
+#define BYTE    BvConst(0x0 , FUNCT3_LEN)
+#define HALF    BvConst(0x1 , FUNCT3_LEN)
+#define WORD    BvConst(0x2 , FUNCT3_LEN)
+#define DOUBLE  BvConst(0x3 , FUNCT3_LEN)
+#define BU      BvConst(0x4 , FUNCT3_LEN)
+#define HU      BvConst(0x5 , FUNCT3_LEN)
+#define WU      BvConst(0x6 , FUNCT3_LEN)
+
+
+
+
+#endif

apps/riscv-spec/include/helpers.hpp

@@ -0,0 +1,23 @@
+/********************
+
+ ILA helpers  
+
+********************/
+
+
+#ifndef __ILA_HELPER_HPP__
+#define __ILA_HELPER_HPP__
+
+/*
+template<typename First, typename ... Rest>
+ExprRef mConcat(const First & arg, const Rest & ... rest ) {
+    return Concat(  arg , mConcat(rest...) );
+}
+*/
+
+#include <list>
+typedef std::list<ila::ExprRef> exp_list;
+ila::ExprRef lConcat(const exp_list & l);
+
+
+#endif

apps/riscv-spec/include/riscvIla.hpp

@@ -0,0 +1,76 @@
+/********************
+
+ RISC-V ILA  
+
+********************/
+
+#ifndef __RISCV_ILA_HPP__
+#define __RISCV_ILA_HPP__
+
+#include <vector>
+
+#include "encoding.hpp"
+
+
+
+class riscvILA_user
+{
+
+    Ila  model;
+
+    ExprRef         pc;
+    ExprRef         mem;
+    std::vector<ExprRef> GPR; // R0-R31
+
+    std::set<std::string>           Instrs;
+    std::map<std::string, InstrRef> InstrMap;
+
+    ExprRef         inst;
+
+    ExprRef         opcode;
+    ExprRef         rd;
+    ExprRef         rs1;
+    ExprRef         rs2;
+    ExprRef         funct3;
+    ExprRef         funct7;
+    ExprRef         funct12;
+    ExprRef         immI;
+    ExprRef         immS;
+    ExprRef         immB;
+    ExprRef         immU;
+    ExprRef         immJ;
+    ExprRef         csr_index;
+
+protected:
+    ExprRef indexIntoGPR(const ExprRef & idxBits);
+    void UpdateGPR(InstrRef & inst, const ExprRef & idxBits, const ExprRef & val );
+
+    ExprRef bv(int val) { return BvConst(val, XLEN); }
+    ExprRef zext(const ExprRef & v) {return ZExt( v, XLEN ); }
+    ExprRef sext(const ExprRef & v) {return SExt( v, XLEN ); }
+
+    ExprRef getSlice(const ExprRef & word,const ExprRef & lowBits, int width, bool unSigned);
+    ExprRef CombineSlices(const ExprRef & word, const ExprRef & lowBits, int width, const ExprRef & old);
+
+
+    // privileged model will overload these to insert their address translation
+    virtual ExprRef FetchFromMem(const ExprRef &m, const ExprRef &addr) { return Load(m,addr); }
+    virtual ExprRef LoadFromMem (const ExprRef &m, const ExprRef &addr) { return Load(m,addr); }
+    virtual ExprRef StoreToMem  (const ExprRef &m, const ExprRef &addr , const ExprRef &data) { return Store(m,addr,data); }
+
+public:
+    riscvILA_user( int pc_init_val );
+    void addInstructions();
+};
+
+
+
+
+class riscvILA_machine : public riscvILA_user
+{
+};
+
+
+
+
+#endif