Index: trunk/hal/tsar_mips32/core/hal_kernel_types.h
===================================================================
--- trunk/hal/tsar_mips32/core/hal_kernel_types.h	(revision 452)
+++ trunk/hal/tsar_mips32/core/hal_kernel_types.h	(revision 452)
@@ -0,0 +1,202 @@
+/*
+ * hal_kernel_types.h - kernel types for TSAR-MIPS32 architecture.
+ *
+ * Author  Alain Greiner (2016)
+ *
+ * Copyright (c) UPMC Sorbonne Universites
+ *
+ * This file is part of ALMOS-MKH.
+ *
+ * ALMOS-MKH is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; version 2.0 of the License.
+ *
+ * ALMOS-MKH is distributed in the hope that it will be useful, but
+ * WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with ALMOS-MKH; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA
+ */
+
+#ifndef HAL_KERNEL_TYPES_H_
+#define HAL_KERNEL_TYPES_H_
+
+#include <kernel_config.h>
+
+#ifndef NULL
+#define NULL    (void*)0
+#endif
+
+/**************************************************************************
+ * This file defines both the hardware dependant and hardware independant
+ * data types used by the kernel for the TSAR-MIPS32 architecture.
+ **************************************************************************/
+
+/**************************************************************************
+ * This defines the .elf files format (used in kernel/libk/elf.h file). 
+ **************************************************************************/
+
+#define HAL_ELF_32_BITS
+
+/**************************************************************************
+ * Exact-width integer types.  
+ **************************************************************************/
+
+typedef signed char             int8_t;
+typedef unsigned char           uint8_t;
+
+typedef signed short            int16_t;
+typedef unsigned short          uint16_t;
+
+typedef signed long int         int32_t;
+typedef unsigned long int       uint32_t;
+
+typedef signed long long int    int64_t;
+typedef unsigned long long int  uint64_t;
+
+/***************************************************************************
+ * Boolean type and macros
+ **************************************************************************/
+
+typedef uint32_t      bool_t;
+
+#define false         0
+#define true          1
+
+/***************************************************************************
+ * Kernel error type : signed
+ **************************************************************************/
+
+typedef int32_t       error_t;
+
+/***************************************************************************
+ * Time related type
+ **************************************************************************/
+
+typedef uint64_t      cycle_t;   // for software cycle counters
+
+/***************************************************************************
+ * Global Process identifier type / fixed format 
+ * 16 MSB = cluster XY identifier
+ * 16 LSB = local process index
+ **************************************************************************/
+
+typedef uint32_t      pid_t;  
+
+/***************************************************************************
+ * Local Process index  
+ **************************************************************************/
+
+typedef uint16_t      lpid_t;
+
+/***************************************************************************
+ * Thread  identifier type / fixed format 
+ * 16 MSB = cluster XY identifier
+ * 16 LSB = local thread index
+ **************************************************************************/
+
+typedef uint32_t      trdid_t;
+
+/***************************************************************************
+ * Local Thread index 
+ **************************************************************************/
+
+typedef uint16_t      ltid_t;
+
+/***************************************************************************
+ * User identifier type
+ **************************************************************************/
+
+typedef uint32_t      uid_t;
+
+/***************************************************************************
+ * CPU identifier types
+ **************************************************************************/
+
+typedef uint16_t      lid_t;    // local index in cluster
+typedef uint32_t      gid_t;    // global (hardware) identifier
+
+/***************************************************************************
+ * File Descriptor Index in File Descriptor Array
+ **************************************************************************/
+
+typedef uint32_t      fdid_t;
+
+/***************************************************************************
+ * This structure defines a single 32 bits integer alone in a cache line. 
+ **************************************************************************/
+
+typedef struct cache_line_s
+{
+  union
+  {
+    uint32_t values[CONFIG_CACHE_LINE_SIZE>>2];
+    uint32_t value;
+  };
+}
+__attribute__((packed)) cacheline_t;
+
+/***************************************************************************
+ *  Address types and macros         !!!  hardware dependant  !!!
+ ***************************************************************************
+ * An extended pointer is a 64 bits integer, structured in two fields :
+ * - cxy : cluster identifier.
+ * - ptr : pointer in the virtual space of a single cluster.
+ *
+ * In TSAR (MIPS32), the kernel virtual space has 4 Gbytes per cluster
+ * - the cxy field occupies bits[47:32]
+ * - the ptr field occupies bits[31:0]
+ ***************************************************************************
+ * A physical address is a 64 bits integer, structured in two fields :
+ * - cxy : cluster identifier.
+ * - lpa : local physical address inside cluster.
+ *
+ * In TSAR (MIPS32), the physical space has 4Gbytes per cluster.
+ * - the cxy field occupies bits[39:32]
+ * - the lpa field occupies bits[31:0]
+ **************************************************************************/
+
+typedef uint64_t               xptr_t;        // extended pointer
+
+typedef uint16_t               cxy_t;         // cluster identifier
+
+typedef uint64_t               paddr_t;       // global physical address
+
+typedef uint32_t               lpa_t;         // local physical address
+
+typedef uint32_t               intptr_t;      // local pointer stored as integer
+
+typedef uint32_t               ppn_t;         // Physical Page Number
+
+typedef uint32_t               vpn_t;         // Virtual Page number
+
+
+#define XPTR_NULL              0
+
+#define PTR_MASK               0x00000000FFFFFFFFULL
+
+#define PTR_SHIFT              32
+
+#define GET_CXY(xp)            ((cxy_t)((xp) >> PTR_SHIFT))
+
+#define GET_PTR(xp)            ((void*)(uint32_t)((xp) & PTR_MASK))
+
+#define XPTR(cxy,ptr)          (((uint64_t)(cxy) << PTR_SHIFT) | (((uint32_t)(ptr)) & PTR_MASK))
+
+
+#define LPA_MASK               0x00000000FFFFFFFFULL
+
+#define LPA_SHIFT              32
+
+#define CXY_FROM_PADDR(paddr)  ((cxy_t)((paddr) >> LPA_SHIFT)) 
+
+#define LPA_FROM_PADDR(paddr)  (lpa_t)(paddr & LPA_MASK)
+
+#define PADDR(cxy,lpa)         (((uint64_t)(cxy) << LPA_SHIFT) | (((uint64_t)(lpa)) & LPA_MASK))
+
+
+
+#endif	/* HAL_KERNEL_TYPES_H_ */
Index: trunk/hal/tsar_mips32/core/hal_shared_types.h
===================================================================
--- trunk/hal/tsar_mips32/core/hal_shared_types.h	(revision 452)
+++ trunk/hal/tsar_mips32/core/hal_shared_types.h	(revision 452)
@@ -0,0 +1,42 @@
+/*
+ * hal_kernel_types.h - Data types shared by kernel & libraries for TSAR-MIPS32.
+ *
+ * Author  Alain Greiner (2016)
+ *
+ * Copyright (c) UPMC Sorbonne Universites
+ *
+ * This file is part of ALMOS-MKH.
+ *
+ * ALMOS-MKH is free software; you can redistribute it and/or modify it
+ * under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; version 2.0 of the License.
+ *
+ * ALMOS-MKH is distributed in the hope that it will be useful, but
+ * WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with ALMOS-MKH; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA
+ */
+
+#ifndef HAL_SHARED_TYPES_H_
+#define HAL_SHARED_TYPES_H_
+
+/*******************i***************************************************************
+ * This file defines - for the TSAR_MIPS32 architecture - the <reg_t> type, used 
+ * by the hal_user_syscall() function, called by several user-level libraries 
+ * to pass syscall arguments to the  kernel, and used by the do_syscall() function,
+ * called by the kernel syscall handler, to analyse arguments.
+ * It is also used by various kernel functions such as the hal_*_irq() functions
+ * to save/restore the SR register value.
+ **********************************************************************************/
+
+#ifndef NULL
+#define NULL    (void*)0
+#endif
+
+typedef unsigned long int     reg_t;    // core register
+
+#endif	/* HAL_TYPES_H_ */
Index: trunk/hal/tsar_mips32/core/hal_types.h
===================================================================
--- trunk/hal/tsar_mips32/core/hal_types.h	(revision 445)
+++ 	(revision )
@@ -1,195 +1,0 @@
-/*
- * hal_types.h - common kernel types for MIPS 32 bits
- *
- * Author  Alain Greiner (2016)
- *
- * Copyright (c) UPMC Sorbonne Universites
- *
- * This file is part of ALMOS-MKH.
- *
- * ALMOS-MKH is free software; you can redistribute it and/or modify it
- * under the terms of the GNU General Public License as published by
- * the Free Software Foundation; version 2.0 of the License.
- *
- * ALMOS-MKH is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with ALMOS-MKH; if not, write to the Free Software Foundation,
- * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA
- */
-
-#ifndef HAL_TYPES_H_
-#define HAL_TYPES_H_
-
-#include <kernel_config.h>
-
-#define HAL_32BIT
-
-#ifndef NULL
-#define NULL (void*)        0
-#endif
-
-/**************************************************************************
- *                      Exact-width integer types.  
- **************************************************************************/
-
-typedef   signed           char     int8_t;
-typedef unsigned           char    uint8_t;
-
-typedef   signed           short    int16_t;
-typedef unsigned           short   uint16_t;
-
-typedef   signed long      int      int32_t;
-typedef unsigned long      int     uint32_t;
-
-typedef   signed long long int      int64_t;
-typedef unsigned long long int     uint64_t;
-
-/***************************************************************************
- * Boolean type and macros
- **************************************************************************/
-
-typedef uint32_t      bool_t;
-
-#define false         0
-#define true          1
-
-/***************************************************************************
- * Kernel error type : signed
- **************************************************************************/
-
-typedef int32_t       error_t;
-
-/***************************************************************************
- * Time related type
- **************************************************************************/
-
-typedef uint64_t      cycle_t;   // for cycle counters
-
-/***************************************************************************
- * Global Process identifier type / fixed format 
- * 16 MSB = cluster XY identifier
- * 16 LSB = local process index
- **************************************************************************/
-
-typedef uint32_t      pid_t;  
-
-/***************************************************************************
- * Local Process index  
- **************************************************************************/
-
-typedef uint16_t      lpid_t;
-
-/***************************************************************************
- * Thread  identifier type / fixed format 
- * 16 MSB = cluster XY identifier
- * 16 LSB = local thread index
- **************************************************************************/
-
-typedef uint32_t      trdid_t;
-
-/***************************************************************************
- * Local Thread index 
- **************************************************************************/
-
-typedef uint16_t      ltid_t;
-
-/***************************************************************************
- * User identifier type
- **************************************************************************/
-
-typedef uint32_t      uid_t;
-
-/***************************************************************************
- * CPU identifier types
- **************************************************************************/
-
-typedef uint16_t      lid_t;    // local index in cluster
-typedef uint32_t      gid_t;    // global (hardware) identifier
-
-/***************************************************************************
- * File Descriptor Index in File Descriptor Array
- **************************************************************************/
-
-typedef uint32_t      fdid_t;
-
-/***************************************************************************
- * This structure defines a single 32 bits integer alone in a cache line. 
- **************************************************************************/
-
-typedef struct cache_line_s
-{
-  union
-  {
-    uint32_t values[CONFIG_CACHE_LINE_SIZE>>2];
-    uint32_t value;
-  };
-}
-__attribute__((packed)) cacheline_t;
-
-/***************************************************************************
- *  Address types and macros         !!!  hardware dependant  !!!
- ***************************************************************************
- * An extended pointer is a 64 bits integer, structured in two fields :
- * - cxy : cluster identifier.
- * - ptr : pointer in the virtual space of a single cluster.
- *
- * In TSAR (MIPS32), the kernel virtual space has 4 Gbytes per cluster
- * - the cxy field occupies bits[47:32]
- * - the ptr field occupies bits[31:0]
- ***************************************************************************
- * A physical address is a 64 bits integer, structured in two fields :
- * - cxy : cluster identifier.
- * - lpa : local physical address inside cluster.
- *
- * In TSAR (MIPS32), the physical space has 4Gbytes per cluster.
- * - the cxy field occupies bits[39:32]
- * - the lpa field occupies bits[31:0]
- **************************************************************************/
-
-typedef uint32_t               reg_t;         // core register
-
-typedef uint64_t               xptr_t;        // extended pointer
-
-typedef uint16_t               cxy_t;         // cluster identifier
-
-typedef uint64_t               paddr_t;       // global physical address
-
-typedef uint32_t               lpa_t;         // local physical address
-
-typedef uint32_t               intptr_t;      // local pointer stored as integer
-
-typedef uint32_t               ppn_t;         // Physical Page Number
-
-typedef uint32_t               vpn_t;         // Virtual Page number
-
-
-#define XPTR_NULL              0
-
-#define PTR_MASK               0x00000000FFFFFFFFULL
-
-#define PTR_SHIFT              32
-
-#define GET_CXY(xp)            ((cxy_t)((xp) >> PTR_SHIFT))
-
-#define GET_PTR(xp)            ((void*)(uint32_t)((xp) & PTR_MASK))
-
-#define XPTR(cxy,ptr)          (((uint64_t)(cxy) << PTR_SHIFT) | (((uint32_t)(ptr)) & PTR_MASK))
-
-
-#define LPA_MASK               0x00000000FFFFFFFFULL
-
-#define LPA_SHIFT              32
-
-#define CXY_FROM_PADDR(paddr)  ((cxy_t)((paddr) >> LPA_SHIFT)) 
-
-#define LPA_FROM_PADDR(paddr)  (lpa_t)(paddr & LPA_MASK)
-
-#define PADDR(cxy,lpa)         (((uint64_t)(cxy) << LPA_SHIFT) | (((uint64_t)(lpa)) & LPA_MASK))
-
-
-
-#endif	/* HAL_TYPES_H_ */
