From aeb83c296e6ca169ef6483562935f7b72bdb2db7 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 3 Nov 2016 16:28:20 +0000 Subject: split out RI node so that ppcmem model does not implement reserved instruction exception behaviour but sequential model does (for test suite). --- mips/mips_epilogue.sail | 5 ----- mips/mips_regfp.sail | 8 ++++---- mips/mips_ri.sail | 42 ++++++++++++++++++++++++++++++++++++++++++ src/Makefile | 4 ++-- 4 files changed, 48 insertions(+), 11 deletions(-) create mode 100644 mips/mips_ri.sail diff --git a/mips/mips_epilogue.sail b/mips/mips_epilogue.sail index 1b8d64f7..3771e26e 100644 --- a/mips/mips_epilogue.sail +++ b/mips/mips_epilogue.sail @@ -34,11 +34,6 @@ (* mips_epilogue.sail: end of decode, execute and AST definitions. *) -union ast member unit RI -function clause decode _ = Some(RI) -function clause execute (RI) = - SignalException (ResI) - end decode end execute end ast diff --git a/mips/mips_regfp.sail b/mips/mips_regfp.sail index 6cfa3230..714ad9fb 100644 --- a/mips/mips_regfp.sail +++ b/mips/mips_regfp.sail @@ -354,24 +354,24 @@ function (regfps,regfps,regfps,nias,dia,instruction_kind) initial_analysis (inst } case (J(offset)) -> { (* XXX actually unconditional jump *) - ik := IK_cond_branch; + (*ik := IK_cond_branch;*) Dia := DIA_concrete((PC + 4)[63..28] : offset : 0b00); } case (JAL(offset)) -> { (* XXX actually unconditional jump *) - ik := IK_cond_branch; + (*ik := IK_cond_branch;*) oR := RFull("GPR31") :: oR; Dia := DIA_concrete((PC + 4)[63..28] : offset : 0b00); } case (JR(rs)) -> { (* XXX actually unconditional jump *) - ik := IK_cond_branch; + (*ik := IK_cond_branch;*) iR := RFull(GPRs[rs]) :: iR; Dia := DIA_reg(RFull(GPRs[rs])); } case (JALR(rs, rd)) -> { (* XXX actually unconditional jump *) - ik := IK_cond_branch; + (*ik := IK_cond_branch;*) iR := RFull(GPRs[rs]) :: iR; oR := RFull("GPR31") :: oR; Dia := DIA_reg(RFull(GPRs[rs])); diff --git a/mips/mips_ri.sail b/mips/mips_ri.sail new file mode 100644 index 00000000..e1222b98 --- /dev/null +++ b/mips/mips_ri.sail @@ -0,0 +1,42 @@ +(*========================================================================*) +(* *) +(* Copyright (c) 2015-2016 Robert M. Norton *) +(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + +(* mips_ri.sail: only use if want unknown instructions to throw + exception (like real hardware) instead of die (convenient for ppcmem) *) + +union ast member unit RI +function clause decode _ = Some(RI) +function clause execute (RI) = + SignalException (ResI) + diff --git a/src/Makefile b/src/Makefile index 7849e666..5d501931 100644 --- a/src/Makefile +++ b/src/Makefile @@ -25,10 +25,10 @@ LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib ELFDIR= $(BITBUCKET_ROOT)/linksem MIPS_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/mips -MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail +MIPS_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail MIPS_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/mips_regfp.sail CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri -CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail elf: make -C $(ELFDIR) -- cgit v1.2.3